Named direct-forward budgets at the literal canonical source radius.
@[reducible, inline]
noncomputable abbrev
EulerPacketTerminalDatum.forwardInitializedRadius
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
Forward initialized radius: an abbreviation for EulerPacketForwardRadius.canonicalRadius L LM NB BC δ ξ.
Equations
- EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ = EulerPacketForwardRadius.canonicalRadius L LM NB BC δ ξ
Instances For
theorem
EulerPacketTerminalDatum.forward_le_initializedRadius
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
theorem
EulerPacketTerminalDatum.mean_le_forwardInitializedRadius
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
noncomputable def
EulerPacketTerminalDatum.forwardInitializedLinearBudget
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
Forward initialized linear budget, given by L.enlargeRadius (forwardInitializedRadius LM L NB BC δ ξ) (forward_le_initializedRadius LM L NB BC δ ξ).
Equations
- EulerPacketTerminalDatum.forwardInitializedLinearBudget LM L NB BC δ ξ = L.enlargeRadius (EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ) ⋯
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedNormalBudget
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
EulerTransversePacketJoin.NormalBudget D 6 (forwardInitializedRadius LM L NB BC δ ξ)
Forward initialized normal budget, given by NB.enlargeRadius (forwardInitializedRadius LM L NB BC δ ξ) (forward_le_initializedRadius LM L NB BC δ ξ).
Equations
- EulerPacketTerminalDatum.forwardInitializedNormalBudget LM L NB BC δ ξ = NB.enlargeRadius (EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ) ⋯
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedMeanBudget
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
EulerMeanPacketProvider.Budget M 6 (forwardInitializedRadius LM L NB BC δ ξ)
Forward initialized mean budget, given by LM.enlargeRadius (forwardInitializedRadius LM L NB BC δ ξ) (mean_le_forwardInitializedRadius LM L NB BC δ ξ).
Equations
- EulerPacketTerminalDatum.forwardInitializedMeanBudget LM L NB BC δ ξ = LM.enlargeRadius (EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ) ⋯
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedRadius_guards
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
(forwardInitializedLinearBudget LM L NB BC δ ξ).GradeGuards (forwardInitializedNormalBudget LM L NB BC δ ξ) 1 ∧ (forwardInitializedMeanBudget LM L NB BC δ ξ).GradeGuards ∧ (forwardInitializedLinearBudget LM L NB BC δ ξ).GradeGuards (forwardInitializedNormalBudget LM L NB BC δ ξ)
(wordCost (Fin 4) 6 δ * ‖ξ‖) ∧ wordRadius (Fin 4) δ ≤ forwardInitializedRadius LM L NB BC δ ξ ∧ BC.termCost ≤ forwardInitializedRadius LM L NB BC δ ξ ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ forwardInitializedRadius LM L NB BC δ ξ