Isometric reindexing of the actual correction state

Pullback along e : D ≃ₗᵢ[ℝ] E sends fields on E to fields on D. Vector directions are transported by e.symm. The final specialization is the existing associator from PressureStream.Lift S to ((ℝ × S) × Plane).

noncomputable def NavierStokes.StateReindex.cylinder {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) : D × ℝ ≃ₗᵢ[ℝ] E × ℝ

Cylinder, bundling toLinearEquiv, norm_map.

Equations

• NavierStokes.StateReindex.cylinder e = { toLinearEquiv := e.prodCongr (LinearEquiv.refl ℝ ℝ), norm_map' := ⋯ }

@[simp]

theorem NavierStokes.StateReindex.cylinder_apply {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (x : D × ℝ) : (cylinder e) x = (e x.1, x.2)

@[simp]

theorem NavierStokes.StateReindex.cylinder_symm_apply {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (x : E × ℝ) : (cylinder e).symm x = (e.symm x.1, x.2)

noncomputable def NavierStokes.StateReindex.vector {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (V : E → E) : D → D

Vector, given by ParticularWaveBounds.reindexVector e V.

Equations

• NavierStokes.StateReindex.vector e V = NavierStokes.ParticularWaveBounds.reindexVector e V

theorem NavierStokes.StateReindex.fderiv_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃ₗᵢ[ℝ] E) (f : E → F) (x v : D) : (fderiv ℝ (fun (y : D) => f (e y)) x) v = (fderiv ℝ f (e x)) (e v)

theorem NavierStokes.StateReindex.along_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃ₗᵢ[ℝ] E) (V : E → E) (f : E → F) : (HarmonicCalculus.along (vector e V) fun (x : D) => f (e x)) = fun (x : D) => HarmonicCalculus.along V f (e x)

theorem NavierStokes.StateReindex.along_pull_component {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_1} (e : D ≃ₗᵢ[ℝ] E) (V : E → E) (f : E → ι → F) (i : ι) : (HarmonicCalculus.along (vector e V) fun (x : D) => f (e x) i) = fun (x : D) => HarmonicCalculus.along V (fun (y : E) => f y i) (e x)

theorem NavierStokes.StateReindex.iteratedFDeriv_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃ₗᵢ[ℝ] E) (f : E → F) (m : ℕ) (x : D) : iteratedFDeriv ℝ m (fun (y : D) => f (e y)) x = (iteratedFDeriv ℝ m f (e x)).compContinuousLinearMap fun (x : Fin m) => ↑↑e

theorem NavierStokes.StateReindex.norm_iteratedFDeriv_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃ₗᵢ[ℝ] E) (f : E → F) (m : ℕ) (x : D) : ‖iteratedFDeriv ℝ m (fun (y : D) => f (e y)) x‖ = ‖iteratedFDeriv ℝ m f (e x)‖

