kernel_perturbation_bounded_above

formal source

 310This resolves Beltracchi's concern (2): the kernel does not run away as
 311`k → 0`. The homogeneous mode is bounded by a finite ceiling fixed by
 312the recognition horizon. -/
 313theorem kernel_perturbation_bounded_above
 314    (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min) {a : ℝ} (ha : 0 < a)
 315    (k : ℝ) :
 316    kernel_perturbation P k_min k a
 317      ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
 318  unfold kernel_perturbation
 319  -- max k_min k ≥ k_min, so 1/(max k_min k) ≤ 1/k_min, so
 320  -- a/(max k_min k * tau0) ≤ a/(k_min * tau0).
 321  have h_max_ge : k_min ≤ max k_min k := le_max_left _ _
 322  have h_max_pos : 0 < max k_min k := lt_of_lt_of_le hkmin h_max_ge
 323  have h_kmin_tau_pos : 0 < k_min * P.tau0 := mul_pos hkmin P.tau0_pos
 324  have h_max_tau_pos : 0 < max k_min k * P.tau0 := mul_pos h_max_pos P.tau0_pos
 325  have h_arg_le : a / (max k_min k * P.tau0) ≤ a / (k_min * P.tau0) := by
 326    apply div_le_div_of_nonneg_left (le_of_lt ha) h_kmin_tau_pos
 327    exact mul_le_mul_of_nonneg_right h_max_ge P.tau0_pos.le
 328  -- Now max 0.01 is monotone, and rpow is monotone for positive base + nonneg exponent.
 329  have h_max_le : max 0.01 (a / (max k_min k * P.tau0))
 330        ≤ max 0.01 (a / (k_min * P.tau0)) := by
 331    exact max_le_max (le_refl _) h_arg_le
 332  have h_lhs_pos : 0 < max 0.01 (a / (max k_min k * P.tau0)) := by
 333    apply lt_max_of_lt_left; norm_num
 334  have h_rpow_le : (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
 335        ≤ (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
 336    apply Real.rpow_le_rpow (le_of_lt h_lhs_pos) h_max_le P.alpha_nonneg
 337  have h_mul_le : P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
 338        ≤ P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
 339    exact mul_le_mul_of_nonneg_left h_rpow_le P.C_nonneg
 340  linarith
 341
 342/-- **The Hubble ceiling theorem.** The Hubble-saturated kernel is bounded
 343above by the value attained at the Hubble wavenumber `k = a H`. This is