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

w_t_ref_with

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)

  80lemma w_t_ref_with (cfg : Config) (hcfg : ConfigProps cfg)
  81  (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t_with cfg P τ0 τ0 = 1 := by

proof body

Tactic-mode proof.

  82  dsimp [w_t_with]
  83  have hdiv : τ0 / τ0 = (1 : ℝ) := by
  84    field_simp [hτ]
  85  have hmax : max cfg.eps_t (τ0 / τ0) = (1 : ℝ) := by
  86    simpa [hdiv, max_eq_right hcfg.eps_t_le_one]
  87  simp [hmax]
  88

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.