294theorem kernel_perturbation_ge_one (P : KernelParams) (k_min k a : ℝ) : 295 1 ≤ kernel_perturbation P k_min k a := by
proof body
Tactic-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.