kernel_pos

formal source

  90/-! ## Basic Properties -/
  91
  92/-- Kernel is always positive for valid parameters. -/
  93theorem kernel_pos (P : KernelParams) (k a : ℝ) : 0 < kernel P k a := by
  94  unfold kernel
  95  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
  96    apply lt_max_of_lt_left
  97    norm_num
  98  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
  99    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
 100  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
 101    mul_nonneg P.C_nonneg hpow_nonneg
 102  linarith
 103
 104/-- Kernel is at least 1. -/
 105theorem kernel_ge_one (P : KernelParams) (k a : ℝ) : 1 ≤ kernel P k a := by
 106  unfold kernel
 107  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
 108    apply lt_max_of_lt_left
 109    norm_num
 110  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
 111    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
 112  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
 113    mul_nonneg P.C_nonneg hpow_nonneg
 114  linarith
 115
 116/-- Kernel equals 1 + C when the ratio a/(k τ₀) = 1 and α = 0. -/
 117theorem kernel_at_ratio_one_alpha_zero (P : KernelParams) (hα : P.alpha = 0)
 118    (k a : ℝ) (hk : k ≠ 0) (hratio : a / (k * P.tau0) = 1) (h1ge : (0.01 : ℝ) ≤ 1) :
 119    kernel P k a = 1 + P.C := by
 120  unfold kernel
 121  have hmax : max 0.01 (a / (k * P.tau0)) = 1 := by
 122    rw [hratio]
 123    exact max_eq_right h1ge