theorem
proved
exponential_vorticity_decay
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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