Concrete fields and residuals for the correction construction

The state stores fields, rather than a residual-solving operator. Covariances are actual angular integrals, and the mean residuals are the differential expressions in MeanIncrementBounds. The three sorts of excluded additive errors are retained as fields on the same space as the oscillations.

@[reducible, inline]

abbrev NavierStokes.CorrectionState.ScalarField (D : Type) : Type

Scalar field: an abbreviation for MeanIncrementBounds.Field D.

Equations

• NavierStokes.CorrectionState.ScalarField D = NavierStokes.MeanIncrementBounds.Field D

@[reducible, inline]

abbrev NavierStokes.CorrectionState.Oscillation (D : Type) : Type

Oscillation: an abbreviation for ℕ → (D × ℝ) → Fin 3 → ℝ.

Equations

• NavierStokes.CorrectionState.Oscillation D = (ℕ → D × ℝ → Fin 3 → ℝ)

@[reducible, inline]

abbrev NavierStokes.CorrectionState.OscillatoryScalar (D : Type) : Type

Oscillatory scalar: an abbreviation for ℕ → (D × ℝ) → ℝ.

Equations

• NavierStokes.CorrectionState.OscillatoryScalar D = (ℕ → D × ℝ → ℝ)

@[reducible, inline]

abbrev NavierStokes.CorrectionState.MeanVector (D : Type) : Type

Mean vector: an abbreviation for ℕ → D → Fin 3 → ℝ.

Equations

• NavierStokes.CorrectionState.MeanVector D = (ℕ → D → Fin 3 → ℝ)

structure NavierStokes.CorrectionState.Context (D : Type) : Type

Fixed data used by every correction stage.

• operators : MeanIncrementBounds.Operators D

  Operators of Context, of type Operators D.

• base : MeanIncrementBounds.Triple D

  Base of Context, of type Triple D.

• virtualTheta : ScalarField D

  Virtual theta of Context, of type ScalarField D.

• virtualAxial : ScalarField D

  Virtual axial of Context, of type ScalarField D.

structure NavierStokes.CorrectionState.ExcludedErrors (D : Type) : Type

Additive errors are fields, not an exemption from the residual identity.

• base : Oscillation D

  Base of ExcludedErrors, of type Oscillation D.

• gaussian : Oscillation D

  Gaussian of ExcludedErrors, of type Oscillation D.

• aliasError : Oscillation D

  Alias error of ExcludedErrors, of type Oscillation D.

noncomputable def NavierStokes.CorrectionState.ExcludedErrors.zero {D : Type} : ExcludedErrors D

Zero, given by ⟨0, 0, 0⟩.

Equations

• NavierStokes.CorrectionState.ExcludedErrors.zero = { base := 0, gaussian := 0, aliasError := 0 }

noncomputable def NavierStokes.CorrectionState.ExcludedErrors.total {D : Type} (e : ExcludedErrors D) : Oscillation D

Total, given by e.base + e.gaussian + e.aliasError.

Equations

• e.total = e.base + e.gaussian + e.aliasError

noncomputable def NavierStokes.CorrectionState.ExcludedErrors.add {D : Type} (e f : ExcludedErrors D) : ExcludedErrors D

Add, given by ⟨e.base + f.base, e.gaussian + f.gaussian, e.aliasError + f.aliasError⟩.

Equations

• e.add f = { base := e.base + f.base, gaussian := e.gaussian + f.gaussian, aliasError := e.aliasError + f.aliasError }

@[simp]

theorem NavierStokes.CorrectionState.ExcludedErrors.total_zero {D : Type} : zero.total = 0

theorem NavierStokes.CorrectionState.ExcludedErrors.total_add {D : Type} (e f : ExcludedErrors D) : (e.add f).total = e.total + f.total

structure NavierStokes.CorrectionState.State (D : Type) : Type

An actual velocity/pressure state on a lifted chart and angular circle.

• mean : MeanIncrementBounds.Triple D

  Mean field of State, of type Triple D.

• pressure : ScalarField D

  Pressure field of State, of type ScalarField D.

• oscillation : Oscillation D

  Oscillation of State, of type Oscillation D.

• oscillatoryPressure : OscillatoryScalar D

  Oscillatory pressure of State, of type OscillatoryScalar D.