noncomputable def NavierStokes.StateReindex.field {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (f : MeanIncrementBounds.Field E) : MeanIncrementBounds.Field D

Field, defined pointwise by f n (e x).

Equations

• NavierStokes.StateReindex.field e f n x = f n (e x)

noncomputable def NavierStokes.StateReindex.triple {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : MeanIncrementBounds.Triple E) : MeanIncrementBounds.Triple D

Triple, given by ⟨field e b.radial, field e b.angular, field e b.axial⟩.

Equations

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

noncomputable def NavierStokes.StateReindex.operators {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (o : MeanIncrementBounds.Operators E) : MeanIncrementBounds.Operators D

Operators, bundling epsilon, radialFrequency, fastCoefficient, radius and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.StateReindex.context {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) : CorrectionState.Context D

Context, bundling operators, base, virtualTheta, virtualAxial.

Equations

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

noncomputable def NavierStokes.StateReindex.oscillation {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.Oscillation E) : CorrectionState.Oscillation D

Oscillation, defined pointwise by u n (cylinder e x).

Equations

• NavierStokes.StateReindex.oscillation e u n x = u n ((NavierStokes.StateReindex.cylinder e) x)

noncomputable def NavierStokes.StateReindex.errors {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : CorrectionState.ExcludedErrors E) : CorrectionState.ExcludedErrors D

Errors, given by ⟨oscillation e a.base, oscillation e a.gaussian, oscillation e a.aliasError⟩.

Equations

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

noncomputable def NavierStokes.StateReindex.state {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State E) : CorrectionState.State D

State, bundling mean, pressure, oscillation, oscillatoryPressure and the required compatibility proofs.

Equations

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

theorem NavierStokes.StateReindex.fderiv_field {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (f : MeanIncrementBounds.Field E) (n : ℕ) (x : D) (v : E) : (fderiv ℝ (field e f n) x) (e.symm v) = (fderiv ℝ (f n) (e x)) v

theorem NavierStokes.StateReindex.dr_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (o : MeanIncrementBounds.Operators E) (f : MeanIncrementBounds.Field E) : (operators e o).dr (field e f) = field e (o.dr f)

theorem NavierStokes.StateReindex.dz_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (o : MeanIncrementBounds.Operators E) (f : MeanIncrementBounds.Field E) : (operators e o).dz (field e f) = field e (o.dz f)

theorem NavierStokes.StateReindex.time_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (o : MeanIncrementBounds.Operators E) (f : MeanIncrementBounds.Field E) : (operators e o).time (field e f) = field e (o.time f)

theorem NavierStokes.StateReindex.radialDiv_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (o : MeanIncrementBounds.Operators E) (k : ℝ) (f : MeanIncrementBounds.Field E) : (operators e o).radialDiv k (field e f) = field e (o.radialDiv k f)

theorem NavierStokes.StateReindex.viscosity_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (o : MeanIncrementBounds.Operators E) (k : ℝ) (f : MeanIncrementBounds.Field E) : (operators e o).viscosity k (field e f) = field e (o.viscosity k f)

theorem NavierStokes.StateReindex.angularAverage_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (f : CorrectionState.OscillatoryScalar E) : (CorrectionState.angularAverage fun (n : ℕ) (x : D × ℝ) => f n ((cylinder e) x)) = field e (CorrectionState.angularAverage f)

theorem NavierStokes.StateReindex.covariance_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State E) (i j : Fin 3) : (state e u).covariance i j = field e (u.covariance i j)

theorem NavierStokes.StateReindex.totalErrors_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : CorrectionState.ExcludedErrors E) : (errors e a).total = oscillation e a.total

theorem NavierStokes.StateReindex.totalVelocity_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) : (state e u).totalVelocity (context e c) = oscillation e (u.totalVelocity c)

theorem NavierStokes.StateReindex.totalPressure_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State E) : (state e u).totalPressureIncrement = fun (n : ℕ) (x : D × ℝ) => u.totalPressureIncrement n ((cylinder e) x)

Finite harmonic coefficients

noncomputable def NavierStokes.StateReindex.coefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) : HarmonicFields.Coefficients D

Coefficients, given by AddMonoidAlgebra.ofCoeff (Finsupp.mapRange (fun f : E → ℂ => fun x => f (e x)) rfl a.coeff).

Equations

• NavierStokes.StateReindex.coefficients e a = AddMonoidAlgebra.ofCoeff (Finsupp.mapRange (fun (f : E → ℂ) (x : D) => f (e x)) ⋯ a.coeff)

@[simp]

theorem NavierStokes.StateReindex.coefficients_apply {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) (j : ℤ) (x : D) : (coefficients e a).coeff j x = a.coeff j (e x)

theorem NavierStokes.StateReindex.coefficients_fun {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) (j : ℤ) : (coefficients e a).coeff j = fun (x : D) => a.coeff j (e x)

theorem NavierStokes.StateReindex.coefficients_support {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) : (coefficients e a).support = a.support

@[simp]

theorem NavierStokes.StateReindex.coefficients_zero {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) : coefficients e 0 = 0

theorem NavierStokes.StateReindex.coefficients_add {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a b : HarmonicFields.Coefficients E) : coefficients e (a + b) = coefficients e a + coefficients e b

theorem NavierStokes.StateReindex.coefficients_sub {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a b : HarmonicFields.Coefficients E) : coefficients e (a - b) = coefficients e a - coefficients e b

theorem NavierStokes.StateReindex.coefficients_neg {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) : coefficients e (-a) = -coefficients e a

theorem NavierStokes.StateReindex.coefficients_mul {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a b : HarmonicFields.Coefficients E) : coefficients e (a * b) = coefficients e a * coefficients e b

