`IncompressibleNSOperator`

definition

show as: view math explainer →

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

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

 212
 213/-- Full operator surface, now constructible from a `CoreNSOperator`.
 214Retained for backward compatibility with downstream modules. -/
 215structure IncompressibleNSOperator (siteCount : ℕ) extends EvolutionIdentity siteCount where
 216  topology : LatticeTopology siteCount
 217  h : ℝ
 218  ν : ℝ
 219  h_pos : 0 < h
 220  ν_pos : 0 < ν
 221  state : State siteCount
 222  velocity : VectorField siteCount
 223  divergence_free : ∀ x : Fin siteCount, divergence topology h velocity x = 0
 224  transportFlux : ScalarField siteCount
 225  transportPerm : Equiv.Perm (Fin siteCount)
 226  transport_def :
 227    contributions.transport = conservativeTransportField transportFlux transportPerm
 228  viscous_def :
 229    contributions.viscous = fun x => ν * scalarLaplacian topology h state.omega x
 230  pairAmplitude : Fin siteCount → ℝ
 231  pairStretchFactor : Fin siteCount → ℝ
 232  pairAmplitude_pos : ∀ i : Fin siteCount, 0 < pairAmplitude i
 233  pairStretchFactor_pos : ∀ i : Fin siteCount, 0 < pairStretchFactor i
 234  stretching_le_pair_budget :
 235    ∀ i : Fin siteCount,
 236      contributions.stretching i ≤
 237        pairwiseStretchingChange (pairAmplitude i) (pairStretchFactor i)
 238  pair_budget_absorbed_by_viscosity :
 239    indexedPairBudget (fun i =>
 240      { amplitude := pairAmplitude i
 241        stretchFactor := pairStretchFactor i
 242        amplitude_pos := pairAmplitude_pos i
 243        stretchFactor_pos := pairStretchFactor_pos i }) ≤
 244      - totalViscous contributions
 245

papers checked against this theorem

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