kernel_perturbation_ge_one

formal source

 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. -/
 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