The chosen geometric growth profile carries a polynomial amplitude bound. This controls the actual grade scale, including its history part.
theorem
EulerPacketSourceGeometry.ParentFrame.rayScale_inv_le_frameBound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
(P : ParentFrame D τ)
(hτ : 0 < τ)
(hτT : τ < D.T)
:
theorem
EulerPacketSourceGeometry.Guards.sourceGrowthProfile_amplitude_frame
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{P : ParentFrame D τ}
{H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
(J : Guards hτ hτT P H)
(hball : 1 / 2 ≤ J.radius)
(t : ↑(Set.Icc 0 (D.T - τ)))
:
J.primaryAmplitude hball * (J.sourceGrowthProfile hball) t ≤ 8 * Real.exp 6 * J.δ * J.hchild * D.frameBound
theorem
EulerPacketSourceGeometry.Guards.budget_fullProfile_amplitude
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{P : ParentFrame D τ}
{H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
(J : Guards hτ hτT P H)
(hball : 1 / 2 ≤ J.radius)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) 6)
(hg : L.g = J.sourceGrowthProfile hball)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerPacketSourceGeometry.Guards.budget_H0_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{P : ParentFrame D τ}
{H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
(J : Guards hτ hτT P H)
(hball : 1 / 2 ≤ J.radius)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) 6)
(hg : L.g = J.sourceGrowthProfile hball)
{T' : ℝ}
(hTime : D.T = T')
(hδ : 0 < J.δ)
(hh : 0 < J.hchild)
:
(EulerPacketTimeProfile.Scales.ofTimeProfile L.fullProfile ⋯ hTime (J.primaryAmplitude hball) ⋯).H0 ≤ max 1 (8 * Real.exp 6 * J.δ * J.hchild * (1 + L.C₀))
theorem
EulerPacketSourceGeometry.ForwardGuards.budget_profile_amplitude
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(J : ForwardGuards P)
(hball : 1 / 2 ≤ J.radius)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(hg : L.g = J.sourceGrowthProfile hball)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerPacketSourceGeometry.ForwardGuards.budget_H0_bound
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(J : ForwardGuards P)
(hball : 1 / 2 ≤ J.radius)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(hg : L.g = J.sourceGrowthProfile hball)
{T' : ℝ}
(hTime : D.T = T')
(hδ : 0 < J.δ)
(hh : 0 < J.hchild)
: