A single source budget closes every forced transverse grade. The actual profile is retained, its positive scalar factor cancels exactly, and one spare derivative shift pays the fixed operator constants.
The complete quantitative forced transverse provider #
Source-only budgets fixed before the forcing give actual A, A_t, π, dπ, Q, Q_t, C and C_t bounds linear in its amplitude. All eight outputs use the same external radius and fixed mixed Sobolev order. They spend at most four derivative shifts, within the manuscript's ten-shift allowance.
Unit-amplitude bounds for the complete actual transverse inverse #
One source-only budget controls the history trace, forward solve and their joined physical velocity and genuine time derivative. The input and output use the same fixed mixed-word Sobolev order and the same external radius.
theorem
EulerTransversePacketJoin.Budget.history_forcing_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
(EulerTransversePacketProvider.HistoryData.forcingPath (G.initial τ hτ ⋯)))
n 0 ≤ EulerGevrey.majorant L.R d n
theorem
EulerTransversePacketJoin.Budget.forward_forcing_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath (G.tail τ ⋯ hτT))))
n 0 ≤ EulerGevrey.majorant L.R d n
theorem
EulerTransversePacketJoin.Budget.terminal_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.translate P a) ↑(forwardInitial τ hτ hτT B G).value)
n 0 ≤ EulerFixedEvolutionSobolev.traceCost τ * EulerGevrey.majorant L.R (d + 2) n
This is the actual datum passed to the forward solution, not a new hypothesis.
theorem
EulerTransversePacketJoin.Budget.past_velocity_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (pastVelocity τ hτ hτT B G))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₀ * EulerFixedEvolutionSobolev.traceCost τ * EulerGevrey.majorant L.R (d + 2) n
theorem
EulerTransversePacketJoin.Budget.past_derivative_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (pastDerivative τ hτ hτT B G))
n 0 ≤ (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₁ * EulerFixedEvolutionSobolev.traceCost τ + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₀) * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.future_velocity_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (futureVelocity τ hτ hτT B G)))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₀ * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.future_derivative_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (futureDerivative τ hτ hτT B G)))
n 0 ≤ EulerSourceCylinderTimeBounds.physicalCost ι q L.Ri L.C₀ L.C₁ 1 1 * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.velocity_unit_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (velocityPath τ hτ hτT B G)))
n 0 ≤ L.velocityCost * EulerGevrey.majorant L.R (d + 3) n
The entire constructed A/g, with the input's original external radius.
theorem
EulerTransversePacketJoin.Budget.derivative_unit_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (derivativePath τ hτ hτT B G)))
n 0 ≤ L.derivativeCost * EulerGevrey.majorant L.R (d + 3) n
The entire actual A_t/g. The profile itself is never differentiated.
Same-radius estimates for the actual corrector, divided by the prescribed time profile.
theorem
EulerTransversePacketJoin.potentialPath_normalized_bound
{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)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
(q : ℕ)
(Rc C R A : ℝ)
(hRc : 0 ≤ Rc)
(hC : 0 ≤ C)
(hA : 0 ≤ A)
(hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R)
(d : ℕ)
(hbA :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (velocityPath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(hbK :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (potentialPath τ hτ hτT B G)))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * (P * A) * EulerGevrey.majorant R d n
theorem
EulerTransversePacketJoin.potentialTimePath_normalized_bound
{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)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
(q : ℕ)
(Rc C R A : ℝ)
(hRc : 0 ≤ Rc)
(hC : 0 ≤ C)
(hA : 0 ≤ A)
(hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R)
(d : ℕ)
(hbA :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (velocityPath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(hbAt :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (derivativePath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(hbK :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(hbKt :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (potentialTimePath τ hτ hτT B G)))
n 0 ≤ 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * (P * A) * EulerGevrey.majorant R d n
theorem
EulerTransversePacketJoin.correctorPath_normalized_bound
{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)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
(q : ℕ)
(Rc C R A : ℝ)
(hRc : 0 ≤ Rc)
(hC : 0 ≤ C)
(hA : 0 ≤ A)
(hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R)
(d : ℕ)
(hbA :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (velocityPath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(hbK :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(hbI :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (correctorPath τ hτ hτT B G)))
n 0 ≤ 27 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C ^ 2 * (P * A) * EulerGevrey.majorant R (d + 1) n
theorem
EulerTransversePacketJoin.correctorTimePath_normalized_bound
{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)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
(q : ℕ)
(Rc C R A : ℝ)
(hRc : 0 ≤ Rc)
(hC : 0 ≤ C)
(hA : 0 ≤ A)
(hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R)
(d : ℕ)
(hbA :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (velocityPath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(hbAt :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (derivativePath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(hbK :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(hbKt :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(hbI :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(hbIt :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative) a‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (correctorTimePath τ hτ hτT B G)))
n 0 ≤ 108 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C ^ 2 * (P * A) * EulerGevrey.majorant R (d + 1) n
Restoring arbitrary forcing amplitudes by actual scalar homogeneity.
theorem
EulerTransversePacketProvider.amplitude_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : Data U}
{ι : Type u_2}
[Fintype ι]
(S :
{r : EulerPacketProfileRecursion.VectorField} →
Forcing P D r → C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hs :
∀ {r : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r),
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (S G))
(hm :
∀ {r r' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r) (H : Forcing P D r') (a : ℝ),
H.path = a • G.path → S H = a • S G)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(q : ℕ)
(R C : ℝ)
(d e : ℕ)
(hunit :
∀ {r : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r),
(∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (HistoryData.forcingPath G)))
n 0 ≤ EulerGevrey.majorant R d n) →
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (S G)))
n 0 ≤ C * EulerGevrey.majorant R e n)
{r : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D r)
(A : ℝ)
(hA : 0 ≤ A)
(hb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (S G)))
n 0 ≤ C * A * EulerGevrey.majorant R e n
A genuine homogeneous operator's unit-amplitude bound extends to every nonnegative amplitude without changing its radius or its derivative shifts.
The actual complete transverse inverse has one source-only radius budget. Its bounds are linear in the forcing amplitude and independent of grade.
theorem
EulerTransversePacketJoin.Budget.velocity_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (velocityPath τ hτ hτT B G)))
n 0 ≤ L.velocityCost * A * EulerGevrey.majorant L.R (d + 3) n
The genuine joined velocity divided by its actual piecewise profile.
theorem
EulerTransversePacketJoin.Budget.derivative_bound
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (derivativePath τ hτ hτT B G)))
n 0 ≤ L.derivativeCost * A * EulerGevrey.majorant L.R (d + 3) n
The genuine time derivative divided by the same profile, with no g derivative.
noncomputable def
EulerTransversePacketJoin.Budget.pressureAmplitude
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
:
Pressure amplitude, given by P*pressureCost (Fin 4) q N.Ri N.C N.C 1 L.commonCost.
Equations
- L.pressureAmplitude N = P * EulerSourceNormalResidualBounds.pressureCost (Fin 4) q N.Ri N.C N.C 1 L.commonCost
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.potentialAmplitude
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
:
Potential amplitude, given by 3*N.blockAmplitude*(P*L.commonCost).
Equations
- L.potentialAmplitude N = 3 * N.blockAmplitude * (P * L.commonCost)
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.potentialTimeAmplitude
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
:
Potential time amplitude, given by 6*N.blockAmplitude*(P*L.commonCost).
Equations
- L.potentialTimeAmplitude N = 6 * N.blockAmplitude * (P * L.commonCost)
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.correctorAmplitude
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
:
Corrector amplitude, given by 27*N.blockAmplitude^2*(P*L.commonCost).
Equations
- L.correctorAmplitude N = 27 * N.blockAmplitude ^ 2 * (P * L.commonCost)
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.correctorTimeAmplitude
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
:
Corrector time amplitude, given by 108*N.blockAmplitude^2*(P*L.commonCost).
Equations
- L.correctorTimeAmplitude N = 108 * N.blockAmplitude ^ 2 * (P * L.commonCost)
Instances For
theorem
EulerTransversePacketJoin.Budget.velocity_common_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (velocityPath τ hτ hτT B G)))
n 0 ≤ L.commonCost * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.derivative_common_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (derivativePath τ hτ hτT B G)))
n 0 ≤ L.commonCost * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.pressure_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (pressurePath τ hτ hτT B G)))
n 0 ≤ L.pressureAmplitude N * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.pressure_gradient_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (scalarGradientField τ hτ hτT B G).path))
n 0 ≤ 3 * L.pressureAmplitude N * A * EulerGevrey.majorant L.R (d + 4) n
theorem
EulerTransversePacketJoin.Budget.potential_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (potentialPath τ hτ hτT B G)))
n 0 ≤ L.potentialAmplitude N * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.potential_time_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (potentialTimePath τ hτ hτT B G)))
n 0 ≤ L.potentialTimeAmplitude N * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketJoin.Budget.corrector_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (correctorPath τ hτ hτT B G)))
n 0 ≤ L.correctorAmplitude N * A * EulerGevrey.majorant L.R (d + 4) n
theorem
EulerTransversePacketJoin.Budget.corrector_time_bound
{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τ ⋯)}
{q : ℕ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯)
(EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ A * EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.fullProfile ⋯) (correctorTimePath τ hτ hτT B G)))
n 0 ≤ L.correctorTimeAmplitude N * A * EulerGevrey.majorant L.R (d + 4) n
theorem
EulerPacketCylinderField.Field.WordBound.unscale_profile
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
(hT : 0 ≤ T)
(g : C(↑(Set.Icc 0 T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t)
(c : ℝ)
(hc : 0 < c)
{q d : ℕ}
{R A : ℝ}
(hG : (G.normalized hT (c • g) ⋯).WordBound q R A d)
:
(G.normalized hT g hg).WordBound q R (c * A) d
theorem
EulerPacketCylinderField.Field.WordBound.scale_profile
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
(hT : 0 ≤ T)
(g : C(↑(Set.Icc 0 T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t)
(c : ℝ)
(hc : 0 < c)
{q d : ℕ}
{R A : ℝ}
(hG : (G.normalized hT g hg).WordBound q R (A * c) d)
:
(G.normalized hT (c • g) ⋯).WordBound q R A d
theorem
EulerTransversePacketJoin.Budget.pressureAmplitude_nonneg
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
:
theorem
EulerTransversePacketJoin.Budget.correctorAmplitude_nonneg
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
:
theorem
EulerTransversePacketJoin.Budget.correctorTimeAmplitude_nonneg
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
:
structure
EulerTransversePacketJoin.Budget.GradeGuards
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
:
These four numerical guards depend only on the source data and the fixed external radius. They are chosen before the forcing, its amplitude or grade.
Instances For
theorem
EulerTransversePacketJoin.Budget.grade_bounds
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((vectorField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p) ∧ ((vectorDerivativeField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p) ∧ ((correctorField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p) ∧ ((correctorDerivativeField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p) ∧ ((scalarGradientField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
Actual A, A_t, curl corrector, its time derivative, and the literal scalar pressure gradient satisfy the unit grade budget with the same time profile.
theorem
EulerTransversePacketJoin.Budget.vector_grade_bound
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((vectorField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
theorem
EulerTransversePacketJoin.Budget.derivative_grade_bound
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((vectorDerivativeField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
theorem
EulerTransversePacketJoin.Budget.corrector_grade_bound
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((correctorField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
theorem
EulerTransversePacketJoin.Budget.corrector_derivative_grade_bound
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((correctorDerivativeField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
theorem
EulerTransversePacketJoin.Budget.pressure_gradient_grade_bound
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((scalarGradientField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)