theorem NavierStokes.StateReindex.coefficients_constant {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : E → ℂ) : coefficients e (HarmonicFields.constantCoefficient a) = HarmonicFields.constantCoefficient fun (x : D) => a (e x)

theorem NavierStokes.StateReindex.evaluate_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) (x : D) (theta : ℝ) : HarmonicFields.evaluate (coefficients e a) x theta = HarmonicFields.evaluate a (e x) theta

theorem NavierStokes.StateReindex.harmonicField_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (x : D × ℝ) : HarmonicFields.field (coefficients e a) k (fun (y : D) => Phi (e y)) kp x = HarmonicFields.field a k Phi kp ((cylinder e) x)

theorem NavierStokes.StateReindex.coefficientMass_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) (x : D) : HarmonicFields.coefficientMass (coefficients e a) x = HarmonicFields.coefficientMass a (e x)

theorem NavierStokes.StateReindex.bandLimited_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {a : HarmonicFields.Coefficients E} {N : ℕ} (ha : HarmonicFields.BandLimited a N) : HarmonicFields.BandLimited (coefficients e a) N

theorem NavierStokes.StateReindex.differentiate_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (V : E → E) (k : ℝ) (Phi : E → ℝ) (a : HarmonicFields.Coefficients E) : HarmonicFields.differentiate (vector e V) k (fun (x : D) => Phi (e x)) (coefficients e a) = coefficients e (HarmonicFields.differentiate V k Phi a)

theorem NavierStokes.StateReindex.angularDifferentiate_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (kp : ℤ) (a : HarmonicFields.Coefficients E) : HarmonicFields.angularDifferentiate kp (coefficients e a) = coefficients e (HarmonicFields.angularDifferentiate kp a)

theorem NavierStokes.StateReindex.realCoefficients_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) : HarmonicResidual.realCoefficients (coefficients e a) = coefficients e (HarmonicResidual.realCoefficients a)

theorem NavierStokes.StateReindex.nonconstant_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients E) : HarmonicResidual.nonconstant (coefficients e a) = coefficients e (HarmonicResidual.nonconstant a)

noncomputable def NavierStokes.StateReindex.block {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock E) : CorrectionState.HarmonicBlock D

Block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.StateReindex.blockCoefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicResidual.BlockCoefficients E) : HarmonicResidual.BlockCoefficients D

Block coefficients, defined pointwise by coefficients e (a n i).

Equations

• NavierStokes.StateReindex.blockCoefficients e a n i = NavierStokes.StateReindex.coefficients e (a n i)

theorem NavierStokes.StateReindex.block_oscillation {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock E) : (block e b).oscillation = oscillation e b.oscillation

theorem NavierStokes.StateReindex.block_pressure {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock E) : (block e b).oscillatoryPressure = fun (n : ℕ) (x : D × ℝ) => b.oscillatoryPressure n ((cylinder e) x)

The actual coefficient residual

noncomputable def NavierStokes.StateReindex.frame {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) : HarmonicResidual.Frame D

Frame, bundling radius, radial, axial, time and the required compatibility proofs.

Equations

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

theorem NavierStokes.StateReindex.rotate_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicResidual.VectorCoefficients E) : (HarmonicResidual.rotate fun (i : Fin 3) => coefficients e (a i)) = fun (i : Fin 3) => coefficients e (HarmonicResidual.rotate a i)

theorem NavierStokes.StateReindex.scalarLaplacian_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (a : HarmonicFields.Coefficients E) : HarmonicResidual.scalarLaplacian (frame e g) k (fun (x : D) => Phi (e x)) kp (coefficients e a) = coefficients e (HarmonicResidual.scalarLaplacian g k Phi kp a)

theorem NavierStokes.StateReindex.vectorLaplacian_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (a : HarmonicResidual.VectorCoefficients E) : (HarmonicResidual.vectorLaplacian (frame e g) k (fun (x : D) => Phi (e x)) kp fun (i : Fin 3) => coefficients e (a i)) = fun (i : Fin 3) => coefficients e (HarmonicResidual.vectorLaplacian g k Phi kp a i)

theorem NavierStokes.StateReindex.transportCoefficients_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (a b : HarmonicResidual.VectorCoefficients E) : (HarmonicResidual.transport (frame e g) k (fun (x : D) => Phi (e x)) kp (fun (i : Fin 3) => coefficients e (a i)) fun (i : Fin 3) => coefficients e (b i)) = fun (i : Fin 3) => coefficients e (HarmonicResidual.transport g k Phi kp a b i)

