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

exponential_vorticity_decay

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)

 127theorem exponential_vorticity_decay {nu h mu w0 : ℝ}
 128    (hw0 : 0 ≤ w0)
 129    (hdom : mu ≤ nu / h ^ 2)
 130    (omega : ℝ → ℝ)
 131    (h_ode : ∀ {t : ℝ}, 0 ≤ t → omega t ≤ w0 * Real.exp (-(nu / h ^ 2 - mu) * t)) :
 132    ∀ {t : ℝ}, 0 ≤ t → omega t ≤ w0 := by

proof body

Tactic-mode proof.

 133  intro t ht
 134  have hgap : 0 ≤ nu / h ^ 2 - mu := by linarith
 135  have hexp : Real.exp (-(nu / h ^ 2 - mu) * t) ≤ 1 := by
 136    apply Real.exp_le_one_iff.mpr
 137    nlinarith [mul_nonneg hgap ht]
 138  exact le_trans (h_ode ht) (mul_le_of_le_one_right hw0 hexp)
 139
 140end
 141
 142end VortexStretching
 143end NavierStokes
 144end IndisputableMonolith

depends on (2)

Lean names referenced from this declaration's body.