kernel_eq_one_of_C_zero

formal source

 124  simp [hmax, hα, Real.rpow_zero]
 125
 126/-- Kernel equals 1 when C = 0 (no ILG modification). -/
 127theorem kernel_eq_one_of_C_zero (P : KernelParams) (hC : P.C = 0) (k a : ℝ) :
 128    kernel P k a = 1 := by
 129  simp [kernel, hC]
 130
 131/-! ## Monotonicity Properties -/
 132
 133/-- For fixed k and positive α, the kernel is monotonically increasing in a
 134    when a/(k τ₀) ≥ 0.01. -/
 135theorem kernel_mono_in_a (P : KernelParams) (hα_pos : 0 < P.alpha) (hC_pos : 0 < P.C)
 136    (k : ℝ) (hk : 0 < k) (a₁ a₂ : ℝ)
 137    (ha₁ : 0.01 * (k * P.tau0) ≤ a₁) (ha₁₂ : a₁ ≤ a₂) :
 138    kernel P k a₁ ≤ kernel P k a₂ := by
 139  unfold kernel
 140  -- When a ≥ 0.01 * (k τ₀), the max is just a / (k τ₀)
 141  have hktau_pos : 0 < k * P.tau0 := mul_pos hk P.tau0_pos
 142  have hr₁ : 0.01 ≤ a₁ / (k * P.tau0) := by
 143    rwa [le_div_iff₀ hktau_pos]
 144  have hmax₁ : max 0.01 (a₁ / (k * P.tau0)) = a₁ / (k * P.tau0) := max_eq_right hr₁
 145  have hr₂ : 0.01 ≤ a₂ / (k * P.tau0) := by
 146    have : a₁ / (k * P.tau0) ≤ a₂ / (k * P.tau0) := by
 147      apply div_le_div_of_nonneg_right ha₁₂
 148      exact le_of_lt hktau_pos
 149    linarith
 150  have hmax₂ : max 0.01 (a₂ / (k * P.tau0)) = a₂ / (k * P.tau0) := max_eq_right hr₂
 151  rw [hmax₁, hmax₂]
 152  -- Now show: 1 + C·(a₁/(kτ₀))^α ≤ 1 + C·(a₂/(kτ₀))^α
 153  apply add_le_add_right
 154  apply mul_le_mul_of_nonneg_left _ (le_of_lt hC_pos)
 155  -- rpow is monotone for positive base and positive exponent
 156  apply Real.rpow_le_rpow
 157  · exact le_of_lt (lt_of_lt_of_le (by norm_num : (0 : ℝ) < 0.01) hr₁)