The primary grade imposes only finitely many fixed lower bounds on the external radius. Enlarging it leaves the time profile and every source cost unchanged, including the terminal amplitude before its scalar multiplier.
The additional primary guards can be met by one explicit enlargement of the common external radius. Neither source coefficients nor profile costs are changed. The extra lower bound can include the actual terminal-wave radius, before the recursive solve begins.
noncomputable def
EulerTransversePacketPrimary.weakRadius
{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)
:
Weak radius as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketPrimary.strongRadius
{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)
:
Strong radius as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketPrimary.uniformRadius
{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)
:
Uniform radius as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketPrimary.forwardRadius
{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)
:
Forward radius as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketPrimary.requiredRadius
{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)
(extra : ℝ)
:
Required radius, given by max extra (max L.R (max (weakRadius L) (max (strongRadius L) (max (uniformRadius L) (forwardRadius L))))).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketPrimary.le_requiredRadius
{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)
(extra : ℝ)
:
theorem
EulerTransversePacketPrimary.extra_le_requiredRadius
{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)
(extra : ℝ)
:
noncomputable def
EulerTransversePacketPrimary.enlargeForPrimary
{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)
(extra : ℝ)
:
EulerTransversePacketJoin.Budget D τ hτ hτT B ι q
Enlarge for primary, given by L.enlargeRadius (requiredRadius L extra) (le_requiredRadius L extra).
Equations
Instances For
theorem
EulerTransversePacketPrimary.requiredBudget
{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)
(extra : ℝ)
:
Budget (enlargeForPrimary L extra)
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B ι q}
(H : Budget L)
(R' : ℝ)
(hR : L.R ≤ R')
:
Budget (L.enlargeRadius R' hR)
@[simp]
theorem
EulerTransversePacketPrimary.Budget.enlargeRadius_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)
(R' : ℝ)
(hR : L.R ≤ R')
:
@[simp]
theorem
EulerTransversePacketPrimary.Budget.enlargeRadius_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)
(R' : ℝ)
(hR : L.R ≤ R')
:
noncomputable def
EulerTransversePacketPrimary.Budget.gradeRadius
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
:
Grade radius, constructed using max.
Equations
- H.gradeRadius N C = max L.R (max (H.commonCost * C) (max (H.correctorAmplitude N * C) (max (H.correctorTimeAmplitude N * C) (3 * H.pressureAmplitude N * C))))
Instances For
theorem
EulerTransversePacketPrimary.Budget.gradeRadius_bounds
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
:
L.R ≤ H.gradeRadius N C ∧ H.commonCost * C ≤ H.gradeRadius N C ∧ H.correctorAmplitude N * C ≤ H.gradeRadius N C ∧ H.correctorTimeAmplitude N * C ≤ H.gradeRadius N C ∧ 3 * H.pressureAmplitude N * C ≤ H.gradeRadius N C
theorem
EulerTransversePacketPrimary.Budget.gradeRadius_guards
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(hC : 0 ≤ C)
(R' : ℝ)
(hR : H.gradeRadius N C ≤ R')
:
∃ (h : L.R ≤ R'), ⋯.GradeGuards (N.enlargeRadius R' h) C
theorem
EulerTransversePacketPrimary.Budget.exists_grade_radius
{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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(hC : 0 ≤ C)
(extra : ℝ)
:
∃ (R' : ℝ), extra ≤ R' ∧ ∃ (h : L.R ≤ R'), ⋯.GradeGuards (N.enlargeRadius R' h) C
An arbitrary extra requirement can be included without changing any source cost or the primary time profile.
theorem
EulerTransversePacketPrimary.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 : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
{H : Budget L}
{N : EulerTransversePacketJoin.NormalBudget D 6 L.R}
{C : ℝ}
(W : H.GradeGuards N C)
(R' : ℝ)
(h : L.R ≤ R')
:
⋯.GradeGuards (N.enlargeRadius R' h) C