poisson_operator_perturbation

formal source

  79cutoff `k_min`. Below `k_min` the kernel saturates at its IR-floor value,
  80preventing the divergence at `k = 0`. The canonical RS choice for the
  81cutoff is the Hubble wavenumber `k_min = a H / c`. -/
  82noncomputable def poisson_operator_perturbation (P : KernelParams)
  83    (k_min k a δρ : ℝ) : ℝ :=
  84  if k = 0 then 0
  85  else -(4 * Real.pi * kernel_perturbation P k_min k a * δρ) / k^2
  86
  87/-- The combined causality-bound Poisson operator: background plus
  88perturbation, with the kernel acting only on the perturbation. -/
  89noncomputable def poisson_operator_full (P : KernelParams)
  90    (k_min k a ρ_bar δρ : ℝ) : ℝ :=
  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