Additional source-only radius guards for the primary endpoint history. The forced-profile budget supplies the original coefficient and propagator bounds. These extra guards use only the unit terminal-data cost, never the terminal amplitude or a recursive derivative shift.
structure
EulerTransversePacketPrimary.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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q)
:
Budget data, collecting history_weak, history_strong, history_uniform,
forward_radius.
- history_weak : 2 * EulerTransverseFixedSobolev.blockCost ι q τ L.Rc L.C₀ L.C₁ L.CH (D.initial τ hτ ⋯).frameLower (EulerCylinderDirichlet.Coefficients.endpointForcingCost ι q τ L.Rc L.C₁) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι L.Rc + 1) ≤ L.R
- history_strong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (D.initial τ hτ ⋯).frameLower L.Rc L.C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q L.Rc L.C₀ L.C₁ (EulerCylinderDirichlet.Coefficients.endpointForcingCost ι q τ L.Rc L.C₁) 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι L.Rc + 1) ≤ L.R
- history_uniform : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (D.initial τ hτ ⋯).frameLower L.Rc L.C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q L.Rc L.C₀ L.C₁ (EulerCylinderDirichlet.Coefficients.endpointForcingCost ι q τ L.Rc L.C₁) (EulerFixedEvolutionSobolev.traceCost τ)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι L.Rc + 1) ≤ L.R
- forward_radius : 2 * EulerLinearDuhamel.forwardSobolevCost ι q (D.T - τ) L.C (τ⁻¹ + EulerFixedEvolutionSobolev.traceCost τ) (EulerSourceCylinderForwardSobolev.forcingCost ι q L.Ri L.C₀ * 0) (18 * L.Ri * L.C₀ * L.C₁) (4 * L.Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * L.Ri) + 1) ≤ L.R
Instances For
def
EulerTransversePacketPrimary.Budget.endpointBudget
{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)
:
B.coefficients.EndpointBudget ι q
Endpoint budget, bundling Rc, C₀, C₁, CH and the required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketPrimary.Budget.velocityCost
{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)
:
Velocity cost, given by H.endpointBudget.velocityCost + 3*sobolevCoefficientAmplitude ι q L.Rc L.C₀.
Equations
Instances For
noncomputable def
EulerTransversePacketPrimary.Budget.derivativeCost
{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)
:
Derivative cost, given by H.endpointBudget.derivativeCost + physicalCost ι q L.Ri L.C₀ L.C₁ 0 1.
Equations
- H.derivativeCost = H.endpointBudget.derivativeCost + EulerSourceCylinderTimeBounds.physicalCost ι q L.Ri L.C₀ L.C₁ 0 1
Instances For
theorem
EulerTransversePacketPrimary.Budget.velocityCost_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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
: