kernel_with_Hubble

formal source

 257
 258/-- The Hubble-saturated kernel: an IR cutoff specialization with
 259    `k_min = a · H` (in units where `c = 1`). -/
 260noncomputable def kernel_with_Hubble (P : KernelParams) (a H k : ℝ) : ℝ :=
 261  kernel_perturbation P (a * H) k a
 262
 263/-- The perturbation kernel reduces to the original `kernel` when the
 264    wavenumber is at or above the IR cutoff. -/
 265theorem kernel_perturbation_eq_kernel_of_ge
 266    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k_min ≤ k) :
 267    kernel_perturbation P k_min k a = kernel P k a := by
 268  unfold kernel_perturbation kernel
 269  have hmax : max k_min k = k := max_eq_right h
 270  rw [hmax]
 271
 272/-- The perturbation kernel collapses to the IR-saturated value when
 273    `k ≤ k_min`. -/
 274theorem kernel_perturbation_at_IR_floor
 275    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k ≤ k_min) :
 276    kernel_perturbation P k_min k a = kernel P k_min a := by
 277  unfold kernel_perturbation kernel
 278  have hmax : max k_min k = k_min := max_eq_left h
 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