theorem
proved
tactic proof
poisson_enhancement
show as:
view Lean formalization →
formal statement (Lean)
36theorem poisson_enhancement (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
37 let Φ_ILG := poisson_operator P k a δρ
proof body
Tactic-mode proof.
38 let Φ_GR := -(4 * Real.pi * δρ) / k^2
39 |Φ_ILG| = kernel P k a * |Φ_GR| := by
40 unfold poisson_operator
41 simp only [if_neg hk]
42 have h_kernel_pos : 0 < kernel P k a := kernel_pos P k a
43 -- Rewrite -(4πw·δρ)/k² as w·(-(4π·δρ)/k²) under absolute value.
44 have h_eq : -(4 * Real.pi * kernel P k a * δρ) / k^2
45 = kernel P k a * (-(4 * Real.pi * δρ) / k^2) := by ring
46 rw [h_eq, abs_mul, abs_of_pos h_kernel_pos]
47
48/-- Coercivity Bound: The modified potential is non-vanishing for any non-vanishing source. -/