• errors : ExcludedErrors D

  Errors of State, of type ExcludedErrors D.

noncomputable def NavierStokes.CorrectionState.angularAverage {D : Type} (f : OscillatoryScalar D) : ScalarField D

The angular normalization agrees with the physical mean over one period.

Equations

• NavierStokes.CorrectionState.angularAverage f n x = (∫ (θ : ℝ) in 0..2 * Real.pi, f n (x, θ)) / (2 * Real.pi)

noncomputable def NavierStokes.CorrectionState.bilinearCovariance {D : Type} (u v : Oscillation D) (i j : Fin 3) : ScalarField D

Bilinear covariance, given by angularAverage (fun n p => u n p i * v n p j).

Equations

• NavierStokes.CorrectionState.bilinearCovariance u v i j = NavierStokes.CorrectionState.angularAverage fun (n : ℕ) (p : D × ℝ) => u n p i * v n p j

theorem NavierStokes.CorrectionState.angularAverage_axisymmetric {D : Type} (f : ScalarField D) : (angularAverage fun (n : ℕ) (p : D × ℝ) => f n p.1) = f

@[simp]

theorem NavierStokes.CorrectionState.angularAverage_zero {D : Type} : angularAverage 0 = 0

theorem NavierStokes.CorrectionState.bilinearCovariance_comm {D : Type} (u v : Oscillation D) (i j : Fin 3) : bilinearCovariance u v i j = bilinearCovariance v u j i

noncomputable def NavierStokes.CorrectionState.State.covariance {D : Type} (s : State D) (i j : Fin 3) : ScalarField D

Covariance, given by bilinearCovariance s.oscillation s.oscillation i j.

Equations

• s.covariance i j = NavierStokes.CorrectionState.bilinearCovariance s.oscillation s.oscillation i j

noncomputable def NavierStokes.CorrectionState.State.totalVelocity {D : Type} (s : State D) (c : Context D) : Oscillation D

Total velocity as an element of Oscillation D.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.State.totalPressureIncrement {D : Type} (s : State D) : OscillatoryScalar D

This is the pressure increment; the fixed base pressure is not part of a stage.

Equations

• s.totalPressureIncrement n p = s.pressure n p.1 + s.oscillatoryPressure n p

noncomputable def NavierStokes.CorrectionState.State.thetaResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : ScalarField D

Theta residual, given by MeanIncrementBounds.thetaResidual c.operators c.base s.mean s.covariance c.virtualTheta.

Equations

• s.thetaResidual c = NavierStokes.MeanIncrementBounds.thetaResidual c.operators c.base s.mean s.covariance c.virtualTheta

noncomputable def NavierStokes.CorrectionState.State.axialResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : ScalarField D

Axial residual, given by MeanIncrementBounds.axialResidual c.operators c.base s.mean s.covariance s.pressure c.virtualAxial.

Equations

• s.axialResidual c = NavierStokes.MeanIncrementBounds.axialResidual c.operators c.base s.mean s.covariance s.pressure c.virtualAxial

noncomputable def NavierStokes.CorrectionState.State.gr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : ScalarField D

Gr, given by MeanIncrementBounds.gr c.operators c.base s.mean s.covariance.

Equations

• s.gr c = NavierStokes.MeanIncrementBounds.gr c.operators c.base s.mean s.covariance

noncomputable def NavierStokes.CorrectionState.State.radialResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : ScalarField D

Radial residual, given by c.operators.dr s.pressure - s.gr c.

Equations

• s.radialResidual c = c.operators.dr s.pressure - s.gr c

noncomputable def NavierStokes.CorrectionState.State.reducedMeanResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : MeanVector D

Reduced mean residual, defined pointwise by ![s.radialResidual c n x, s.thetaResidual c n x, s.axialResidual c n x].

Equations

• s.reducedMeanResidual c n x = ![s.radialResidual c n x, s.thetaResidual c n x, s.axialResidual c n x]

noncomputable def NavierStokes.CorrectionState.State.meanBaseError {D : Type} (s : State D) : MeanVector D

Mean base error, defined pointwise by angularAverage (fun k p => s.errors.base k p i) n x.

Equations

• s.meanBaseError n x i = NavierStokes.CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => s.errors.base k p i) n x

