pith. machine review for the scientific record. sign in
theorem proved term proof

kernel_perturbation_eq_kernel_of_ge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 265theorem kernel_perturbation_eq_kernel_of_ge
 266    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k_min ≤ k) :
 267    kernel_perturbation P k_min k a = kernel P k a := by

proof body

Term-mode proof.

 268  unfold kernel_perturbation kernel
 269  have hmax : max k_min k = k := max_eq_right h
 270  rw [hmax]
 271
 272/-- The perturbation kernel collapses to the IR-saturated value when
 273    `k ≤ k_min`. -/

depends on (5)

Lean names referenced from this declaration's body.