theorem NavierStokes.StateReindex.gradientCoefficients_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (a : HarmonicFields.Coefficients E) : HarmonicResidual.gradient (frame e g) k (fun (x : D) => Phi (e x)) kp (coefficients e a) = fun (i : Fin 3) => coefficients e (HarmonicResidual.gradient g k Phi kp a i)

theorem NavierStokes.StateReindex.linearCoefficients_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (B a : HarmonicResidual.VectorCoefficients E) (p : HarmonicFields.Coefficients E) : HarmonicResidual.linearResidual (frame e g) k (fun (x : D) => Phi (e x)) kp (fun (i : Fin 3) => coefficients e (B i)) (fun (i : Fin 3) => coefficients e (a i)) (coefficients e p) = fun (i : Fin 3) => coefficients e (HarmonicResidual.linearResidual g k Phi kp B a p i)

theorem NavierStokes.StateReindex.nonlinearCoefficients_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (g : HarmonicResidual.Frame E) (k : ℝ) (Phi : E → ℝ) (kp : ℤ) (B a : HarmonicResidual.VectorCoefficients E) (p : HarmonicFields.Coefficients E) : HarmonicResidual.nonlinearResidual (frame e g) k (fun (x : D) => Phi (e x)) kp (fun (i : Fin 3) => coefficients e (B i)) (fun (i : Fin 3) => coefficients e (a i)) (coefficients e p) = fun (i : Fin 3) => coefficients e (HarmonicResidual.nonlinearResidual g k Phi kp B a p i)

theorem NavierStokes.StateReindex.constantVector_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (B : E → HarmonicCalculus.ComplexVector) : (HarmonicResidual.constantVector fun (x : D) => B (e x)) = fun (i : Fin 3) => coefficients e (HarmonicResidual.constantVector B i)

noncomputable def NavierStokes.StateReindex.label {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (d : HarmonicResidual.LabelData E) : HarmonicResidual.LabelData D

Label, bundling frequency, phase, angularFrequency, velocity and the required compatibility proofs.

Equations

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

theorem NavierStokes.StateReindex.labelResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (d : HarmonicResidual.LabelData E) (g : HarmonicResidual.Frame E) (B M : E → HarmonicCalculus.ComplexVector) : ((label e d).residualCoefficients (frame e g) (fun (x : D) => B (e x)) fun (x : D) => M (e x)) = fun (i : Fin 3) => coefficients e (d.residualCoefficients g B M i)

theorem NavierStokes.StateReindex.labelWaveResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (d : HarmonicResidual.LabelData E) (g : HarmonicResidual.Frame E) (B M : E → HarmonicCalculus.ComplexVector) : ((label e d).waveResidualCoefficients (frame e g) (fun (x : D) => B (e x)) fun (x : D) => M (e x)) = fun (i : Fin 3) => coefficients e (d.waveResidualCoefficients g B M i)

theorem NavierStokes.StateReindex.contextFrame_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : HarmonicResidual.contextFrame (context e c) n = frame e (HarmonicResidual.contextFrame c n)

theorem NavierStokes.StateReindex.contextBase_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : HarmonicResidual.contextBase (context e c) n = fun (x : D) => HarmonicResidual.contextBase c n (e x)

theorem NavierStokes.StateReindex.stateMean_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State E) (n : ℕ) : HarmonicResidual.stateMean (state e u) n = fun (x : D) => HarmonicResidual.stateMean u n (e x)

theorem NavierStokes.StateReindex.ofBlock_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock E) (G A : HarmonicResidual.BlockCoefficients E) (n : ℕ) : HarmonicResidual.ofBlock (block e b) (blockCoefficients e G) (blockCoefficients e A) n = label e (HarmonicResidual.ofBlock b G A n)

theorem NavierStokes.StateReindex.residualBlock_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (b : CorrectionState.HarmonicBlock E) (G A : HarmonicResidual.BlockCoefficients E) : HarmonicResidual.residualBlock (context e c) (state e u) (block e b) (blockCoefficients e G) (blockCoefficients e A) = block e (HarmonicResidual.residualBlock c u b G A)

Exact reindexing of the stripped nonzero coefficients of the actual current-state residual, including Gaussian and alias subtraction.