noncomputable def NavierStokes.CorrectionState.State.meanResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : MeanVector D

Equation (32) omits the fixed base-flat error from (24); it is restored here.

Equations

• s.meanResidual c = s.reducedMeanResidual c + s.meanBaseError

noncomputable def NavierStokes.CorrectionState.State.meanExcluded {D : Type} (s : State D) : MeanVector D

Mean excluded, defined pointwise by angularAverage (fun k p => s.errors.total k p i) n x.

Equations

• s.meanExcluded n x i = NavierStokes.CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => s.errors.total k p i) n x

noncomputable def NavierStokes.CorrectionState.State.meanGoodResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : MeanVector D

Only the actual mean of the explicitly stored errors is removed here.

Equations

• s.meanGoodResidual c = s.meanResidual c - s.meanExcluded

theorem NavierStokes.CorrectionState.State.meanResidual_eq_good_add_excluded {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : State D) (c : Context D) : s.meanResidual c = s.meanGoodResidual c + s.meanExcluded

theorem NavierStokes.CorrectionState.State.covariance_symm {D : Type} (s : State D) (i j : Fin 3) : s.covariance i j = s.covariance j i

noncomputable def NavierStokes.CorrectionState.State.addIncrement {D : Type} (s : State D) (m : MeanIncrementBounds.Triple D) (p : ScalarField D) (u : Oscillation D) (q : OscillatoryScalar D) (e : ExcludedErrors D) : State D

Addition of actual fields. No estimate or cancellation is part of this definition.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CorrectionState.State.totalVelocity_addIncrement {D : Type} (s : State D) (c : Context D) (m : MeanIncrementBounds.Triple D) (p : ScalarField D) (u : Oscillation D) (q : OscillatoryScalar D) (e : ExcludedErrors D) : (s.addIncrement m p u q e).totalVelocity c = fun (n : ℕ) (x : D × ℝ) => s.totalVelocity c n x + ![m.radial n x.1, m.angular n x.1, m.axial n x.1] + u n x

structure NavierStokes.CorrectionState.HarmonicBlock (D : Type) : Type

A single grouped label. The finite group algebra records actual harmonics.

• velocity : ℕ → Fin 3 → HarmonicFields.Coefficients D

  Velocity field of HarmonicBlock, of type ℕ → Fin 3 → HarmonicFields.Coefficients D.

• pressure : ℕ → HarmonicFields.Coefficients D

  Pressure field of HarmonicBlock, of type ℕ → HarmonicFields.Coefficients D.

• frequency : ℕ → ℝ

  Frequency of HarmonicBlock, of type ℕ → ℝ.

• phase : ℕ → D → ℝ

  Phase of HarmonicBlock, of type ℕ → D → ℝ.

• angularFrequency : ℕ → ℤ

  Angular frequency of HarmonicBlock, of type ℕ → ℤ.

noncomputable def NavierStokes.CorrectionState.HarmonicBlock.oscillation {D : Type} (b : HarmonicBlock D) : Oscillation D

Oscillation, defined pointwise by (HarmonicFields.field (b.velocity n i) (b.frequency n) (b.phase n) (b.angularFrequency n) p).re.

Equations

• b.oscillation n p i = (NavierStokes.HarmonicFields.field (b.velocity n i) (b.frequency n) (b.phase n) (b.angularFrequency n) p).re

noncomputable def NavierStokes.CorrectionState.HarmonicBlock.oscillatoryPressure {D : Type} (b : HarmonicBlock D) : OscillatoryScalar D

Oscillatory pressure, defined pointwise by (HarmonicFields.field (b.pressure n) (b.frequency n) (b.phase n) (b.angularFrequency n) p).re.

Equations

• b.oscillatoryPressure n p = (NavierStokes.HarmonicFields.field (b.pressure n) (b.frequency n) (b.phase n) (b.angularFrequency n) p).re

def NavierStokes.CorrectionState.HarmonicBlock.BandLimited {D : Type} (b : HarmonicBlock D) (N : ℕ) : Prop

Band limited, given by (∀ n i, HarmonicFields.BandLimited (b.velocity n i) N) ∧ ∀ n, HarmonicFields.BandLimited (b.pressure n) N.

Equations

