poisson_background_independent_of_kernel

formal source

  91  poisson_operator_background a ρ_bar + poisson_operator_perturbation P k_min k a δρ
  92
  93/-- The background piece is independent of the kernel parameters. -/
  94@[simp] theorem poisson_background_independent_of_kernel
  95    (P : KernelParams) (a ρ_bar : ℝ) :
  96    poisson_operator_full P 0 0 a ρ_bar 0
  97      = poisson_operator_background a ρ_bar := by
  98  unfold poisson_operator_full poisson_operator_perturbation
  99  simp
 100
 101/-- The perturbation kernel inside `poisson_operator_perturbation` is
 102bounded above by its IR-saturated value. This is the operator-level
 103restatement of `kernel_perturbation_bounded_above`: the multiplier in
 104front of `δρ/k²` is uniformly bounded above by a finite ceiling fixed by
 105the IR cutoff, so the perturbation operator does not run away as
 106`k → 0`. -/
 107theorem poisson_operator_perturbation_kernel_bounded
 108    (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min)
 109    {a : ℝ} (ha : 0 < a) (k : ℝ) :
 110    kernel_perturbation P k_min k a
 111      ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha :=
 112  kernel_perturbation_bounded_above P hkmin ha k
 113
 114/-- **Background-mode invariance.** When the perturbation `δρ = 0` (pure
 115homogeneous configuration), the perturbation operator vanishes and only
 116the standard FRW background remains. This is the operator-level statement
 117that the ILG kernel does not affect the homogeneous mode. -/
 118@[simp] theorem poisson_operator_perturbation_homogeneous
 119    (P : KernelParams) (k_min k a : ℝ) :
 120    poisson_operator_perturbation P k_min k a 0 = 0 := by
 121  unfold poisson_operator_perturbation
 122  by_cases hk : k = 0
 123  · simp [hk]
 124  · simp [hk]