theorem
proved
tactic proof
kernel_perturbation_bounded_above
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
344a specialization of `kernel_perturbation_bounded_above` to the canonical
345RS choice `k_min = a H / c`. -/