• b.BandLimited N = ((∀ (n : ℕ) (i : Fin 3), NavierStokes.HarmonicFields.BandLimited (b.velocity n i) N) ∧ ∀ (n : ℕ), NavierStokes.HarmonicFields.BandLimited (b.pressure n) N)

def NavierStokes.CorrectionState.HarmonicBlock.WaveBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (P : ℕ → D → ℝ) (α : ℝ) (b : HarmonicBlock D) : Prop

Bounds are on stripped, grouped, nonzero harmonic coefficients.

Equations

• NavierStokes.CorrectionState.HarmonicBlock.WaveBounds s P α b = ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → NavierStokes.WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (b.velocity n i).coeff j x

def NavierStokes.CorrectionState.HarmonicBlock.PressureBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (P : ℕ → D → ℝ) (α : ℝ) (b : HarmonicBlock D) : Prop

Pressure bounds, given by ∀ j : ℤ, j ≠ 0 → WaveClass s P α (fun n x => b.pressure n j x).

Equations

• NavierStokes.CorrectionState.HarmonicBlock.PressureBounds s P α b = ∀ (j : ℤ), j ≠ 0 → NavierStokes.WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (b.pressure n).coeff j x

def NavierStokes.CorrectionState.Represents {D ι : Type} (labels : Finset ι) (blocks : ι → HarmonicBlock D) (s : State D) : Prop

A representation on a finite set of labels active in a fixed chart. Global local-finiteness is a separate property of the physical label assembly.

Equations

• NavierStokes.CorrectionState.Represents labels blocks s = (s.oscillation = ∑ l ∈ labels, (blocks l).oscillation ∧ s.oscillatoryPressure = ∑ l ∈ labels, (blocks l).oscillatoryPressure)

structure NavierStokes.CorrectionState.CumulativeBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (u : State D) : Prop

The mean portion of the cumulative bounds after initialization.

• velocity : MeanIncrementBounds.CumulativeBounds s u.mean
• pressure : WeightedClasses.MeanClass s (9 / 10) u.pressure

structure NavierStokes.CorrectionState.MeanResidualBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (σ : ℝ) (c : Context D) (u : State D) : Prop

The mean residual portion of (36), computed from the state fields.

• angular : WeightedClasses.MeanClass s (1 + σ) fun (n : ℕ) (x : D) => u.meanGoodResidual c n x 1
• axial : WeightedClasses.MeanClass s (1 + σ) fun (n : ℕ) (x : D) => u.meanGoodResidual c n x 2

noncomputable def NavierStokes.CorrectionState.radialMoment {S : Type} (k : ℕ) (f : ScalarField (PressureStream.Lift S)) : ScalarField S

Actual radial moment of the full auxiliary torus mean.

Equations

• NavierStokes.CorrectionState.radialMoment k f n p = NavierStokes.PressureStream.pressureMass (fun (x : NavierStokes.PressureStream.Lift S) => x.1 ^ k * f n x) p

noncomputable def NavierStokes.CorrectionState.pressureDefect {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : Context (PressureStream.Lift S)) (u : State (PressureStream.Lift S)) : ScalarField S

Pressure defect, given by radialMoment 0 (u.gr c).

Equations

• NavierStokes.CorrectionState.pressureDefect c u = NavierStokes.CorrectionState.radialMoment 0 (u.gr c)

noncomputable def NavierStokes.CorrectionState.thetaDefect {S : Type} (c : Context (PressureStream.Lift S)) (u : State (PressureStream.Lift S)) : ScalarField S

Theta defect, given by radialMoment 2 (thetaAxial c.base u.mean + u.covariance 2 1).

Equations

• NavierStokes.CorrectionState.thetaDefect c u = NavierStokes.CorrectionState.radialMoment 2 (NavierStokes.MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1)

noncomputable def NavierStokes.CorrectionState.axialDefect {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : Context (PressureStream.Lift S)) (u : State (PressureStream.Lift S)) : ScalarField S

Axial defect, given by radialMoment 1 (axialAxial c.base u.mean + u.covariance 2 2) - (1 / 2 : ℝ) • radialMoment 2 (u.gr c).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.debt {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : Context (PressureStream.Lift S)) (u : State (PressureStream.Lift S)) : ℕ → S → Fin 3 → ℝ

The row order is exactly (P, Jθ, Jz), as in MeanRankUpdate.

