`pairEventAt`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 270 · 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 270.

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

 267  pair_budget_absorbed_by_viscosity := op.viscous_absorbs
 268
 269/-- The concrete RCL pair event attached to a lattice site. -/
 270def pairEventAt {siteCount : ℕ} (ns : IncompressibleNSOperator siteCount)
 271    (i : Fin siteCount) : PairEvent where
 272  amplitude := ns.pairAmplitude i
 273  stretchFactor := ns.pairStretchFactor i
 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

papers checked against this theorem

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