theorem
proved
exponential_vorticity_decay
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NavierStokes.VortexStretching on GitHub at line 127.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
124
125/-! ## Exponential Decay -/
126
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
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