The full differential residual

theorem NavierStokes.StateReindex.scalarLaplacian_field_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vt Vz : E → E) (f : E → F) (x : D) : HarmonicCalculus.cylindricalLaplacian (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (fun (y : D) => f (e y)) x = HarmonicCalculus.cylindricalLaplacian R Vr Vt Vz f (e x)

theorem NavierStokes.StateReindex.scalarLaplacian_component_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_1} (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vt Vz : E → E) (f : E → ι → F) (i : ι) (x : D) : HarmonicCalculus.cylindricalLaplacian (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (fun (y : D) => f (e y) i) x = HarmonicCalculus.cylindricalLaplacian R Vr Vt Vz (fun (y : E) => f y i) (e x)

theorem NavierStokes.StateReindex.transport_field_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vt Vz : E → E) (u v : E → HarmonicCalculus.ComplexVector) (x : D) : LinearWaveResidual.transport (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (fun (y : D) => u (e y)) (fun (y : D) => v (e y)) x = LinearWaveResidual.transport R Vr Vt Vz u v (e x)

theorem NavierStokes.StateReindex.vectorLaplacian_field_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vt Vz : E → E) (a : E → HarmonicCalculus.ComplexVector) (x : D) : HarmonicCalculus.cylindricalVectorLaplacian (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (fun (y : D) => a (e y)) x = HarmonicCalculus.cylindricalVectorLaplacian R Vr Vt Vz a (e x)

theorem NavierStokes.StateReindex.linearResidual_field_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (epsilon : ℝ) (R : E → ℝ) (Vr Vt Vz Vtime : E → E) (B a : E → HarmonicCalculus.ComplexVector) (p : E → ℂ) (x : D) : LinearWaveResidual.linearResidual epsilon (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (vector e Vtime) (fun (y : D) => B (e y)) (fun (y : D) => a (e y)) (fun (y : D) => p (e y)) x = LinearWaveResidual.linearResidual epsilon R Vr Vt Vz Vtime B a p (e x)

theorem NavierStokes.StateReindex.radialDirection_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : LiftedMeanResidual.radialDirection (context e c) n = vector (cylinder e) (LiftedMeanResidual.radialDirection c n)

theorem NavierStokes.StateReindex.axialDirection_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : LiftedMeanResidual.axialDirection (context e c) n = vector (cylinder e) (LiftedMeanResidual.axialDirection c n)

theorem NavierStokes.StateReindex.timeDirection_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : LiftedMeanResidual.timeDirection (context e c) n = vector (cylinder e) (LiftedMeanResidual.timeDirection c n)

theorem NavierStokes.StateReindex.angularDirection_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) : vector (cylinder e) LiftedMeanResidual.angularDirection = LiftedMeanResidual.angularDirection

theorem NavierStokes.StateReindex.complexBase_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : LiftedMeanResidual.complexBase (context e c) n = fun (x : D × ℝ) => LiftedMeanResidual.complexBase c n ((cylinder e) x)

theorem NavierStokes.StateReindex.complexPerturbation_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State E) (n : ℕ) : LiftedMeanResidual.complexPerturbation (state e u) n = fun (x : D × ℝ) => LiftedMeanResidual.complexPerturbation u n ((cylinder e) x)

theorem NavierStokes.StateReindex.complexPressure_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State E) (n : ℕ) : LiftedMeanResidual.complexPressure (state e u) n = fun (x : D × ℝ) => LiftedMeanResidual.complexPressure u n ((cylinder e) x)

theorem NavierStokes.StateReindex.virtualDivergence_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) (x : D × ℝ) : LiftedMeanResidual.virtualDivergence (context e c) n x = LiftedMeanResidual.virtualDivergence c n ((cylinder e) x)

theorem NavierStokes.StateReindex.fullResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (n : ℕ) (x : D × ℝ) (i : Fin 3) : LiftedMeanResidual.fullResidual (context e c) (state e u) n x i = LiftedMeanResidual.fullResidual c u n ((cylinder e) x) i

theorem NavierStokes.StateReindex.fullGoodResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (n : ℕ) (x : D × ℝ) (i : Fin 3) : LiftedMeanResidual.fullGoodResidual (context e c) (state e u) n x i = LiftedMeanResidual.fullGoodResidual c u n ((cylinder e) x) i

Exact return from the alternate layout

