kernel_perturbation_at_IR_floor

formal source

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