pith. machine review for the scientific record. sign in
structure definition def or abbrev

IncompressibleNSOperator

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Definition body.

 241        stretchFactor := pairStretchFactor i
 242        amplitude_pos := pairAmplitude_pos i
 243        stretchFactor_pos := pairStretchFactor_pos i }) ≤
 244      - totalViscous contributions
 245
 246/-- Construct the legacy operator from a core operator. -/
 247def IncompressibleNSOperator.ofCore {siteCount : ℕ}
 248    (op : CoreNSOperator siteCount) : IncompressibleNSOperator siteCount where
 249  toEvolutionIdentity := op.toEvolutionIdentity
 250  topology := op.topology
 251  h := op.h
 252  ν := op.ν
 253  h_pos := op.h_pos
 254  ν_pos := op.ν_pos
 255  state := op.state
 256  velocity := op.velocity
 257  divergence_free := op.divergence_free
 258  transportFlux := op.transportFlux
 259  transportPerm := op.transportPerm
 260  transport_def := op.transport_def
 261  viscous_def := op.viscous_def
 262  pairAmplitude := corePairAmplitude op
 263  pairStretchFactor := corePairStretchFactor op
 264  pairAmplitude_pos := corePairAmplitude_pos op
 265  pairStretchFactor_pos := corePairStretchFactor_pos op
 266  stretching_le_pair_budget := core_stretching_le_pair_budget op
 267  pair_budget_absorbed_by_viscosity := op.viscous_absorbs
 268
 269/-- The concrete RCL pair event attached to a lattice site. -/

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (24)

Lean names referenced from this declaration's body.