Physical residuals in the slow-coordinate order (T,Z)

PhysicalResidualBridge uses slow coordinates (Z,T). The correction-state pipeline uses (T,Z). The map below swaps those two input coordinates and leaves radius, fast variables, angle, and vector components unchanged.

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualTZ.Plane : Type

Plane: an abbreviation for PhysicalResidualBridge.Plane.

Equations

• NavierStokes.PhysicalResidualTZ.Plane = NavierStokes.PhysicalResidualBridge.Plane

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualTZ.Lift : Type

Lift: an abbreviation for PhysicalResidualBridge.Lift.

Equations

• NavierStokes.PhysicalResidualTZ.Lift = NavierStokes.PhysicalResidualBridge.Lift

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualTZ.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.PhysicalResidualTZ.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

noncomputable def NavierStokes.PhysicalResidualTZ.swapSlow : Lift ≃ₗᵢ[ℝ] Lift

The fixed isometric involution (R,(Z,T),Y) ↔ (R,(T,Z),Y).

Equations

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

@[simp]

theorem NavierStokes.PhysicalResidualTZ.swapSlow_apply (x : Lift) : swapSlow x = (x.1, (x.2.1.2, x.2.1.1), x.2.2)

@[simp]

theorem NavierStokes.PhysicalResidualTZ.swapSlow_symm_apply (x : Lift) : swapSlow.symm x = swapSlow x

theorem NavierStokes.PhysicalResidualTZ.swapSlow_swapSlow (x : Lift) : swapSlow (swapSlow x) = x

noncomputable def NavierStokes.PhysicalResidualTZ.swapCylinder : Cylinder ≃ₗᵢ[ℝ] Cylinder

Extension to the actual angular cylinder; the angle is not permuted.

Equations

• NavierStokes.PhysicalResidualTZ.swapCylinder = { toLinearEquiv := NavierStokes.PhysicalResidualTZ.swapSlow.prodCongr (LinearEquiv.refl ℝ ℝ), norm_map' := ⋯ }

@[simp]

theorem NavierStokes.PhysicalResidualTZ.swapCylinder_apply (x : Cylinder) : swapCylinder x = (swapSlow x.1, x.2)

@[simp]

theorem NavierStokes.PhysicalResidualTZ.swapCylinder_symm_apply (x : Cylinder) : swapCylinder.symm x = swapCylinder x

theorem NavierStokes.PhysicalResidualTZ.swapCylinder_swapCylinder (x : Cylinder) : swapCylinder (swapCylinder x) = x

theorem NavierStokes.PhysicalResidualTZ.swapSlow_toContinuousLinearMap : ↑↑swapSlow = (ContinuousLinearMap.id ℝ ℝ).prodMap ((↑(ContinuousLinearEquiv.prodComm ℝ ℝ ℝ)).prodMap (ContinuousLinearMap.id ℝ Plane))

This is exactly the continuous linear map used for swapSlow in the variable-gauge module, expressed using only frozen dependencies.

noncomputable def NavierStokes.PhysicalResidualTZ.reindexVector {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (V : E → E) (x : E) : E

Pullback of a vector field under a fixed linear change of coordinates.

Equations

• NavierStokes.PhysicalResidualTZ.reindexVector e V x = e.symm (V (e x))

theorem NavierStokes.PhysicalResidualTZ.fderiv_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] E) (f : E → F) (x v : E) : (fderiv ℝ (fun (y : E) => f (e y)) x) v = (fderiv ℝ f (e x)) (e v)

The chain rule is valid even for the total derivative convention at a nondifferentiable point, because the coordinate change is an equivalence.

theorem NavierStokes.PhysicalResidualTZ.along_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] E) (V : E → E) (f : E → F) : (HarmonicCalculus.along (reindexVector e V) fun (x : E) => f (e x)) = fun (x : E) => HarmonicCalculus.along V f (e x)

theorem NavierStokes.PhysicalResidualTZ.along_reindex_component {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_3} (e : E ≃L[ℝ] E) (V : E → E) (f : E → ι → F) (i : ι) : (HarmonicCalculus.along (reindexVector e V) fun (x : E) => f (e x) i) = fun (x : E) => HarmonicCalculus.along V (fun (y : E) => f y i) (e x)

theorem NavierStokes.PhysicalResidualTZ.cylindricalLaplacian_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (f : E → F) (x : E) : HarmonicCalculus.cylindricalLaplacian (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => f (e y)) x = HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz f (e x)

