The actual primary closes the first packet grade. Its terminal scalar amplitude is canceled against the actual time profile, and only fixed source costs are absorbed into the radius.
Same-radius estimates for the actual corrector, divided by the prescribed time profile.
Unit-terminal-data estimates for the actual joined primary. The same external radius controls its history, actual trace, and weighted future.
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y).value)
n 0 ≤ H.endpointBudget.coordinateCost * EulerGevrey.majorant L.R (d + 2) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y))
n 0 ≤ H.endpointBudget.velocityCost * EulerGevrey.majorant L.R (d + 2) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y))
n 0 ≤ H.endpointBudget.derivativeCost * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₀ * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ EulerSourceCylinderTimeBounds.physicalCost ι q L.Ri L.C₀ L.C₁ 0 1 * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.velocityCost * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.derivativeCost * EulerGevrey.majorant L.R (d + 3) n
Unit-data estimates extend to arbitrary actual terminal amplitudes at the same radius.
theorem
EulerTransversePacketProvider.initial_amplitude_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
{V : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{D : Data U}
{ι : Type u_3}
[Fintype ι]
(S : InitialData P D → C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P V)))
(hs :
∀ (Y : InitialData P D),
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (S Y))
(hm : ∀ (Y Z : InitialData P D) (a : ℝ), Z.value = a • Y.value → S Z = a • S Y)
(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 :
∀ (Y : InitialData P D),
(∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ C * EulerGevrey.majorant R e n)
(Y : InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(hb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ C * A * EulerGevrey.majorant R e n
The actual primary A/g and A_t/g retain one fixed mixed Sobolev radius. The constants and guards depend only on source coefficients, the history length and the genuine propagator bound. Arbitrary terminal amplitude is restored by the proved exact homogeneity of the constructed solution.
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.velocityCost * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.derivativeCost * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(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 Y)))
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 Y)))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * (P * A) * EulerGevrey.majorant R d n
theorem
EulerTransversePacketPrimary.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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(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 Y)))
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 Y)))
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 Y)))
n 0 ≤ 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * (P * A) * EulerGevrey.majorant R d n
theorem
EulerTransversePacketPrimary.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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(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 Y)))
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 Y)))
n 0 ≤ 27 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C ^ 2 * (P * A) * EulerGevrey.majorant R (d + 1) n
theorem
EulerTransversePacketPrimary.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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(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 Y)))
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 Y)))
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 Y)))
n 0 ≤ 108 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C ^ 2 * (P * A) * EulerGevrey.majorant R (d + 1) n
theorem
EulerTransversePacketPrimary.Budget.derivativeCost_nonneg
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
:
noncomputable def
EulerTransversePacketPrimary.Budget.commonCost
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
:
Common cost, given by H.velocityCost+H.derivativeCost.
Equations
- H.commonCost = H.velocityCost + H.derivativeCost
Instances For
noncomputable def
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
Pressure amplitude, given by P*pressureCost (Fin 4) q N.Ri N.C N.C 0 H.commonCost.
Equations
- H.pressureAmplitude N = P * EulerSourceNormalResidualBounds.pressureCost (Fin 4) q N.Ri N.C N.C 0 H.commonCost
Instances For
noncomputable def
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
Potential amplitude, given by 3*N.blockAmplitude*(P*H.commonCost).
Equations
- H.potentialAmplitude N = 3 * N.blockAmplitude * (P * H.commonCost)
Instances For
noncomputable def
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
Potential time amplitude, given by 6*N.blockAmplitude*(P*H.commonCost).
Equations
- H.potentialTimeAmplitude N = 6 * N.blockAmplitude * (P * H.commonCost)
Instances For
noncomputable def
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
Corrector amplitude, given by 27*N.blockAmplitude^2*(P*H.commonCost).
Equations
- H.correctorAmplitude N = 27 * N.blockAmplitude ^ 2 * (P * H.commonCost)
Instances For
noncomputable def
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
Corrector time amplitude, given by 108*N.blockAmplitude^2*(P*H.commonCost).
Equations
- H.correctorTimeAmplitude N = 108 * N.blockAmplitude ^ 2 * (P * H.commonCost)
Instances For
theorem
EulerTransversePacketPrimary.Budget.commonCost_nonneg
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
:
theorem
EulerTransversePacketPrimary.Budget.velocityCost_le_common
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
:
theorem
EulerTransversePacketPrimary.Budget.derivativeCost_le_common
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
:
theorem
EulerTransversePacketPrimary.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τ ⋯)}
{q : ℕ}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
theorem
EulerTransversePacketPrimary.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τ ⋯)}
{q : ℕ}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
theorem
EulerTransversePacketPrimary.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τ ⋯)}
{q : ℕ}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
:
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.commonCost * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.commonCost * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.pressureAmplitude N * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y).path))
n 0 ≤ 3 * H.pressureAmplitude N * A * EulerGevrey.majorant L.R (d + 4) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.potentialAmplitude N * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.potentialTimeAmplitude N * A * EulerGevrey.majorant L.R (d + 3) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.correctorAmplitude N * A * EulerGevrey.majorant L.R (d + 4) n
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D q L.R)
(Y : EulerTransversePacketProvider.InitialData P D)
(A : ℝ)
(hA : 0 ≤ A)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) 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 Y)))
n 0 ≤ H.correctorTimeAmplitude N * A * EulerGevrey.majorant L.R (d + 4) n
structure
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
:
C bounds the unmultiplied terminal datum. No guard involves the scalar amplitude α, and the original radius is retained.
Instances For
theorem
EulerTransversePacketPrimary.Budget.grade_fields
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : H.GradeGuards N C)
(Y : EulerTransversePacketProvider.InitialData P D)
(α : ℝ)
(hα : 0 < α)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) n 0 ≤ α * C * EulerGevrey.majorant L.R 0 n)
:
((vectorField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1) ∧ ((vectorDerivativeField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1) ∧ ((correctorField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1) ∧ ((correctorDerivativeField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1) ∧ ((scalarGradientField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1)
theorem
EulerTransversePacketPrimary.Budget.profile_budget
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : H.GradeGuards N C)
(Y : EulerTransversePacketProvider.InitialData P D)
(α : ℝ)
(hα : 0 < α)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) n 0 ≤ α * C * EulerGevrey.majorant L.R 0 n)
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector P)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T))
(hgrowth : S.growth = α • L.fullProfile)
:
EulerPacketCylinderField.ProfileBudget (profileRegularity τ hτ hτT B Y O hcorrector) S L.R 1
theorem
EulerPacketTerminalDatum.scaled_initialData_bound
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.translate period a) ↑(initialData D δ hδ (α • ξ) hs).value)
n 0 ≤ α * (wordCost (Fin 4) 6 δ * ‖ξ‖) * EulerGevrey.majorant L.R 0 n
theorem
EulerPacketTerminalDatum.primary_profile_budget
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : EulerTransversePacketPrimary.Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(W : H.GradeGuards N (wordCost (Fin 4) 6 δ * ‖ξ‖))
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector period)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T))
(hgrowth : S.growth = α • L.fullProfile)
:
EulerPacketCylinderField.ProfileBudget
(EulerTransversePacketPrimary.profileRegularity τ hτ hτT B (initialData D δ hδ (α • ξ) hs) O hcorrector) S L.R 1
The literal α χ₁ fδ ξT terminal datum supplies the required primary profile budget, with every terminal jet estimate discharged.