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

w_t_ge_one

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)

 136lemma w_t_ge_one (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) (hτ : 0 < τ0) (hT : τ0 ≤ Tdyn) :
 137    1 ≤ w_t P Tdyn τ0 := by

proof body

Term-mode proof.

 138  unfold w_t w_t_with
 139  let t := max defaultConfig.eps_t (Tdyn / τ0)
 140  have h_ratio : 1 ≤ Tdyn / τ0 := (one_le_div hτ).mpr hT
 141  have h_base : 1 ≤ t := le_max_of_le_right h_ratio
 142  -- Since base >= 1 and alpha >= 0, base^alpha >= 1
 143  have h_pow : 1 ≤ t ^ P.alpha := Real.one_le_rpow h_base H.alpha_nonneg
 144  have h_diff : 0 ≤ t ^ P.alpha - 1 := sub_nonneg.mpr h_pow
 145  have h_mul : 0 ≤ P.Clag * (t ^ P.alpha - 1) :=
 146    mul_nonneg H.Clag_nonneg h_diff
 147  -- Goal: 1 ≤ 1 + P.Clag * (t ^ P.alpha - 1)
 148  -- This follows from h_mul: 0 ≤ P.Clag * (t ^ P.alpha - 1)
 149  simp only [ge_iff_le, le_add_iff_nonneg_right]
 150  exact h_mul
 151
 152end
 153end ILG
 154end Gravity
 155end IndisputableMonolith

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.