Equations

• One or more equations did not get rendered due to their size.

def NavierStokes.CorrectionState.DefectBounds {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (s : WeightedClasses.StripData S) (σ : ℝ) (c : Context (PressureStream.Lift S)) (u : State (PressureStream.Lift S)) : Prop

Defect bounds, given by ∀ i : Fin 3, UnweightedClass s (1 + σ) (fun n x => debt c u n x i).

Equations

• One or more equations did not get rendered due to their size.

def NavierStokes.CorrectionState.ZeroMasses {S : Type} (u : State (PressureStream.Lift S)) : Prop

Zero masses, given by radialMoment 2 u.mean.angular = 0 ∧ radialMoment 1 u.mean.axial = 0.

Equations

• NavierStokes.CorrectionState.ZeroMasses u = (NavierStokes.CorrectionState.radialMoment 2 u.mean.angular = 0 ∧ NavierStokes.CorrectionState.radialMoment 1 u.mean.axial = 0)

structure NavierStokes.CorrectionState.ReconstructionData : Type

Geometry of the genuine compact shifted pressure/stream primitive.

• exponent : ℝ

  Exponent of ReconstructionData, of type ℝ.

• inner : ℝ

  Inner of ReconstructionData, of type ℝ.

• outer : ℝ

  Outer of ReconstructionData, of type ℝ.

• inner_lt_outer : self.inner < self.outer
• frequency : ℕ → ℝ

  Frequency of ReconstructionData, of type ℕ → ℝ.

• radialDirection : PressureStream.Plane

  Radial direction of ReconstructionData, of type PressureStream.Plane.

@[reducible, inline]

abbrev NavierStokes.CorrectionState.Lift (S : Type) : Type

Lift: an abbreviation for PressureStream.Lift S.

Equations

• NavierStokes.CorrectionState.Lift S = NavierStokes.PressureStream.Lift S

noncomputable def NavierStokes.CorrectionState.reconstructPressure {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (c : Context (Lift S)) (u : State (Lift S)) : State (Lift S)

Recompute (33) from the current actual radial source.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.pressureAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (c : Context (Lift S)) (u : State (Lift S)) : Oscillation (Lift S)

The pressure alias has the sign with which it occurs in the radial residual.

Equations

• NavierStokes.CorrectionState.pressureAlias r c u n p = ![-NavierStokes.PressureStream.pressureAlias r.exponent r.inner r.outer (r.frequency n) ⋯ r.radialDirection (u.gr c n) p.1, 0, 0]

@[simp]

theorem NavierStokes.CorrectionState.reconstructPressure_gr {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (c : Context (Lift S)) (u : State (Lift S)) : (reconstructPressure r c u).gr c = u.gr c

@[simp]

theorem NavierStokes.CorrectionState.reconstructPressure_covariance {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (c : Context (Lift S)) (u : State (Lift S)) : (reconstructPressure r c u).covariance = u.covariance

noncomputable def NavierStokes.CorrectionState.graphOperators {S : Type} [NormedAddCommGroup S] (r : ReconstructionData) (epsilon fast : ℕ → ℝ) (axial slowTime : S × PressureStream.Plane) (temporal : PressureStream.Plane) : MeanIncrementBounds.Operators (Lift S)

Explicit graph operators with the pressure primitive's radial direction.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CorrectionState.graphOperators_dr {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (epsilon fast : ℕ → ℝ) (axial slowTime : S × PressureStream.Plane) (temporal : PressureStream.Plane) (f : ScalarField (Lift S)) (n : ℕ) (x : Lift S) : (graphOperators r epsilon fast axial slowTime temporal).dr f n x = PressureStream.graphDr (PressureStream.physicalSpeed r.exponent (r.frequency n)) (0, r.radialDirection) (f n) x

theorem NavierStokes.CorrectionState.graphOperators_dz {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (epsilon fast : ℕ → ℝ) (axial slowTime : S × PressureStream.Plane) (temporal : PressureStream.Plane) (f : ScalarField (Lift S)) (n : ℕ) (x : Lift S) : (graphOperators r epsilon fast axial slowTime temporal).dz f n x = PressureStream.graphDz (epsilon n • axial) (f n) x

theorem NavierStokes.CorrectionState.graphOperators_fastTime {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (epsilon : ℕ → ℝ) (h : ℝ) (axial slowTime : S × PressureStream.Plane) (f : ScalarField (Lift S)) (n : ℕ) (x : Lift S) : (graphOperators r epsilon (ChartScales.timeCoefficient h) axial slowTime (TorusInverse.vector TorusInverse.Direction.temporal)).fastTime f n x = TemporalMeanUpdate.fastDerivative h n (f n) x

theorem NavierStokes.CorrectionState.reconstructed_radial_residual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) (c : Context (Lift S)) (u : State (Lift S)) (hoperator : ∀ (f : ScalarField (Lift S)) (n : ℕ) (x : Lift S), c.operators.dr f n x = PressureStream.graphDr (PressureStream.physicalSpeed r.exponent (r.frequency n)) (0, r.radialDirection) (f n) x) (hsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u.gr c n)) (hsupport : ∀ (n : ℕ), RadialAlias.RadiallySupported r.inner r.outer (u.gr c n)) (n : ℕ) (x : Lift S) : (reconstructPressure r c u).radialResidual c n x = -PressureStream.rho r.inner r.outer ⋯ x.1 * pressureDefect c u n x.2.1 + pressureAlias r c u n (x, 0) 0

noncomputable def NavierStokes.CorrectionState.temporalIncrement {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (h : ℝ) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) : MeanIncrementBounds.Triple (Lift S)

The actual temporal increment, including the compactified axial stream.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.temporalAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (h : ℝ) (c : Context (Lift S)) (u : State (Lift S)) : Oscillation (Lift S)

The exact remaining axial fast-time error, not its asymptotic estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.temporalStage {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ReconstructionData) (h : ℝ) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) : State (Lift S)

Temporal stage, given by reconstructPressure r c (u.addIncrement (temporalIncrement r h axial c u) 0 0 0 ⟨0, 0, temporalAlias r h c u⟩).

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CorrectionState.temporal_fast_cancellation {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : ReconstructionData) (h : ℝ) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) (ha : 0 < r.inner) (hd : 0 < r.exponent) (hθ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u.thetaResidual c n)) (hz : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u.axialResidual c n)) (hpθ : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.thetaResidual c n)) (hpz : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.axialResidual c n)) (hsz : ∀ (n : ℕ), RadialAlias.RadiallySupported r.inner r.outer (u.axialResidual c n)) (n : ℕ) (x : Lift S) : TemporalMeanUpdate.fastDerivative h n ((temporalIncrement r h axial c u).angular n) x + TemporalMeanUpdate.centered (u.thetaResidual c n) x = 0 ∧ TemporalMeanUpdate.fastDerivative h n ((temporalIncrement r h axial c u).axial n) x + TemporalMeanUpdate.centered (u.axialResidual c n) x = temporalAlias r h c u n (x, 0) 2

