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

poisson_operator_solves

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)

  27theorem poisson_operator_solves (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
  28    SolvesModifiedPoisson P k a δρ (poisson_operator P k a δρ) := by

proof body

Term-mode proof.

  29  unfold SolvesModifiedPoisson poisson_operator
  30  simp only [if_neg hk]
  31  have hk2 : (k^2 : ℝ) ≠ 0 := pow_ne_zero 2 hk
  32  field_simp
  33
  34/-- Stability/Scaling Bound: The ILG potential Φ is strictly enhanced relative to
  35    the GR potential Φ_GR by exactly the kernel factor w(k, a). -/

depends on (9)

Lean names referenced from this declaration's body.