lemma
proved
tactic proof
w_t_nonneg_with
show as:
view Lean formalization →
formal statement (Lean)
104lemma w_t_nonneg_with (cfg : Config) (hcfg : ConfigProps cfg)
105 (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
106 0 ≤ w_t_with cfg P Tdyn τ0 := by
proof body
Tactic-mode proof.
107 dsimp [w_t_with]
108 set t := max cfg.eps_t (Tdyn / τ0) with ht
109 have ht_nonneg : 0 ≤ t := by
110 have hle : cfg.eps_t ≤ t := by
111 simpa [ht] using le_max_left cfg.eps_t (Tdyn / τ0)
112 exact le_trans hcfg.eps_t_nonneg hle
113 have hrpow_nonneg : 0 ≤ Real.rpow t P.alpha := by
114 simpa using Real.rpow_nonneg ht_nonneg P.alpha
115 have h_rpow_minus_one : (-1 : ℝ) ≤ Real.rpow t P.alpha - 1 := by
116 linarith
117 have h_mul : (-P.Clag : ℝ) ≤ P.Clag * (Real.rpow t P.alpha - 1) := by
118 have h := mul_le_mul_of_nonneg_left h_rpow_minus_one H.Clag_nonneg
119 -- h : P.Clag * (-1) ≤ P.Clag * (Real.rpow t P.alpha - 1)
120 simpa using h
121 have h_base : 0 ≤ (1 : ℝ) - P.Clag := sub_nonneg.mpr H.Clag_le_one
122 have h_lower : (1 : ℝ) - P.Clag ≤ 1 + P.Clag * (Real.rpow t P.alpha - 1) := by
123 linarith
124 exact le_trans h_base h_lower
125