theorem NavierStokes.StateReindex.coefficients_roundtrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : HarmonicFields.Coefficients D) : coefficients e (coefficients e.symm a) = a

theorem NavierStokes.StateReindex.block_roundtrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock D) : block e (block e.symm b) = b

theorem NavierStokes.StateReindex.field_roundtrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (f : MeanIncrementBounds.Field D) : field e (field e.symm f) = f

theorem NavierStokes.StateReindex.oscillation_roundtrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (f : CorrectionState.Oscillation D) : oscillation e (oscillation e.symm f) = f

theorem NavierStokes.StateReindex.state_roundtrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (u : CorrectionState.State D) : state e (state e.symm u) = u

theorem NavierStokes.StateReindex.context_roundtrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context D) : context e (context e.symm c) = c

The same weighted classes, without loss of exponents

noncomputable def NavierStokes.StateReindex.strip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (s : WeightedClasses.StripData E) : WeightedClasses.StripData D

Strip, given by ParticularWaveBounds.reindexStrip e s.

Equations

• NavierStokes.StateReindex.strip e s = NavierStokes.ParticularWaveBounds.reindexStrip e s

theorem NavierStokes.StateReindex.memClass_pull {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {alpha : ℝ} {f : ℕ → E → F} (hf : WeightedClasses.MemClass s w alpha f) : WeightedClasses.MemClass (strip e s) (fun (n : ℕ) (x : D) => w n (e x)) alpha fun (n : ℕ) (x : D) => f n (e x)

theorem NavierStokes.StateReindex.block_waveBounds {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {alpha : ℝ} {b : CorrectionState.HarmonicBlock E} (hb : CorrectionState.HarmonicBlock.WaveBounds s w alpha b) : CorrectionState.HarmonicBlock.WaveBounds (strip e s) (fun (n : ℕ) (x : D) => w n (e x)) alpha (block e b)

theorem NavierStokes.StateReindex.block_pressureBounds {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {w : ℕ → E → ℝ} {alpha : ℝ} {b : CorrectionState.HarmonicBlock E} (hb : CorrectionState.HarmonicBlock.PressureBounds s w alpha b) : CorrectionState.HarmonicBlock.PressureBounds (strip e s) (fun (n : ℕ) (x : D) => w n (e x)) alpha (block e b)

Real linearization and the mean equations

theorem NavierStokes.StateReindex.realTransport_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vt Vz : E → E) (u v : E → Fin 3 → ℝ) (x : D) : LinearWaveResidual.realTransport (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (fun (y : D) => u (e y)) (fun (y : D) => v (e y)) x = LinearWaveResidual.realTransport R Vr Vt Vz u v (e x)

theorem NavierStokes.StateReindex.realFrameLaplacian_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vt Vz : E → E) (a : E → Fin 3 → ℝ) (x : D) : LinearWaveResidual.realFrameLaplacian (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (fun (y : D) => a (e y)) x = LinearWaveResidual.realFrameLaplacian R Vr Vt Vz a (e x)

theorem NavierStokes.StateReindex.realComponentLinearResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (epsilon : ℝ) (R : E → ℝ) (Vr Vt Vz Vtime : E → E) (B a : E → Fin 3 → ℝ) (p : E → ℝ) (x : D) : LinearWaveResidual.realComponentLinearResidual epsilon (fun (y : D) => R (e y)) (vector e Vr) (vector e Vt) (vector e Vz) (vector e Vtime) (fun (y : D) => B (e y)) (fun (y : D) => a (e y)) (fun (y : D) => p (e y)) x = LinearWaveResidual.realComponentLinearResidual epsilon R Vr Vt Vz Vtime B a p (e x)

theorem NavierStokes.StateReindex.thetaResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) : (state e u).thetaResidual (context e c) = field e (u.thetaResidual c)

theorem NavierStokes.StateReindex.axialResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) : (state e u).axialResidual (context e c) = field e (u.axialResidual c)

theorem NavierStokes.StateReindex.gr_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) : (state e u).gr (context e c) = field e (u.gr c)

theorem NavierStokes.StateReindex.radialResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) : (state e u).radialResidual (context e c) = field e (u.radialResidual c)

theorem NavierStokes.StateReindex.reducedMeanResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (n : ℕ) (x : D) : (state e u).reducedMeanResidual (context e c) n x = u.reducedMeanResidual c n (e x)

