One finite source radius accommodates the zero-history primary, every forced direct-forward grade, the mean solve and the nonlinear coefficients. Neither the positive packet amplitude nor the recursive grade enters it.
def
EulerTransversePacketForward.Budget.gradeRadius
{P : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
:
Grade radius, constructed using max.
Equations
- L.gradeRadius N C = max L.R (max (L.commonCost * C) (max (L.correctorAmplitude N * C) (max (L.correctorTimeAmplitude N * C) (3 * L.pressureAmplitude N * C))))
Instances For
theorem
EulerTransversePacketForward.Budget.gradeRadius_bounds
{P : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
:
L.R ≤ L.gradeRadius N C ∧ L.commonCost * C ≤ L.gradeRadius N C ∧ L.correctorAmplitude N * C ≤ L.gradeRadius N C ∧ L.correctorTimeAmplitude N * C ≤ L.gradeRadius N C ∧ 3 * L.pressureAmplitude N * C ≤ L.gradeRadius N C
theorem
EulerTransversePacketForward.Budget.gradeRadius_guards
{P : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(hC : 0 ≤ C)
(R' : ℝ)
(hR : L.gradeRadius N C ≤ R')
:
∃ (h : L.R ≤ R'), (L.enlargeRadius R' h).GradeGuards (N.enlargeRadius R' h) C
theorem
EulerTransversePacketForward.Budget.exists_grade_radius
{P : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(hC : 0 ≤ C)
(extra : ℝ)
:
∃ (R' : ℝ), extra ≤ R' ∧ ∃ (h : L.R ≤ R'), (L.enlargeRadius R' h).GradeGuards (N.enlargeRadius R' h) C
noncomputable def
EulerPacketForwardCommonRadius.commonRadius
{P Tc : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData P Tc O}
{DM : EulerMeanPacketProvider.Data}
{Rm : ℝ}
(M : EulerMeanPacketProvider.Budget DM 6 Rm)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(CB : EulerPacketCylinderField.CoefficientBudget C)
(terminalCost extra : ℝ)
:
Common radius as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketForwardCommonRadius.commonRadius_bounds
{P Tc : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData P Tc O}
{DM : EulerMeanPacketProvider.Data}
{Rm : ℝ}
(M : EulerMeanPacketProvider.Budget DM 6 Rm)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(CB : EulerPacketCylinderField.CoefficientBudget C)
(terminalCost extra : ℝ)
:
Rm ≤ commonRadius M L N CB terminalCost extra ∧ L.R ≤ commonRadius M L N CB terminalCost extra ∧ CB.termCost ≤ commonRadius M L N CB terminalCost extra ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) CB.Rc ≤ commonRadius M L N CB terminalCost extra ∧ M.velocityCost ≤ commonRadius M L N CB terminalCost extra ∧ M.derivativeCost ≤ commonRadius M L N CB terminalCost extra ∧ M.pressureGradientCost ≤ commonRadius M L N CB terminalCost extra ∧ L.gradeRadius N 1 ≤ commonRadius M L N CB terminalCost extra ∧ L.gradeRadius N terminalCost ≤ commonRadius M L N CB terminalCost extra ∧ extra ≤ commonRadius M L N CB terminalCost extra
theorem
EulerPacketForwardCommonRadius.commonRadius_guards
{P Tc : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData P Tc O}
{DM : EulerMeanPacketProvider.Data}
{Rm : ℝ}
(M : EulerMeanPacketProvider.Budget DM 6 Rm)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(CB : EulerPacketCylinderField.CoefficientBudget C)
(terminalCost extra : ℝ)
(hC : 0 ≤ terminalCost)
(R' : ℝ)
(hR : commonRadius M L N CB terminalCost extra ≤ R')
:
∃ (hM : Rm ≤ R') (hL : L.R ≤ R'),
(M.enlargeRadius R' hM).GradeGuards ∧ (L.enlargeRadius R' hL).GradeGuards (N.enlargeRadius R' hL) 1 ∧ (L.enlargeRadius R' hL).GradeGuards (N.enlargeRadius R' hL) terminalCost ∧ CB.termCost ≤ R' ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) CB.Rc ≤ R' ∧ extra ≤ R'
theorem
EulerPacketForwardCommonRadius.exists_common_radius
{P Tc : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData P Tc O}
{DM : EulerMeanPacketProvider.Data}
{Rm : ℝ}
(M : EulerMeanPacketProvider.Budget DM 6 Rm)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(CB : EulerPacketCylinderField.CoefficientBudget C)
(terminalCost extra : ℝ)
(hC : 0 ≤ terminalCost)
:
∃ (R' : ℝ) (hM : Rm ≤ R') (hL : L.R ≤ R'),
(M.enlargeRadius R' hM).GradeGuards ∧ (L.enlargeRadius R' hL).GradeGuards (N.enlargeRadius R' hL) 1 ∧ (L.enlargeRadius R' hL).GradeGuards (N.enlargeRadius R' hL) terminalCost ∧ CB.termCost ≤ R' ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) CB.Rc ≤ R' ∧ extra ≤ R'