Monotone enlargement of the actual source budgets and a common external radius for the mean, forced transverse and nonlinear packet estimates.
def
EulerMeanPacketProvider.Budget.enlargeRadius
{D : Data}
{q : ℕ}
{R : ℝ}
(M : Budget D q R)
(R' : ℝ)
(h : R ≤ R')
:
Budget D q R'
Only the three upper-radius guards change. Every coefficient, inverse constant, and actual source solver is preserved.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
EulerTransversePacketJoin.Budget.enlargeRadius
{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 : Budget D τ hτ hτT B ι q)
(R' : ℝ)
(h : L.R ≤ R')
:
Budget D τ hτ hτT B ι q
The homogeneous propagator, time profile and all source constants are unchanged. The five external-radius inequalities are monotone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
EulerTransversePacketJoin.Budget.enlargeRadius_R
{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 : Budget D τ hτ hτT B ι q)
(R' : ℝ)
(h : L.R ≤ R')
:
@[simp]
theorem
EulerTransversePacketJoin.Budget.enlargeRadius_fullProfile
{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 : Budget D τ hτ hτT B ι q)
(R' : ℝ)
(h : L.R ≤ R')
:
@[simp]
theorem
EulerTransversePacketJoin.Budget.enlargeRadius_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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
(R' : ℝ)
(h : L.R ≤ R')
:
def
EulerTransversePacketJoin.NormalBudget.enlargeRadius
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{q : ℕ}
{R : ℝ}
(N : NormalBudget D q R)
(R' : ℝ)
(h : R ≤ R')
:
NormalBudget D q R'
The normal inverse radius and the actual inverse-frame/strain jets stay fixed; only the target radius of their multiplier bound is enlarged.
Equations
Instances For
@[simp]
theorem
EulerTransversePacketJoin.Budget.enlargeRadius_pressureAmplitude
{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 : ℕ}
{P : ℝ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
(R' : ℝ)
(h : L.R ≤ R')
:
@[simp]
theorem
EulerTransversePacketJoin.Budget.enlargeRadius_correctorAmplitude
{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 : ℕ}
{P : ℝ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
(R' : ℝ)
(h : L.R ≤ R')
:
@[simp]
theorem
EulerTransversePacketJoin.Budget.enlargeRadius_correctorTimeAmplitude
{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 : ℕ}
{P : ℝ}
(L : Budget D τ hτ hτT B (Fin 4) q)
(N : NormalBudget D q L.R)
(R' : ℝ)
(h : L.R ≤ R')
:
theorem
EulerMeanPacketProvider.Budget.GradeGuards.enlargeRadius
{D : Data}
{R : ℝ}
{M : Budget D 6 R}
(W : M.GradeGuards)
(R' : ℝ)
(h : R ≤ R')
:
(M.enlargeRadius R' h).GradeGuards
theorem
EulerTransversePacketJoin.Budget.GradeGuards.enlargeRadius
{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 : Budget D τ hτ hτT B (Fin 4) 6}
{N : NormalBudget D 6 L.R}
(W : L.GradeGuards N)
(R' : ℝ)
(h : L.R ≤ R')
:
(L.enlargeRadius R' h).GradeGuards (N.enlargeRadius R' h)
noncomputable def
EulerPacketCommonRadius.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}
{τ : ℝ}
{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)
(CB : EulerPacketCylinderField.CoefficientBudget C)
:
Every summand is a fixed source quantity. There is no occurrence of the new target radius, the forcing amplitude, or the recursive grade on the right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCommonRadius.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}
{τ : ℝ}
{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)
(CB : EulerPacketCylinderField.CoefficientBudget C)
:
Rm ≤ commonRadius M L N CB ∧ L.R ≤ commonRadius M L N CB ∧ CB.termCost ≤ commonRadius M L N CB ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) CB.Rc ≤ commonRadius M L N CB ∧ M.velocityCost ≤ commonRadius M L N CB ∧ M.derivativeCost ≤ commonRadius M L N CB ∧ M.pressureGradientCost ≤ commonRadius M L N CB ∧ L.commonCost ≤ commonRadius M L N CB ∧ L.correctorAmplitude N ≤ commonRadius M L N CB ∧ L.correctorTimeAmplitude N ≤ commonRadius M L N CB ∧ 3 * L.pressureAmplitude N ≤ commonRadius M L N CB
theorem
EulerPacketCommonRadius.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}
{τ : ℝ}
{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)
(CB : EulerPacketCylinderField.CoefficientBudget C)
(R' : ℝ)
(h : commonRadius M L N CB ≤ R')
:
∃ (hM : Rm ≤ R') (hL : L.R ≤ R'),
(M.enlargeRadius R' hM).GradeGuards ∧ (L.enlargeRadius R' hL).GradeGuards (N.enlargeRadius R' hL) ∧ CB.termCost ≤ R' ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) CB.Rc ≤ R'
Every target radius at least this fixed threshold allows the actual enlarged budgets, with their original source constants and time profile.
theorem
EulerPacketCommonRadius.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}
{τ : ℝ}
{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)
(CB : EulerPacketCylinderField.CoefficientBudget C)
:
∃ (R' : ℝ) (hM : Rm ≤ R') (hL : L.R ≤ R'),
(M.enlargeRadius R' hM).GradeGuards ∧ (L.enlargeRadius R' hL).GradeGuards (N.enlargeRadius R' hL) ∧ CB.termCost ≤ R' ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) CB.Rc ≤ R'
Concrete source-preserving rebudgeting at one common radius closes all linear grade guards and the nonlinear coefficient/finite-sum guards.