`operatorPairBudget`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 277 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteNSOperator on GitHub at line 277.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 274  amplitude_pos := ns.pairAmplitude_pos i
 275  stretchFactor_pos := ns.pairStretchFactor_pos i
 276
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.