kernel_perturbation_pos

formal source

 279  rw [hmax]
 280
 281/-- The perturbation kernel is positive. -/
 282theorem kernel_perturbation_pos (P : KernelParams) (k_min k a : ℝ) :
 283    0 < kernel_perturbation P k_min k a := by
 284  unfold kernel_perturbation
 285  have hmax_pos : 0 < max 0.01 (a / (max k_min k * P.tau0)) := by
 286    apply lt_max_of_lt_left; norm_num
 287  have hpow_nonneg : 0 ≤ (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha :=
 288    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
 289  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha :=
 290    mul_nonneg P.C_nonneg hpow_nonneg
 291  linarith
 292
 293/-- The perturbation kernel is at least 1. -/
 294theorem kernel_perturbation_ge_one (P : KernelParams) (k_min k a : ℝ) :
 295    1 ≤ kernel_perturbation P k_min k a := by
 296  unfold kernel_perturbation
 297  have hmax_pos : 0 < max 0.01 (a / (max k_min k * P.tau0)) := by
 298    apply lt_max_of_lt_left; norm_num
 299  have hpow_nonneg : 0 ≤ (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha :=
 300    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
 301  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha :=
 302    mul_nonneg P.C_nonneg hpow_nonneg
 303  linarith
 304
 305/-- **The IR boundedness theorem.** For any positive IR cutoff `k_min > 0`,
 306positive scale factor `a > 0`, and any wavenumber `k`, the perturbation
 307kernel is bounded above by its IR-saturated value:
 308\[ w_{\rm pert}(k_{\min}, k, a) \le 1 + C \left(\frac{a}{k_{\min}\,\tau_0}\right)^\alpha. \]
 309
 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. -/