structure NavierStokes.CorrectionState.RankData (S : Type) : Type

The physical length, velocity, and background amplitude used by the five-row inverse. These may depend on the band and slow variables.

• lambda : ℝ

  Lambda of RankData, of type ℝ.

• inner : ℝ

  Inner of RankData, of type ℝ.

• outer : ℝ

  Outer of RankData, of type ℝ.

• length : ℕ → S → ℝ

  Length of RankData, of type ℕ → S → ℝ.

• velocity : ℕ → S → ℝ

  Velocity field of RankData, of type ℕ → S → ℝ.

• coefficient : ℕ → S → ℝ

  Coefficient of RankData, of type ℕ → S → ℝ.

noncomputable def NavierStokes.CorrectionState.rankAngular {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : RankData S) (c : Context (Lift S)) (u : State (Lift S)) (n : ℕ) : ℝ × S → ℝ

Rank angular, given by MeanRankUpdate.angularFamily r.lambda r.inner r.outer (r.length n) (r.velocity n) (r.coefficient n) (debt c u n).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.rankDesiredAxial {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : RankData S) (c : Context (Lift S)) (u : State (Lift S)) (n : ℕ) : ℝ × S → ℝ

Rank desired axial, given by MeanRankUpdate.desiredAxialFamily r.lambda r.inner r.outer (r.length n) (r.velocity n) (r.coefficient n) (debt c u n).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.rankPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : ReconstructionData) (r : RankData S) (c : Context (Lift S)) (u : State (Lift S)) (n : ℕ) : Lift S → ℝ

