theorem
proved
tactic proof
kernel_mono_in_a
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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₁)
158 · exact div_le_div_of_nonneg_right ha₁₂ (le_of_lt hktau_pos)
159 · exact le_of_lt hα_pos
160
161/-! ## Connection to RS Constants -/
162
163/-- The RS-canonical alpha equals alphaLock = (1 - 1/φ)/2. -/