A uniform polynomial bound for the actual initialized common radius. Primitive scalar bounds are stated explicitly, including the original source radii; later source constructors discharge them polynomially.
The literal common radius of the initialized packet, with named budgets that retain it. Quantitative bounds must concern this radius, rather than an arbitrary witness of a radius-existence theorem.
@[reducible, inline]
noncomputable abbrev
EulerPacketTerminalDatum.primaryRadiusBudget
{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)
(δ : ℝ)
:
EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6
Primary radius budget: an abbreviation for EulerTransversePacketPrimary.enlargeForPrimary L (wordRadius (Fin 4) δ).
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
EulerPacketTerminalDatum.primaryRadiusNormal
{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)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(δ : ℝ)
:
Primary radius normal: an abbreviation for NB.enlargeRadius (primaryRadiusBudget L δ).R (EulerTransversePacketPrimary.le_requiredRadius L _).
Equations
Instances For
@[reducible, inline]
abbrev
EulerPacketTerminalDatum.primaryRadiusPrimary
{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)
(δ : ℝ)
:
Primary radius primary: an abbreviation for EulerTransversePacketPrimary.requiredBudget L (wordRadius (Fin 4) δ).
Equations
- ⋯ = ⋯
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedRadius
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
Initialized radius, constructed using max.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.primary_le_initializedRadius
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
theorem
EulerPacketTerminalDatum.mean_le_initializedRadius
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
noncomputable def
EulerPacketTerminalDatum.initializedJoinedBudget
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6
Initialized joined budget, given by (primaryRadiusBudget L δ).enlargeRadius (initializedRadius LM L NB BC δ ξ) (primary_le_initializedRadius LM L NB BC δ ξ).
Equations
- EulerPacketTerminalDatum.initializedJoinedBudget LM L NB BC δ ξ = (EulerPacketTerminalDatum.primaryRadiusBudget L δ).enlargeRadius (EulerPacketTerminalDatum.initializedRadius LM L NB BC δ ξ) ⋯
Instances For
theorem
EulerPacketTerminalDatum.initializedPrimaryBudget
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
EulerTransversePacketPrimary.Budget (initializedJoinedBudget LM L NB BC δ ξ)
noncomputable def
EulerPacketTerminalDatum.initializedNormalBudget
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
EulerTransversePacketJoin.NormalBudget D 6 (initializedRadius LM L NB BC δ ξ)
Initialized normal budget, given by (primaryRadiusNormal L NB δ).enlargeRadius (initializedRadius LM L NB BC δ ξ) (primary_le_initializedRadius LM L NB BC δ ξ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedMeanBudget
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
EulerMeanPacketProvider.Budget M 6 (initializedRadius LM L NB BC δ ξ)
Initialized mean budget, given by LM.enlargeRadius (initializedRadius LM L NB BC δ ξ) (mean_le_initializedRadius LM L NB BC δ ξ).
Equations
- EulerPacketTerminalDatum.initializedMeanBudget LM L NB BC δ ξ = LM.enlargeRadius (EulerPacketTerminalDatum.initializedRadius LM L NB BC δ ξ) ⋯
Instances For
@[simp]
theorem
EulerPacketTerminalDatum.initializedJoinedBudget_radius
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
@[simp]
theorem
EulerPacketTerminalDatum.initializedJoinedBudget_profile
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
theorem
EulerPacketTerminalDatum.initializedRadius_guards
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
(initializedJoinedBudget LM L NB BC δ ξ).GradeGuards (initializedNormalBudget LM L NB BC δ ξ) ∧ (initializedMeanBudget LM L NB BC δ ξ).GradeGuards ∧ ⋯.GradeGuards (initializedNormalBudget LM L NB BC δ ξ) (wordCost (Fin 4) 6 δ * ‖ξ‖) ∧ wordRadius (Fin 4) δ ≤ initializedRadius LM L NB BC δ ξ ∧ BC.termCost ≤ initializedRadius LM L NB BC δ ξ ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ initializedRadius LM L NB BC δ ξ
All the actual constructed budgets use the named canonical radius. The profile and every coefficient cost are unchanged by enlargement.
theorem
EulerPacketRadiusPolynomial.joined_inverseRadius_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τ ⋯)}
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
:
theorem
EulerPacketRadiusPolynomial.endpointForcing_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hτi : τ⁻¹ ≤ W)
(hRc : L.Rc ≤ W)
(hC1 : L.C₁ ≤ W)
:
theorem
EulerPacketRadiusPolynomial.primary_weak_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hτi : τ⁻¹ ≤ W)
(hci : (D.initial τ hτ ⋯).frameLower⁻¹ ≤ W)
(hRc : L.Rc ≤ W)
(hC0 : L.C₀ ≤ W)
(hC1 : L.C₁ ≤ W)
(hCH : L.CH ≤ W)
:
theorem
EulerPacketRadiusPolynomial.primary_gram_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hτi : τ⁻¹ ≤ W)
(hci : (D.initial τ hτ ⋯).frameLower⁻¹ ≤ W)
(hRc : L.Rc ≤ W)
(hC0 : L.C₀ ≤ W)
(hC1 : L.C₁ ≤ W)
(V : ℝ)
(hV : 0 ≤ V)
(hVW : V ≤ 2 * W + 2)
:
EulerTimeLpGramSobolev.gramBlockCost (Fin 4) 6 (D.initial τ hτ ⋯).frameLower L.Rc L.C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude (Fin 4) 6 L.Rc L.C₀ L.C₁
(EulerCylinderDirichlet.Coefficients.endpointForcingCost (Fin 4) 6 τ L.Rc L.C₁) V) ≤ strongEnvelope W
theorem
EulerPacketRadiusPolynomial.primary_forward_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hT : D.T ≤ 1)
(hτi : τ⁻¹ ≤ W)
(hC0 : L.C₀ ≤ W)
(hC1 : L.C₁ ≤ W)
(hC : L.C ≤ W)
(hRi : L.Ri ≤ W)
:
theorem
EulerPacketRadiusPolynomial.requiredEnvelope_bounds
(W : ℝ)
(hW : 0 ≤ W)
:
W ≤ requiredEnvelope W ∧ 16 * jetEnvelope W ≤ requiredEnvelope W ∧ 2 * weakEnvelope W * (16 * W + 1) ≤ requiredEnvelope W ∧ 2 * strongEnvelope W * (16 * W + 1) ≤ requiredEnvelope W ∧ 2 * forwardEnvelope W * (64 * W + 1) ≤ requiredEnvelope W
theorem
EulerPacketRadiusPolynomial.primary_required_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hT : D.T ≤ 1)
(hτi : τ⁻¹ ≤ W)
(hci : (D.initial τ hτ ⋯).frameLower⁻¹ ≤ W)
(hRc : L.Rc ≤ W)
(hC0 : L.C₀ ≤ W)
(hC1 : L.C₁ ≤ W)
(hCH : L.CH ≤ W)
(hC : L.C ≤ W)
(hRi : L.Ri ≤ W)
(hR : L.R ≤ W)
(δ : ℝ)
(hδ : 0 < δ)
(hi : δ⁻¹ ≤ W)
:
theorem
EulerPacketRadiusPolynomial.joined_common_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hτi : τ⁻¹ ≤ W)
(hRc : L.Rc ≤ W)
(hC0 : L.C₀ ≤ W)
(hC1 : L.C₁ ≤ W)
(hRi : L.Ri ≤ W)
:
theorem
EulerPacketRadiusPolynomial.primary_common_le
{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)
(W : ℝ)
(hW : 1 ≤ W)
(hτi : τ⁻¹ ≤ W)
(hRc : L.Rc ≤ W)
(hC0 : L.C₀ ≤ W)
(hC1 : L.C₁ ≤ W)
(hRi : L.Ri ≤ W)
(H : EulerTransversePacketPrimary.Budget L)
:
theorem
EulerPacketRadiusPolynomial.normal_block_le
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{qR : ℝ}
(N : EulerTransversePacketJoin.NormalBudget D 6 qR)
(W : ℝ)
(hW : 0 ≤ W)
(hNR : N.Rc ≤ W)
(hNC : N.C ≤ W)
(hNI : N.Ri ≤ W)
:
theorem
EulerPacketRadiusPolynomial.joined_grade_sum_le
{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)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : ℝ)
(hW : 0 ≤ W)
(hNR : N.Rc ≤ W)
(hNC : N.C ≤ W)
(hNI : N.Ri ≤ W)
(hcommon : L.commonCost ≤ commonEnvelope W)
:
L.commonCost + L.correctorAmplitude N + L.correctorTimeAmplitude N + 3 * L.pressureAmplitude N ≤ gradeEnvelope W
theorem
EulerPacketRadiusPolynomial.primary_grade_sum_le
{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)
(W : ℝ)
(hW : 0 ≤ W)
(hNR : N.Rc ≤ W)
(hNC : N.C ≤ W)
(hNI : N.Ri ≤ W)
(hcommon : H.commonCost ≤ commonEnvelope W)
:
H.commonCost + H.correctorAmplitude N + H.correctorTimeAmplitude N + 3 * H.pressureAmplitude N ≤ gradeEnvelope W
theorem
EulerPacketRadiusPolynomial.terminal_cost_le
{U : Type u_1}
[NormedAddCommGroup U]
(δ W : ℝ)
(ξ : U)
(hδ : 0 < δ)
(hi : δ⁻¹ ≤ W)
(hξ : ‖ξ‖ ≤ W)
:
structure
EulerPacketRadiusPolynomial.RadiusPrimitives
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
(W : ℝ)
:
Scalar leaves of the actual source budgets. The original source radii are included; the new canonical radius is not an input.
Instances For
theorem
EulerPacketRadiusPolynomial.initializedRadius_le_envelope
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
(W : ℝ)
(hδ : 0 < δ)
(H : RadiusPrimitives LM L NB BC δ ξ W)
:
theorem
EulerPacketRadiusPolynomial.initializedRadius_power
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
(W : ℝ)
(hδ : 0 < δ)
(H : RadiusPrimitives LM L NB BC δ ξ W)
: