The literal zero-history initialized packet supplies the all-order approximation residual identity, including its actual pressure gradient. Its velocity, time derivative and residual are the fields already constructed from the source profiles, not additional approximation hypotheses.
The actual direct-forward source packet has a lifted pressure gradient. Every component is constructed from its mean or oscillatory inverse.
noncomputable def
EulerTransversePacketProvider.Forcing.pressureGradientWitness
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(I : InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
:
EulerPacketPressure.GradientWitness P D.T κ m (G.scalar I)
Pressure gradient witness, constructed using GradientWitness.compact.
Equations
- G.pressureGradientWitness I κ m = EulerPacketPressure.GradientWitness.compact (G.scalar I) (G.pressurePath I) ⋯ ⋯ D.support ⋯ ⋯
Instances For
noncomputable def
EulerPacketCylinderField.sourceHighPressureWitnessStep
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
(hp : 2 ≤ p)
:
EulerPacketPressure.GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).highPressure
Source high pressure witness step as an element of GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).highPressure.
Equations
- EulerPacketCylinderField.sourceHighPressureWitnessStep P M D hTime I Iprimary κ m p hp = ⋯.mpr (id (⋯.mpr (((Classical.choice ⋯).pressureGradientWitness I κ m).changeTime ⋯)))
Instances For
noncomputable def
EulerPacketCylinderField.sourceMeanPressureWitnessStep
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
(hp : 2 ≤ p)
:
EulerPacketPressure.GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).meanPressure
Source mean pressure witness step as an element of GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).meanPressure.
Equations
- EulerPacketCylinderField.sourceMeanPressureWitnessStep P M D hTime I Iprimary κ m p hp = ⋯.mpr (id (⋯.mpr ((Classical.choice ⋯).pressureGradientWitness P κ m)))
Instances For
noncomputable def
EulerPacketCylinderField.sourceHighPressureWitness
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
:
EulerPacketPressure.GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).highPressure
Source high pressure witness as an element of GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).highPressure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceMeanPressureWitness
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
:
EulerPacketPressure.GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).meanPressure
Source mean pressure witness as an element of GradientWitness P M.T κ m (sourceProfiles P M D I Iprimary p).meanPressure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourcePressureWitness
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(N : ℕ)
(r : ℝ)
:
EulerPacketPressure.GradientWitness P M.T κ m
(EulerPacketPointJets.fieldSum (N + 1) r
(EulerPacketProfileRecursion.assembledPressure N (sourceProfiles P M D I Iprimary)))
Source pressure witness, constructed using GradientWitness.evaluateFamily.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finite zero-history pressure and its actual lifted gradient.
noncomputable def
EulerPacketTerminalDatum.forwardInitializedPressure
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Forward initialized pressure, given by fieldSum (N+1) κ (assembledPressure N (forwardInitializedProfiles M D δ hδ ξ hs α)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedPressureWitness
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketPressure.GradientWitness period M.T κ D.m₀ (forwardInitializedPressure M D δ hδ ξ hs α N κ)
Forward initialized pressure witness, given by sourcePressureWitness period M D hTime (InitialData.zero period D) (initialData D δ hδ (α • ξ) hs) κ D.m₀ N κ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedCoordinatePressureField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
(hk : k ≠ 0)
:
EulerPacketCylinderField.Field period D.T
(EulerPacketCoordinates.coordinatePressure D k (forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹))
Forward initialized coordinate pressure field, given by pressureField D k hk ((forwardInitializedPressureWitness M D hTime δ hδ ξ hs α N k⁻¹).changeTime hTime).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedCoordinatePressureField_mem
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
(hk : k ≠ 0)
(t : ↑(Set.Icc 0 D.T))
:
(forwardInitializedCoordinatePressureField M D hTime δ hδ ξ hs α N k hk).path t ∈ EulerLiftedGradientSpace.gradientSpace period k⁻¹ D.m₀
theorem
EulerPacketCylinderField.Field.toFieldTower_eq_of_path_eq_forward
{P T : ℝ}
[Fact (0 < P)]
{raw raw' : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(H : Field P T raw')
(h : G.path = H.path)
:
noncomputable def
EulerPacketTerminalDatum.forwardInitializedVelocity
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Forward initialized velocity, given by fieldSum (N+1) κ (assembledVelocity N (forwardInitializedProfiles M D δ hδ ξ hs α)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedVelocityField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.Field period D.T (forwardInitializedVelocity M D δ hδ ξ hs α N κ)
Forward initialized velocity field as an element of Field period D.T (forwardInitializedVelocity M D δ hδ ξ hs α N κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedVelocityDerivative
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Forward initialized velocity derivative, constructed using fieldSum.
Equations
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedVelocityDerivativeField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.Field period D.T (forwardInitializedVelocityDerivative M D δ hδ ξ hs α N κ)
Forward initialized velocity derivative field as an element of Field period D.T (forwardInitializedVelocityDerivative M D δ hδ ξ hs α N κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedVelocityField_time
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.TimeDerivative ⋯ (forwardInitializedVelocityField M D hTime δ hδ ξ hs α N κ)
(forwardInitializedVelocityDerivativeField M D hTime δ hδ ξ hs α N κ)
theorem
EulerPacketTerminalDatum.forwardInitializedNormalizedField_path_eq
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
(forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k).path = (EulerPacketCoordinates.coordinateField D (forwardInitializedVelocityField M D hTime δ hδ ξ hs α N k⁻¹) k).path
The pairwise curl construction and the literal velocity sum represent the same normalized coordinate field.
theorem
EulerPacketTerminalDatum.forwardInitializedNormalizedField_tower_eq
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
(forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k).toFieldTower = (EulerPacketCoordinates.coordinateField D (forwardInitializedVelocityField M D hTime δ hδ ξ hs α N k⁻¹)
k).toFieldTower
noncomputable def
EulerPacketTerminalDatum.forwardInitializedCoordinateResidualField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
:
EulerPacketCylinderField.Field period D.T
(EulerPacketCoordinates.normalizedResidual D k (forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹)
(forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹))
Forward initialized coordinate residual field used in packet forward initialized residual equation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedCorrectionData_eq_coordinate
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hκ : |k⁻¹| ≤ 1)
:
forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk = EulerPacketCoordinates.coordinateData D k hκ (forwardInitializedVelocityField M D hTime δ hδ ξ hs α N k⁻¹)
(forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹)
(forwardInitializedCoordinateResidualField M D hTime δ hδ ξ hs α Cagree N hN k hk)
This is the exact initialized correction data used by the quantitative budget, after identifying the two genuine realizations of its fields.
noncomputable def
EulerPacketTerminalDatum.forwardInitializedApproximationResidual
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
:
EulerAllOrderDriftCorrection.ApproximationResidual period ⋯
(forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)
The actual finite pressure and every-order residual identity, with no assumed pressure field, approximation derivative or residual cancellation.
Equations
- One or more equations did not get rendered due to their size.