kernel_with_Hubble_bounded_above

formal source

 343above by the value attained at the Hubble wavenumber `k = a H`. This is
 344a specialization of `kernel_perturbation_bounded_above` to the canonical
 345RS choice `k_min = a H / c`. -/
 346theorem kernel_with_Hubble_bounded_above
 347    (P : KernelParams) {a H : ℝ} (ha : 0 < a) (hH : 0 < H) (k : ℝ) :
 348    kernel_with_Hubble P a H k
 349      ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha := by
 350  unfold kernel_with_Hubble
 351  exact kernel_perturbation_bounded_above P (mul_pos ha hH) ha k
 352
 353/-- The background mode is independent of every kernel parameter: the
 354homogeneous density does not source any ILG enhancement. This formalizes
 355the perturbation/background split that resolves Beltracchi's concern (2)
 356on the Lean side. -/
 357theorem kernel_background_independent_of_params (P : KernelParams) :
 358    kernel_background = 1 := rfl
 359
 360/-- **The mode partition.** For a density field `ρ = ρ̄ + δρ` with
 361homogeneous mean `ρ̄` and zero-mean fluctuation `δρ`, the ILG-modified
 362Poisson source decomposes as
 363\[ \rho_{\rm eff}(k,a) = \bar\rho \cdot k_{\rm bg} + \delta\rho(k) \cdot
 364  w_{\rm pert}(k_{\min}, k, a), \]
 365with the background factor `k_bg = 1` and the perturbation factor
 366saturated at `kernel_perturbation P k_min k_min a`. -/
 367noncomputable def mode_partition (P : KernelParams) (k_min k a ρ_bar δρ : ℝ) : ℝ :=
 368  ρ_bar * kernel_background + δρ * kernel_perturbation P k_min k a
 369
 370theorem mode_partition_eq (P : KernelParams) (k_min k a ρ_bar δρ : ℝ) :
 371    mode_partition P k_min k a ρ_bar δρ
 372      = ρ_bar + δρ * kernel_perturbation P k_min k a := by
 373  unfold mode_partition kernel_background; ring
 374
 375/-- **Background mode of the partition is unmodified.** When `δρ = 0`,
 376the effective source equals the background source — no ILG enhancement