theorem
proved
master_absorption
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 117.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
114
115/-- Master absorption theorem: the J-cost derivative is nonpositive when
116transport cancels and stretching is absorbed by viscosity. -/
117theorem master_absorption
118 {dJdt transport_total viscous_total stretching_total : ℝ}
119 (hsplit : dJdt = transport_total + viscous_total + stretching_total)
120 (htransport : transport_total = 0)
121 (habsorb : stretching_total ≤ -viscous_total) :
122 dJdt ≤ 0 := by
123 rw [hsplit, htransport, zero_add]; linarith
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