theorem NavierStokes.StateReindex.meanResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (n : ℕ) (x : D) (i : Fin 3) : (state e u).meanResidual (context e c) n x i = u.meanResidual c n (e x) i

theorem NavierStokes.StateReindex.meanGoodResidual_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (n : ℕ) (x : D) (i : Fin 3) : (state e u).meanGoodResidual (context e c) n x i = u.meanGoodResidual c n (e x) i

theorem NavierStokes.StateReindex.block_bandLimited {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {b : CorrectionState.HarmonicBlock E} {N : ℕ} (hb : b.BandLimited N) : (block e b).BandLimited N

The actual association used by the wave assembly

@[reducible, inline]

abbrev NavierStokes.StateReindex.Associated (S : Type) : Type

Associated: an abbreviation for (ℝ × S) × TorusInverse.Plane.

Equations

• NavierStokes.StateReindex.Associated S = ((ℝ × S) × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.StateReindex.associatedTorusAverage {S : Type} (f : Associated S → ℝ) (p : ℝ × S) : ℝ

The actual auxiliary torus integral in the associated layout.

Equations

• NavierStokes.StateReindex.associatedTorusAverage f p = ∫ (y : ℝ) (x : ℝ) in 0..1, f (p, x, y)

noncomputable def NavierStokes.StateReindex.associatedMass {S : Type} (f : Associated S → ℝ) (s : S) : ℝ

The actual radial integral of that torus average.

Equations

• NavierStokes.StateReindex.associatedMass f s = ∫ (r : ℝ), NavierStokes.StateReindex.associatedTorusAverage f (r, s)

theorem NavierStokes.StateReindex.torusAverage_liftAssoc {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (f : Associated S → ℝ) (p : ℝ × S) : PressureStream.torusAverage (fun (x : PressureStream.Lift S) => f ((ParticularWaveBounds.liftAssoc S) x)) p = associatedTorusAverage f p

theorem NavierStokes.StateReindex.pressureMass_liftAssoc {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (f : Associated S → ℝ) (s : S) : PressureStream.pressureMass (fun (x : PressureStream.Lift S) => f ((ParticularWaveBounds.liftAssoc S) x)) s = associatedMass f s

theorem NavierStokes.StateReindex.radialMoment_liftAssoc {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (k : ℕ) (f : MeanIncrementBounds.Field (Associated S)) (n : ℕ) (s : S) : CorrectionState.radialMoment k (field (ParticularWaveBounds.liftAssoc S) f) n s = associatedMass (fun (x : Associated S) => x.1.1 ^ k * f n x) s

theorem NavierStokes.StateReindex.covarianceMass_liftAssoc {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (k : ℕ) (u : CorrectionState.State (Associated S)) (i j : Fin 3) (n : ℕ) (s : S) : CorrectionState.radialMoment k ((state (ParticularWaveBounds.liftAssoc S) u).covariance i j) n s = associatedMass (fun (x : Associated S) => x.1.1 ^ k * u.covariance i j n x) s

theorem NavierStokes.StateReindex.residualBlock_liftAssoc_return {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (b : CorrectionState.HarmonicBlock (PressureStream.Lift S)) (G A : HarmonicResidual.BlockCoefficients (PressureStream.Lift S)) : block (ParticularWaveBounds.liftAssoc S) (HarmonicResidual.residualBlock (context (ParticularWaveBounds.liftAssoc S).symm c) (state (ParticularWaveBounds.liftAssoc S).symm u) (block (ParticularWaveBounds.liftAssoc S).symm b) (blockCoefficients (ParticularWaveBounds.liftAssoc S).symm G) (blockCoefficients (ParticularWaveBounds.liftAssoc S).symm A)) = HarmonicResidual.residualBlock c u b G A

A current state sent into the assembly and returned has exactly its original stripped residual block, including the actual error coefficients.

theorem NavierStokes.StateReindex.fullResidual_liftAssoc_return {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (x : PressureStream.Lift S × ℝ) (i : Fin 3) : LiftedMeanResidual.fullResidual (context (ParticularWaveBounds.liftAssoc S).symm c) (state (ParticularWaveBounds.liftAssoc S).symm u) n ((cylinder (ParticularWaveBounds.liftAssoc S)) x) i = LiftedMeanResidual.fullResidual c u n x i