Sharp whole-horizon low-order propagation for the actual child fields. On good times only the negative part of f' can increase the upper pressure bound; history and early times use the exponentially small target ratio. No child low bound is assumed.
theorem
EulerPacketPhysicalLowBounds.pressureTerm_eq_coefficient
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a slope : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
pressureTerm a slope ((D.M.field t) x) ((D.normal.field t) x)
(EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT H ξ hs (↑t) x) = (EulerPacketPrimaryPressure.coefficient τ hτ hτT H ξ hs a t x * slope) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) x)) ((D.normal.field t) x)
theorem
EulerParentPacketFrames.Evolution.exactPacket_derivative_split
{A : Parent}
(E : Evolution A)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T}
(B :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(residual :
EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(k : ℝ)
(hk : k * κ = 1)
(t : ↑(Set.Icc 0 A.T))
(x : EulerSmoothLimit.Space)
:
fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y))
x = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x + fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k E.inverse t) (A.ell⁻¹ • x) ∧ fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x = fderiv ℝ (E.force t) x + fderiv ℝ (gradient (A.normalizedPacketPressure m hm J support hSupport B residual k E.inverse t)) (A.ell⁻¹ • x)
def
EulerParentPacketFrames.Evolution.SourceErrors
{A : Parent}
(E : Evolution A)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T}
(B :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(residual :
EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(k : ℝ)
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < A.T}
{F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ}
{H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)}
(G : EulerPacketSourceGeometry.Guards hτ hτT F H)
(hball : 1 / 2 ≤ G.radius)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(ev ep : ℝ)
:
The exact source (20) errors, expressed on the same normalized packet that defines the physical child. These are precisely the two errors supplied by the same-Q packet choice.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerParentPacketFrames.Evolution.sourceErrors_of_global
{A : Parent}
(E : Evolution A)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T}
(B :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(residual :
EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(k : ℝ)
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < A.T}
{F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ}
{H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)}
(G : EulerPacketSourceGeometry.Guards hτ hτT F H)
(hball : 1 / 2 ≤ G.radius)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(ev ep : ℝ)
(herr :
∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space),
‖fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k E.inverse t) x - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (E.inverse.normalized t x))) • ((InnerProductSpace.rankOne ℝ)
(EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT H
(EulerPacketSourceGeometry.Guards.terminal hτ hτT F H G) hs (↑t) (E.inverse.normalized t x)))
(((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))‖ < ev ∧ ‖fderiv ℝ (gradient (A.normalizedPacketPressure m hm J support hSupport B residual k E.inverse t)) x - (EulerPacketPrimaryPressure.coefficient τ hτ hτT H (EulerPacketSourceGeometry.Guards.terminal hτ hτT F H G)
hs (G.primaryAmplitude hball) t (E.inverse.normalized t x) * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (E.inverse.normalized t x))) • ((InnerProductSpace.rankOne ℝ)
(((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x)))
(((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))‖ < ep)
:
E.SourceErrors m hm J support hSupport B residual k G hball hs ev ep
The literal strict errors returned by the global same-Q packet theorem imply the error record without any additional analytic bound.
theorem
EulerParentPacketFrames.Evolution.exactPacket_good_low_bounds
{A : Parent}
(E : Evolution A)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T}
(B :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(residual :
EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(k : ℝ)
(hk : k * κ = 1)
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < A.T}
{F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ}
{H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)}
(G : EulerPacketSourceGeometry.Guards hτ hτT F H)
(hball : 1 / 2 ≤ G.radius)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(hδ : 0 < G.δ)
(hδ1 : G.δ ≤ 1)
(ev ep CM CH Kupper : ℝ)
(herr : E.SourceErrors m hm J support hSupport B residual k G hball hs ev ep)
(t : ↑(Set.Icc 0 A.T))
(ht : 1 ≤ EulerPacketMovingFrame.scaledTime τ F.a F.epsilon ↑t)
(x : EulerSmoothLimit.Space)
(hCM : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM)
(hCH : ‖fderiv ℝ (E.force t) x‖ ≤ CH)
(hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2)
:
‖fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y))
x‖ ≤ CM + G.hchild * EulerPacketGeometryLowBounds.goodRatio + ev ∧ ‖fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x‖ ≤ CH + 2 * CM * (G.hchild * EulerPacketGeometryLowBounds.goodRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space),
inner ℝ
((fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x)
z)
z ≤ (Kupper + 2 * CM * G.δ * (G.hchild * EulerPacketGeometryLowBounds.goodRatio) + ep) * ‖z‖ ^ 2
theorem
EulerParentPacketFrames.Evolution.exactPacket_bad_low_bounds
{A : Parent}
(E : Evolution A)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T}
(B :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(residual :
EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(k : ℝ)
(hk : k * κ = 1)
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < A.T}
{F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ}
{H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)}
(G : EulerPacketSourceGeometry.Guards hτ hτT F H)
(hball : 1 / 2 ≤ G.radius)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(hδ : 0 < G.δ)
(hδ1 : G.δ ≤ 1)
(ev ep CM CH Kupper : ℝ)
(herr : E.SourceErrors m hm J support hSupport B residual k G hball hs ev ep)
(t : ↑(Set.Icc 0 A.T))
(ht : EulerPacketMovingFrame.scaledTime τ F.a F.epsilon ↑t ≤ 1)
(x : EulerSmoothLimit.Space)
(hCM : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM)
(hCH : ‖fderiv ℝ (E.force t) x‖ ≤ CH)
(hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2)
:
‖fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y))
x‖ ≤ CM + G.hchild * G.badRatio + ev ∧ ‖fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x‖ ≤ CH + 2 * CM * (G.hchild * G.badRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space),
inner ℝ
((fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x)
z)
z ≤ (Kupper + 2 * CM * (G.hchild * G.badRatio) + ep) * ‖z‖ ^ 2
theorem
EulerParentPacketFrames.Evolution.exactPacket_whole_horizon_low_bounds
{A : Parent}
(E : Evolution A)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T}
(B :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(residual :
EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯
(EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport)
EulerPacketTerminalDatum.period κ hκ Z R))
(k : ℝ)
(hk : k * κ = 1)
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < A.T}
{F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ}
{H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)}
(G : EulerPacketSourceGeometry.Guards hτ hτT F H)
(hball : 1 / 2 ≤ G.radius)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(hδ : 0 < G.δ)
(hδ1 : G.δ ≤ 1)
(ev ep CM CH Kupper : ℝ)
(herr : E.SourceErrors m hm J support hSupport B residual k G hball hs ev ep)
(hCM :
∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space),
‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM)
(hCH : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (E.force t) x‖ ≤ CH)
(hupper :
∀ (t : ↑(Set.Icc 0 A.T)) (x z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2)
(t : ↑(Set.Icc 0 A.T))
(x : EulerSmoothLimit.Space)
:
‖fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y))
x‖ ≤ CM + G.hchild * (EulerPacketGeometryLowBounds.goodRatio + G.badRatio) + ev ∧ ‖fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x‖ ≤ CH + 2 * CM * G.hchild * (EulerPacketGeometryLowBounds.goodRatio + G.badRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space),
inner ℝ
((fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y))
x)
z)
z ≤ (Kupper + 2 * CM * G.hchild * (G.δ * EulerPacketGeometryLowBounds.goodRatio + G.badRatio) + ep) * ‖z‖ ^ 2
The full horizon has one fixed absolute-size cost, while the upper pressure cost retains delta on good times and the exponentially small bad-time ratio. The parent constants remain the actual sharp CM and CH.