The literal 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 literal initialized finite packet has a genuine pressure-gradient Field in the closed lifted gradient space. Both the mean and oscillatory pieces come from the actual source inverses.
noncomputable def
EulerTransversePacketPrimary.pressureGradientWitness
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
:
EulerPacketPressure.GradientWitness P D.T κ m (scalar τ hτ hτT B Y)
Pressure gradient witness, constructed using GradientWitness.compact.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketJoin.pressureGradientWitness
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
:
EulerPacketPressure.GradientWitness P D.T κ m (scalar τ hτ hτT B G)
Pressure gradient witness, constructed using GradientWitness.compact.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.joinedSourceHighPressureWitnessStep
(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)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
(hp : 2 ≤ p)
:
EulerPacketPressure.GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure
Joined source high pressure witness step as an element of GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.joinedSourceMeanPressureWitnessStep
(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)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
(hp : 2 ≤ p)
:
EulerPacketPressure.GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure
Joined source mean pressure witness step as an element of GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure.
Equations
- EulerPacketCylinderField.joinedSourceMeanPressureWitnessStep P M D hTime τ hτ hτT B primary hprimary κ m p hp = ⋯.mpr (id (⋯.mpr ((Classical.choice ⋯).pressureGradientWitness P κ m)))
Instances For
noncomputable def
EulerPacketCylinderField.joinedSourceHighPressureWitness
(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)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(hπ : EulerPacketPressure.GradientWitness P M.T κ m primary.highPressure)
(p : ℕ)
:
EulerPacketPressure.GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure
Joined source high pressure witness as an element of GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.joinedSourceMeanPressureWitness
(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)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(hq : EulerPacketPressure.GradientWitness P M.T κ m primary.meanPressure)
(p : ℕ)
:
EulerPacketPressure.GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure
Joined source mean pressure witness as an element of GradientWitness P M.T κ m (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.joinedPressureWitness
(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)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(hq : EulerPacketPressure.GradientWitness P M.T κ m primary.meanPressure)
(hπ : EulerPacketPressure.GradientWitness P M.T κ m primary.highPressure)
(N : ℕ)
(r : ℝ)
:
EulerPacketPressure.GradientWitness P M.T κ m
(EulerPacketPointJets.fieldSum (N + 1) r
(EulerPacketProfileRecursion.assembledPressure N (joinedSourceProfiles P M D τ hτ hτT B primary)))
Joined pressure witness, constructed using GradientWitness.evaluateFamily.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedPressure
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Initialized pressure, given by fieldSum (N+1) κ (assembledPressure N (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedPressureWitness
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketPressure.GradientWitness period M.T κ D.m₀ (initializedPressure M D τ hτ hτT B δ hδ ξ hs α N κ)
Every pressure component is supplied by its actual inverse, including the literal compact terminal primary at grade one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedCoordinatePressureField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
(hk : k ≠ 0)
:
EulerPacketCylinderField.Field period D.T
(EulerPacketCoordinates.coordinatePressure D k (initializedPressure M D τ hτ hτT B δ hδ ξ hs α N k⁻¹))
The actual pressure-gradient input Pa for the normalized coordinate equation. The factor k² is the same as in the literal residual identity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedCoordinatePressureField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
(hk : k ≠ 0)
(t : ↑(Set.Icc 0 D.T))
:
(initializedCoordinatePressureField M D hTime τ hτ hτT B δ hδ ξ hs α N k hk).path t ∈ EulerLiftedGradientSpace.gradientSpace period k⁻¹ D.m₀
theorem
EulerPacketCylinderField.Field.toFieldTower_eq_of_path_eq
{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.initializedVelocity
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Initialized velocity, given by fieldSum (N+1) κ (assembledVelocity N (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedVelocityField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.Field period D.T (initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N κ)
Initialized velocity field as an element of Field period D.T (initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedVelocityDerivative
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Initialized velocity derivative, constructed using fieldSum.
Equations
- EulerPacketTerminalDatum.initializedVelocityDerivative M D τ hτ hτT B δ hδ ξ hs α N κ = EulerPacketPointJets.fieldSum (N + 1) κ EulerPacketCylinderField.ProfileRegularity.velocityTimeCoefficients
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedVelocityDerivativeField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.Field period D.T (initializedVelocityDerivative M D τ hτ hτT B δ hδ ξ hs α N κ)
Initialized velocity derivative field as an element of Field period D.T (initializedVelocityDerivative M D τ hτ hτT B δ hδ ξ hs α N κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedVelocityField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.TimeDerivative ⋯ (initializedVelocityField M D hTime τ hτ hτT B δ hδ ξ hs α N κ)
(initializedVelocityDerivativeField M D hTime τ hτ hτT B δ hδ ξ hs α N κ)
theorem
EulerPacketTerminalDatum.initializedNormalizedField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
(initializedNormalizedField M D hTime τ hτ hτT B δ hδ ξ hs α N k).path = (EulerPacketCoordinates.coordinateField D (initializedVelocityField M D hTime τ hτ hτT B δ hδ ξ hs α N k⁻¹) k).path
The pairwise curl construction and the literal velocity sum represent the same normalized coordinate field.
theorem
EulerPacketTerminalDatum.initializedNormalizedField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
(initializedNormalizedField M D hTime τ hτ hτT B δ hδ ξ hs α N k).toFieldTower = (EulerPacketCoordinates.coordinateField D (initializedVelocityField M D hTime τ hτ hτT B δ hδ ξ hs α N k⁻¹)
k).toFieldTower
noncomputable def
EulerPacketTerminalDatum.initializedCoordinateResidualField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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 (initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N k⁻¹)
(initializedPressure M D τ hτ hτT B δ hδ ξ hs α N k⁻¹))
Initialized coordinate residual field used in packet initialized residual equation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedCorrectionData_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
:
initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk = EulerPacketCoordinates.coordinateData D k hκ (initializedVelocityField M D hTime τ hτ hτT B δ hδ ξ hs α N k⁻¹)
(initializedPressure M D τ hτ hτT B δ hδ ξ hs α N k⁻¹)
(initializedCoordinateResidualField M D hTime τ hτ hτT B δ 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.initializedApproximationResidual
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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 ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ 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.