Rank potential, constructed using PressureStream.streamPotential.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.rankIncrement {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : ReconstructionData) (r : RankData S) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) : MeanIncrementBounds.Triple (Lift S)

Rank increment, bundling radial, angular, axial.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.CorrectionState.rankStage {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : ReconstructionData) (r : RankData S) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) : State (Lift S)

Rank stage, given by reconstructPressure p c (u.addIncrement (rankIncrement p r axial c u) 0 0 0 ExcludedErrors.zero).

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CorrectionState.rank_model_rows {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : RankData S) (c : Context (Lift S)) (u : State (Lift S)) (n : ℕ) (x : S) (hlam : 0 < r.lambda) (hC : r.coefficient n x ≠ 0) (ha : 0 < r.inner) (hab : r.inner < r.outer) (hell : 0 < r.length n x) (hU : r.velocity n x ≠ 0) : FiveRowRank.FiveRows (MeanRankUpdate.background r.lambda (r.coefficient n x) (r.length n x) (r.velocity n x)) (fun (x : ℝ) => 0) (debt c u n x) (fun (R : ℝ) => rankAngular r c u n (R, x)) fun (R : ℝ) => rankDesiredAxial r c u n (R, x)

theorem NavierStokes.CorrectionState.rank_rows_on_patch {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : RankData S) (c : Context (Lift S)) (u : State (Lift S)) (n : ℕ) (x : S) (Y : PressureStream.Plane) (hlam : 0 < r.lambda) (hC : r.coefficient n x ≠ 0) (ha : 0 < r.inner) (hab : r.inner < r.outer) (hell : 0 < r.length n x) (hU : r.velocity n x ≠ 0) (hV : ∀ R ∈ Set.Ioo (r.length n x * r.inner) (r.length n x * r.outer), c.base.angular n (R, x, Y) = MeanRankUpdate.background r.lambda (r.coefficient n x) (r.length n x) (r.velocity n x) R) (hG : ∀ R ∈ Set.Ioo (r.length n x * r.inner) (r.length n x * r.outer), c.base.axial n (R, x, Y) = 0) : FiveRowRank.FiveRows (fun (R : ℝ) => c.base.angular n (R, x, Y)) (fun (R : ℝ) => c.base.axial n (R, x, Y)) (debt c u n x) (fun (R : ℝ) => rankAngular r c u n (R, x)) fun (R : ℝ) => rankDesiredAxial r c u n (R, x)

The linear rows hold for the actual base whenever it agrees with the prescribed background on the support of the constructed bumps.

theorem NavierStokes.CorrectionState.rank_axial_eq_desired {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : ReconstructionData) (r : RankData S) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) (ha : 0 < p.inner) (hd : 0 < p.exponent) (n : ℕ) (hlam : 0 < r.lambda) (hC : ∀ (x : S), r.coefficient n x ≠ 0) (hra : 0 < r.inner) (hrab : r.inner < r.outer) (hell : ∀ (x : S), 0 < r.length n x) (hU : ∀ (x : S), r.velocity n x ≠ 0) (hf : ContDiff ℝ (↑⊤) (rankDesiredAxial r c u n)) (hs : RadialAlias.RadiallySupported p.inner p.outer (rankDesiredAxial r c u n)) (x : Lift S) : (rankIncrement p r axial c u).axial n x = rankDesiredAxial r c u n (x.1, x.2.1)

theorem NavierStokes.CorrectionState.rank_divergence_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : ReconstructionData) (r : RankData S) (axial : S × PressureStream.Plane) (c : Context (Lift S)) (u : State (Lift S)) (ha : 0 < p.inner) (hd : 0 < p.exponent) (n : ℕ) (hf : ContDiff ℝ (↑⊤) (rankDesiredAxial r c u n)) (hs : RadialAlias.RadiallySupported p.inner p.outer (rankDesiredAxial r c u n)) (x : Lift S) : PressureStream.graphDivergence (PressureStream.physicalSpeed p.exponent (p.frequency n)) (0, p.radialDirection) (c.operators.epsilon n • axial) ((rankIncrement p r axial c u).radial n) ((rankIncrement p r axial c u).axial n) x = 0