theorem
proved
dJdt_eq_viscous_plus_stretching
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NavierStokes.DiscreteVorticity on GitHub at line 105.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
102 simp [hzero]
103
104/-- The exact derivative identity can be rewritten after transport cancellation. -/
105theorem dJdt_eq_viscous_plus_stretching {siteCount : ℕ} (e : EvolutionIdentity siteCount)
106 (htransport : totalTransport e.contributions = 0) :
107 e.dJdt = totalViscous e.contributions + totalStretching e.contributions := by
108 rw [e.split, htransport, zero_add]
109
110/-- If stretching is absorbed by viscosity, then the total derivative is nonpositive. -/
111theorem dJdt_nonpos_of_transport_cancel_and_absorption
112 {siteCount : ℕ} (e : EvolutionIdentity siteCount)
113 (htransport : totalTransport e.contributions = 0)
114 (habsorb :
115 totalStretching e.contributions ≤ - totalViscous e.contributions) :
116 e.dJdt ≤ 0 := by
117 rw [dJdt_eq_viscous_plus_stretching e htransport]
118 linarith
119
120end
121
122end DiscreteVorticity
123end NavierStokes
124end IndisputableMonolith