poisson_operator_solves

formal source

  24  - (k^2 * Φ) = 4 * Real.pi * kernel P k a * δρ
  25
  26/-- The operator definition satisfies the predicate. -/
  27theorem poisson_operator_solves (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
  28    SolvesModifiedPoisson P k a δρ (poisson_operator P k a δρ) := by
  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). -/
  36theorem poisson_enhancement (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
  37    let Φ_ILG := poisson_operator P k a δρ
  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. -/
  49theorem poisson_coercive (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) (hδρ : δρ ≠ 0) :
  50    poisson_operator P k a δρ ≠ 0 := by
  51  unfold poisson_operator
  52  simp only [if_neg hk]
  53  have hk2 : (k^2 : ℝ) ≠ 0 := pow_ne_zero 2 hk
  54  have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 :=
  55    mul_ne_zero (by norm_num) Real.pi_ne_zero
  56  have hkern_ne : kernel P k a ≠ 0 := (kernel_pos P k a).ne'
  57  have hnum_ne : (4 * Real.pi * kernel P k a * δρ : ℝ) ≠ 0 :=