theorem
proved
operator_transport_zero
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NavierStokes.DiscreteNSOperator on GitHub at line 280.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
277def operatorPairBudget {siteCount : ℕ} (ns : IncompressibleNSOperator siteCount) : ℝ :=
278 indexedPairBudget (pairEventAt ns)
279
280theorem operator_transport_zero {siteCount : ℕ}
281 (ns : IncompressibleNSOperator siteCount) :
282 totalTransport ns.contributions = 0 := by
283 unfold totalTransport
284 rw [ns.transport_def]
285 exact total_conservativeTransportField_zero _ _
286
287theorem operatorPairBudget_nonneg {siteCount : ℕ}
288 (ns : IncompressibleNSOperator siteCount) :
289 0 ≤ operatorPairBudget ns := by
290 unfold operatorPairBudget
291 exact indexedPairBudget_nonneg (pairEventAt ns)
292
293theorem totalStretching_le_operatorPairBudget {siteCount : ℕ}
294 (ns : IncompressibleNSOperator siteCount) :
295 totalStretching ns.contributions ≤ operatorPairBudget ns := by
296 unfold totalStretching total operatorPairBudget indexedPairBudget
297 refine Finset.sum_le_sum ?_
298 intro i hi
299 simpa [pairEventAt, pairEventBudget] using ns.stretching_le_pair_budget i
300
301theorem operatorPairBudget_absorbed_by_viscosity {siteCount : ℕ}
302 (ns : IncompressibleNSOperator siteCount) :
303 operatorPairBudget ns ≤ - totalViscous ns.contributions := by
304 simpa [operatorPairBudget, pairEventAt] using ns.pair_budget_absorbed_by_viscosity
305
306end
307
308end DiscreteNSOperator
309end NavierStokes
310end IndisputableMonolith