theorem NavierStokes.PhysicalResidualTZ.cylindricalLaplacian_reindex_component {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_3} (e : E ≃L[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (f : E → ι → F) (i : ι) (x : E) : HarmonicCalculus.cylindricalLaplacian (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => f (e y) i) x = HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz (fun (y : E) => f y i) (e x)

theorem NavierStokes.PhysicalResidualTZ.transport_reindex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (u v : E → HarmonicCalculus.ComplexVector) (x : E) : LinearWaveResidual.transport (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => u (e y)) (fun (y : E) => v (e y)) x = LinearWaveResidual.transport R Vr Vθ Vz u v (e x)

theorem NavierStokes.PhysicalResidualTZ.cylindricalVectorLaplacian_reindex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → HarmonicCalculus.ComplexVector) (x : E) : HarmonicCalculus.cylindricalVectorLaplacian (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => a (e y)) x = HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz a (e x)

theorem NavierStokes.PhysicalResidualTZ.linearResidual_reindex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (epsilon : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (B a : E → HarmonicCalculus.ComplexVector) (p : E → ℂ) (x : E) : LinearWaveResidual.linearResidual epsilon (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (reindexVector e Vt) (fun (y : E) => B (e y)) (fun (y : E) => a (e y)) (fun (y : E) => p (e y)) x = LinearWaveResidual.linearResidual epsilon R Vr Vθ Vz Vt B a p (e x)

theorem NavierStokes.PhysicalResidualTZ.realTransport_reindex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (u v : E → Fin 3 → ℝ) (x : E) : LinearWaveResidual.realTransport (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => u (e y)) (fun (y : E) => v (e y)) x = LinearWaveResidual.realTransport R Vr Vθ Vz u v (e x)

theorem NavierStokes.PhysicalResidualTZ.realFrameLaplacian_reindex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → Fin 3 → ℝ) (x : E) : LinearWaveResidual.realFrameLaplacian (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => a (e y)) x = LinearWaveResidual.realFrameLaplacian R Vr Vθ Vz a (e x)

theorem NavierStokes.PhysicalResidualTZ.graphResidual_reindex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E ≃L[ℝ] E) (epsilon : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (a : E → Fin 3 → ℝ) (p : E → ℝ) (x : E) : PhysicalResidualBridge.graphResidual epsilon (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (reindexVector e Vt) (fun (y : E) => a (e y)) (fun (y : E) => p (e y)) x = PhysicalResidualBridge.graphResidual epsilon R Vr Vθ Vz Vt a p (e x)

noncomputable def NavierStokes.PhysicalResidualTZ.swapField (f : MeanIncrementBounds.Field Lift) : MeanIncrementBounds.Field Lift

Swap field, defined pointwise by f n (swapSlow x).

Equations

• NavierStokes.PhysicalResidualTZ.swapField f n x = f n (NavierStokes.PhysicalResidualTZ.swapSlow x)

noncomputable def NavierStokes.PhysicalResidualTZ.swapTriple (m : MeanIncrementBounds.Triple Lift) : MeanIncrementBounds.Triple Lift

Swap triple, given by ⟨swapField m.radial, swapField m.angular, swapField m.axial⟩.

Equations

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

noncomputable def NavierStokes.PhysicalResidualTZ.swapOperators (o : MeanIncrementBounds.Operators Lift) : MeanIncrementBounds.Operators Lift

Swap 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.PhysicalResidualTZ.swapContext (c : CorrectionState.Context Lift) : CorrectionState.Context Lift

Swap context, bundling operators, base, virtualTheta, virtualAxial.

Equations

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

noncomputable def NavierStokes.PhysicalResidualTZ.swapOscillation (f : CorrectionState.Oscillation Lift) : CorrectionState.Oscillation Lift

Swap oscillation, defined pointwise by f n (swapCylinder x).

Equations

• NavierStokes.PhysicalResidualTZ.swapOscillation f n x = f n (NavierStokes.PhysicalResidualTZ.swapCylinder x)

noncomputable def NavierStokes.PhysicalResidualTZ.swapErrors (e : CorrectionState.ExcludedErrors Lift) : CorrectionState.ExcludedErrors Lift

Swap errors, bundling base, gaussian, aliasError.

Equations

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

noncomputable def NavierStokes.PhysicalResidualTZ.swapState (s : CorrectionState.State Lift) : CorrectionState.State Lift

Swap 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.PhysicalResidualTZ.fderiv_swapField (f : MeanIncrementBounds.Field Lift) (n : ℕ) (x v : Lift) : (fderiv ℝ (swapField f n) x) (swapSlow v) = (fderiv ℝ (f n) (swapSlow x)) v

theorem NavierStokes.PhysicalResidualTZ.dr_swap (o : MeanIncrementBounds.Operators Lift) (f : MeanIncrementBounds.Field Lift) : (swapOperators o).dr (swapField f) = swapField (o.dr f)

theorem NavierStokes.PhysicalResidualTZ.dz_swap (o : MeanIncrementBounds.Operators Lift) (f : MeanIncrementBounds.Field Lift) : (swapOperators o).dz (swapField f) = swapField (o.dz f)

theorem NavierStokes.PhysicalResidualTZ.time_swap (o : MeanIncrementBounds.Operators Lift) (f : MeanIncrementBounds.Field Lift) : (swapOperators o).time (swapField f) = swapField (o.time f)

theorem NavierStokes.PhysicalResidualTZ.radialDiv_swap (o : MeanIncrementBounds.Operators Lift) (k : ℝ) (f : MeanIncrementBounds.Field Lift) : (swapOperators o).radialDiv k (swapField f) = swapField (o.radialDiv k f)

theorem NavierStokes.PhysicalResidualTZ.radialDirection_swap (c : CorrectionState.Context Lift) (n : ℕ) : LiftedMeanResidual.radialDirection (swapContext c) n = reindexVector (↑swapCylinder) (LiftedMeanResidual.radialDirection c n)

theorem NavierStokes.PhysicalResidualTZ.axialDirection_swap (c : CorrectionState.Context Lift) (n : ℕ) : LiftedMeanResidual.axialDirection (swapContext c) n = reindexVector (↑swapCylinder) (LiftedMeanResidual.axialDirection c n)

theorem NavierStokes.PhysicalResidualTZ.timeDirection_swap (c : CorrectionState.Context Lift) (n : ℕ) : LiftedMeanResidual.timeDirection (swapContext c) n = reindexVector (↑swapCylinder) (LiftedMeanResidual.timeDirection c n)

theorem NavierStokes.PhysicalResidualTZ.angularDirection_swap : reindexVector (↑swapCylinder) LiftedMeanResidual.angularDirection = LiftedMeanResidual.angularDirection

theorem NavierStokes.PhysicalResidualTZ.complexBase_swap (c : CorrectionState.Context Lift) (n : ℕ) : LiftedMeanResidual.complexBase (swapContext c) n = fun (x : Cylinder) => LiftedMeanResidual.complexBase c n (swapCylinder x)

theorem NavierStokes.PhysicalResidualTZ.complexPerturbation_swap (s : CorrectionState.State Lift) (n : ℕ) : LiftedMeanResidual.complexPerturbation (swapState s) n = fun (x : Cylinder) => LiftedMeanResidual.complexPerturbation s n (swapCylinder x)

theorem NavierStokes.PhysicalResidualTZ.complexPressure_swap (s : CorrectionState.State Lift) (n : ℕ) : LiftedMeanResidual.complexPressure (swapState s) n = fun (x : Cylinder) => LiftedMeanResidual.complexPressure s n (swapCylinder x)

theorem NavierStokes.PhysicalResidualTZ.virtualDivergence_swap (c : CorrectionState.Context Lift) (n : ℕ) (x : Cylinder) : LiftedMeanResidual.virtualDivergence (swapContext c) n x = LiftedMeanResidual.virtualDivergence c n (swapCylinder x)

theorem NavierStokes.PhysicalResidualTZ.fullResidual_swap (c : CorrectionState.Context Lift) (s : CorrectionState.State Lift) (n : ℕ) (x : Cylinder) (i : Fin 3) : LiftedMeanResidual.fullResidual (swapContext c) (swapState s) n x i = LiftedMeanResidual.fullResidual c s n (swapCylinder x) i

Exact covariance of the full nonlinear correction residual. It includes the fixed base error once, exactly as in the original state definition.

theorem NavierStokes.PhysicalResidualTZ.fullGoodResidual_swap (c : CorrectionState.Context Lift) (s : CorrectionState.State Lift) (n : ℕ) (x : Cylinder) (i : Fin 3) : LiftedMeanResidual.fullGoodResidual (swapContext c) (swapState s) n x i = LiftedMeanResidual.fullGoodResidual c s n (swapCylinder x) i

structure NavierStokes.PhysicalResidualTZ.MatchesAtTZ (o : MeanIncrementBounds.Operators Lift) (G : PhysicalResidualBridge.ScaledGraph) (n : ℕ) : Prop

Literal operator data in the order (T,Z). No derivative identity is assumed: all derivative transport is supplied by the preceding theorems.

• epsilon : o.epsilon n = G.epsilon
• frequency : o.radialFrequency n = G.frequency
• fast : o.fastCoefficient n = G.fastCoefficient
• radius : o.radius = Prod.fst
• profile : o.radialProfile = fun (x : Lift) => GraphCalculus.radialSpeed G.exponent x.1
• eR : o.eR = (1, 0, 0)
• eZ : o.eZ = (0, (0, 1), 0)
• eT : o.eT = (0, (1, 0), 0)
• vR : o.vR = (0, 0, G.radialVector)
• vT : o.vT = (0, 0, G.temporalVector)

theorem NavierStokes.PhysicalResidualTZ.MatchesAtTZ.toMatchesAt {o : MeanIncrementBounds.Operators Lift} {G : PhysicalResidualBridge.ScaledGraph} {n : ℕ} (H : MatchesAtTZ o G n) : PhysicalResidualBridge.MatchesAt (swapOperators o) G n

theorem NavierStokes.PhysicalResidualTZ.matchesAtTZ_graphOperators (r : CorrectionState.ReconstructionData) (epsilon fast : ℕ → ℝ) (G : PhysicalResidualBridge.ScaledGraph) (n : ℕ) (hε : epsilon n = G.epsilon) (hM : r.frequency n = G.frequency) (hc : fast n = G.fastCoefficient) (hd : r.exponent = G.exponent) (hv : r.radialDirection = G.radialVector) : MatchesAtTZ (CorrectionState.graphOperators r epsilon fast ((0, 1), 0) ((1, 0), 0) G.temporalVector) G n

noncomputable def NavierStokes.PhysicalResidualTZ.graphMapTZ (G : PhysicalResidualBridge.ScaledGraph) (p : ProblemStatement.SpaceTime) : Cylinder

The actual scaled physical graph, with the slow coordinates in (T,Z) order.

Equations

• NavierStokes.PhysicalResidualTZ.graphMapTZ G p = NavierStokes.PhysicalResidualTZ.swapCylinder (G.map p)

noncomputable def NavierStokes.PhysicalResidualTZ.graphSourceTZ (G : PhysicalResidualBridge.ScaledGraph) (U : Set Cylinder) : Set ProblemStatement.SpaceTime

Graph source TZ, given by {p | 0 < p.2 0 ∧ graphMapTZ G p ∈ U}.

Equations

• NavierStokes.PhysicalResidualTZ.graphSourceTZ G U = {p : NavierStokes.ProblemStatement.SpaceTime | 0 < p.2.ofLp 0 ∧ NavierStokes.PhysicalResidualTZ.graphMapTZ G p ∈ U}

noncomputable def NavierStokes.PhysicalResidualTZ.graphRadialTZ (G : PhysicalResidualBridge.ScaledGraph) : Cylinder → Cylinder

Graph radial TZ, given by reindexVector swapCylinder.toContinuousLinearEquiv G.radial.

Equations

• NavierStokes.PhysicalResidualTZ.graphRadialTZ G = NavierStokes.PhysicalResidualTZ.reindexVector (↑NavierStokes.PhysicalResidualTZ.swapCylinder) G.radial

noncomputable def NavierStokes.PhysicalResidualTZ.graphAngularTZ : Cylinder → Cylinder

Graph angular TZ, given by reindexVector swapCylinder.toContinuousLinearEquiv PhysicalResidualBridge.ScaledGraph.angular.

Equations

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

noncomputable def NavierStokes.PhysicalResidualTZ.graphAxialTZ (G : PhysicalResidualBridge.ScaledGraph) : Cylinder → Cylinder

Graph axial TZ, given by reindexVector swapCylinder.toContinuousLinearEquiv G.axial.

Equations

• NavierStokes.PhysicalResidualTZ.graphAxialTZ G = NavierStokes.PhysicalResidualTZ.reindexVector (↑NavierStokes.PhysicalResidualTZ.swapCylinder) G.axial

noncomputable def NavierStokes.PhysicalResidualTZ.graphTemporalTZ (G : PhysicalResidualBridge.ScaledGraph) : Cylinder → Cylinder

Graph temporal TZ, given by reindexVector swapCylinder.toContinuousLinearEquiv G.temporal.

Equations

• NavierStokes.PhysicalResidualTZ.graphTemporalTZ G = NavierStokes.PhysicalResidualTZ.reindexVector (↑NavierStokes.PhysicalResidualTZ.swapCylinder) G.temporal

theorem NavierStokes.PhysicalResidualTZ.graphAxialTZ_apply (G : PhysicalResidualBridge.ScaledGraph) (x : Cylinder) : graphAxialTZ G x = ((0, (0, G.epsilon), 0), 0)

theorem NavierStokes.PhysicalResidualTZ.graphTemporalTZ_apply (G : PhysicalResidualBridge.ScaledGraph) (x : Cylinder) : graphTemporalTZ G x = ((0, (-G.epsilon, 0), G.fastCoefficient • G.temporalVector), 0)

theorem NavierStokes.PhysicalResidualTZ.graphRadialTZ_eq (G : PhysicalResidualBridge.ScaledGraph) : graphRadialTZ G = G.radial

theorem NavierStokes.PhysicalResidualTZ.graphAngularTZ_eq : graphAngularTZ = PhysicalResidualBridge.ScaledGraph.angular

noncomputable def NavierStokes.PhysicalResidualTZ.velocityTZ (G : PhysicalResidualBridge.ScaledGraph) (a : Cylinder → Fin 3 → ℝ) : ProblemStatement.VelocityField

Velocity TZ, given by G.velocity (fun x => a (swapCylinder x)).

Equations

• NavierStokes.PhysicalResidualTZ.velocityTZ G a = G.velocity fun (x : NavierStokes.PhysicalResidualBridge.Cylinder) => a (NavierStokes.PhysicalResidualTZ.swapCylinder x)

noncomputable def NavierStokes.PhysicalResidualTZ.pressureTZ (G : PhysicalResidualBridge.ScaledGraph) (p : Cylinder → ℝ) : ProblemStatement.PressureField

Pressure TZ, given by G.pressure (fun x => p (swapCylinder x)).

Equations

• NavierStokes.PhysicalResidualTZ.pressureTZ G p = G.pressure fun (x : NavierStokes.PhysicalResidualBridge.Cylinder) => p (NavierStokes.PhysicalResidualTZ.swapCylinder x)

theorem NavierStokes.PhysicalResidualTZ.graphResidual_swap (G : PhysicalResidualBridge.ScaledGraph) (a : Cylinder → Fin 3 → ℝ) (p : Cylinder → ℝ) (x : Cylinder) : PhysicalResidualBridge.graphResidual G.epsilon PhysicalResidualBridge.ScaledGraph.radius G.radial PhysicalResidualBridge.ScaledGraph.angular G.axial G.temporal (fun (y : PhysicalResidualBridge.Cylinder) => a (swapCylinder y)) (fun (y : PhysicalResidualBridge.Cylinder) => p (swapCylinder y)) x = PhysicalResidualBridge.graphResidual G.epsilon PhysicalResidualBridge.ScaledGraph.radius (graphRadialTZ G) graphAngularTZ (graphAxialTZ G) (graphTemporalTZ G) a p (swapCylinder x)

Exact covariance of the complete real graph equation in the two layouts.

noncomputable def NavierStokes.PhysicalResidualTZ.physicalToChartTZ (h : ℝ) (n k : ℕ) : Lift →L[ℝ] Lift

The same fixed linear chart map used by the variable-gauge mean, in (T,Z) order.

Equations

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

theorem NavierStokes.PhysicalResidualTZ.physicalToChartTZ_swap (h : ℝ) (n k : ℕ) (x : Lift) : (physicalToChartTZ h n k) (swapSlow x) = swapSlow ((MeanChartCompatibility.physicalToChart h n k) x)

theorem NavierStokes.PhysicalResidualTZ.physicalToChartTZ_eq_formula (h : ℝ) (n k : ℕ) : physicalToChartTZ h n k = MeanChartCompatibility.chartLinear (MeanChartCompatibility.chartScale n) (((ChartScales.Q n ^ (-1) • ContinuousLinearMap.fst ℝ ℝ ℝ).prod (ChartScales.Q n ^ (-CoordinateAlgebra.D h) • ContinuousLinearMap.snd ℝ ℝ ℝ)).prodMap (TemporalMeanUpdate.coverMap k))

noncomputable def NavierStokes.PhysicalResidualTZ.absoluteLiftTZ (h : ℝ) (p : ProblemStatement.SpaceTime) : Lift

Absolute lift TZ, given by swapSlow (PhysicalResidualBridge.absoluteLift h p).

Equations

• NavierStokes.PhysicalResidualTZ.absoluteLiftTZ h p = NavierStokes.PhysicalResidualTZ.swapSlow (NavierStokes.PhysicalResidualBridge.absoluteLift h p)

theorem NavierStokes.PhysicalResidualTZ.commonGraph_eq_physicalToChartTZ (h : ℝ) (n k : ℕ) {p : ProblemStatement.SpaceTime} (hr : 0 < p.2.ofLp 0) : graphMapTZ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h k) p = ((physicalToChartTZ h n k) (absoluteLiftTZ h p), p.2.ofLp 1)

theorem NavierStokes.PhysicalResidualTZ.context_fullResidual_physicalTZ {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k n : ℕ) (c : CorrectionState.Context Lift) (s : CorrectionState.State Lift) (H : MatchesAtTZ c.operators (PhysicalResidualBridge.commonGraph Q h k) n) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {p₀ : Cylinder → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : PhysicalResidualBridge.Cylinder) => PhysicalResidualBridge.baseComponents c n x i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : PhysicalResidualBridge.Cylinder) => PhysicalResidualBridge.incrementComponents s n x i) U) (hp₀ : ContDiffOn ℝ (↑⊤) p₀ U) (hp : ContDiffOn ℝ (↑⊤) (s.totalPressureIncrement n) U) {t : ℝ} {q : ProblemStatement.Space} (hz : (t, q) ∈ graphSourceTZ (PhysicalResidualBridge.commonGraph Q h k) U) (hbase : ∀ (i : Fin 3), PhysicalResidualBridge.graphResidual (Q ^ h) PhysicalResidualBridge.ScaledGraph.radius (graphRadialTZ (PhysicalResidualBridge.commonGraph Q h k)) graphAngularTZ (graphAxialTZ (PhysicalResidualBridge.commonGraph Q h k)) (graphTemporalTZ (PhysicalResidualBridge.commonGraph Q h k)) (PhysicalResidualBridge.baseComponents c n) p₀ (graphMapTZ (PhysicalResidualBridge.commonGraph Q h k) (t, q)) i = LiftedMeanResidual.virtualDivergence c n (graphMapTZ (PhysicalResidualBridge.commonGraph Q h k) (t, q)) i + s.errors.base n (graphMapTZ (PhysicalResidualBridge.commonGraph Q h k) (t, q)) i) {u : ProblemStatement.VelocityField} {P : ProblemStatement.PressureField} (hu : ContDiffAt ℝ 2 u (t, CylindricalResidual.chart q)) (hP : DifferentiableAt ℝ P (t, CylindricalResidual.chart q)) (hrep : (fun (z : ProblemStatement.SpaceTime) => u (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) (velocityTZ (PhysicalResidualBridge.commonGraph Q h k) (fun (y : Cylinder) (j : Fin 3) => PhysicalResidualBridge.baseComponents c n y j + PhysicalResidualBridge.incrementComponents s n y j) z)) (hpRep : CylindricalResidual.pressurePullback P =ᶠ[nhds (t, q)] pressureTZ (PhysicalResidualBridge.commonGraph Q h k) fun (y : Cylinder) => p₀ y + s.totalPressureIncrement n y) (i : Fin 3) : LiftedMeanResidual.fullResidual c s n (graphMapTZ (PhysicalResidualBridge.commonGraph Q h k) (t, q)) i = Q ^ (2 * CoordinateAlgebra.A h + 1 / 2) * ((CylindricalResidual.frame (-q.ofLp 1)) (ProblemStatement.navierStokesResidual u P t (CylindricalResidual.chart q))).ofLp i

The full correction-state residual in (T,Z) coordinates is the actual scaled Cartesian Navier--Stokes residual. The fixed base-pressure equation and the neighborhood representation of the actual physical fields remain explicit.