The source growth profile is selected together with its amplitude bound. Keeping both properties in the choice specification is necessary for a uniform source-frequency estimate.
theorem
EulerPacketGeometrySourceGrowth.growthProfile_amplitude_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
{Ω : Set EulerSmoothLimit.Space}
(G : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // x ∈ Ω })
{F F₁ Z Z₁ : ℝ → ℝ}
(H : EulerPacketMovingFrame.PhysicalGeometryConclusion G F F₁ Z Z₁)
(hhorizon : G.time G.H = G.t₀ + D.T)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerPacketGeometryLowBounds.amplitude_pos
{ι : Type u_1}
(G : EulerPacketMovingFrame.PhysicalGeometryData ι)
(hδ : 0 < G.δ)
(hh : 0 < G.hchild)
:
theorem
EulerPacketSourceGeometry.Guards.primaryAmplitude_pos
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(hδ : 0 < A.δ)
(hh : 0 < A.hchild)
:
theorem
EulerPacketSourceGeometry.Guards.primaryAmplitude_exponential
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
:
theorem
EulerPacketSourceGeometry.Guards.halfBall_controlledGrowth
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
:
∃ (g : C(↑(Set.Icc 0 (D.T - τ)), ℝ)),
(∀ (t : ↑(Set.Icc 0 (D.T - τ))), 0 < g t) ∧ g ⟨0, ⋯⟩ = 1 ∧ EulerPacketSourcePropagator.PhysicalGrowth (D.tail τ ⋯ hτT) {x : EulerSmoothLimit.Space | ‖x‖ ≤ 1 / 2} (⇑g)
(560 * P.horizon ^ 10 / P.epsilon) ∧ ∀ (t : ↑(Set.Icc 0 (D.T - τ))),
A.primaryAmplitude hball * g t ≤ 8 * Real.exp 6 * A.δ * A.hchild / P.rayScale hτ hτT
theorem
EulerPacketSourceGeometry.ForwardGuards.primaryAmplitude_pos
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(hball : 1 / 2 ≤ A.radius)
(hδ : 0 < A.δ)
(hh : 0 < A.hchild)
:
theorem
EulerPacketSourceGeometry.ForwardGuards.primaryAmplitude_exponential
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(hball : 1 / 2 ≤ A.radius)
:
theorem
EulerPacketSourceGeometry.ForwardGuards.halfBall_controlledGrowth
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(hball : 1 / 2 ≤ A.radius)
:
∃ (g : C(↑(Set.Icc 0 D.T), ℝ)),
(∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) ∧ g ⟨0, ⋯⟩ = 1 ∧ EulerPacketSourcePropagator.PhysicalGrowth D {x : EulerSmoothLimit.Space | ‖x‖ ≤ 1 / 2} (⇑g)
(560 * P.horizon ^ 10 / P.epsilon) ∧ ∀ (t : ↑(Set.Icc 0 D.T)), A.primaryAmplitude hball * g t ≤ 8 * Real.exp 6 * A.δ * A.hchild