theorem
proved
tactic proof
kernel_at_ratio_one_alpha_zero
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
120 unfold kernel
121 have hmax : max 0.01 (a / (k * P.tau0)) = 1 := by
122 rw [hratio]
123 exact max_eq_right h1ge
124 simp [hmax, hα, Real.rpow_zero]
125
126/-- Kernel equals 1 when C = 0 (no ILG modification). -/