pith. machine review for the scientific record. sign in
lemma proved term proof

w_t_nonneg

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 126lemma w_t_nonneg (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
 127    0 ≤ w_t P Tdyn τ0 := by

proof body

Term-mode proof.

 128  -- For defaultConfig, eps_t = 0.01 > 0.
 129  -- Thus t = max(0.01, Tdyn/τ0) > 0.
 130  -- rpow t alpha is non-negative for t > 0.
 131  -- Result follows from Clag <= 1.
 132  unfold w_t
 133  exact w_t_nonneg_with defaultConfig defaultConfig_props P H Tdyn τ0
 134
 135/-- Time-kernel is at least 1 when alpha >= 0, Clag >= 0 and Tdyn >= tau0. -/

depends on (29)

Lean names referenced from this declaration's body.