theorem
proved
tactic proof
kernel_ge_one
show as:
view Lean formalization →
formal statement (Lean)
105theorem kernel_ge_one (P : KernelParams) (k a : ℝ) : 1 ≤ kernel P k a := by
proof body
Tactic-mode proof.
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. -/