The actual constructed geometric stage supplies the physical H3 profile on the forward part of the source interval. The same scalar solution also retains the amplification and amplitude conclusions.
theorem
EulerPacketSourceGeometry.Guards.source_interval
{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)
(Ω : Set EulerSmoothLimit.Space)
(h0 : 0 ∈ Ω)
(hΩ : ∀ x ∈ Ω, ‖x‖ ≤ A.radius)
:
(A.geometryData Ω h0 hΩ).S = Set.Icc (A.geometryData Ω h0 hΩ).t₀ ((A.geometryData Ω h0 hΩ).t₀ + (D.tail τ ⋯ hτT).T)
theorem
EulerPacketSourceGeometry.Guards.source_horizon
{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)
(Ω : Set EulerSmoothLimit.Space)
(h0 : 0 ∈ Ω)
(hΩ : ∀ x ∈ Ω, ‖x‖ ≤ A.radius)
:
(A.geometryData Ω h0 hΩ).time (A.geometryData Ω h0 hΩ).H = (A.geometryData Ω h0 hΩ).t₀ + (D.tail τ ⋯ hτT).T
theorem
EulerPacketSourceGeometry.Guards.source_strain
{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)
(Ω : Set EulerSmoothLimit.Space)
(h0 : 0 ∈ Ω)
(hΩ : ∀ x ∈ Ω, ‖x‖ ≤ A.radius)
(x : { x : EulerSmoothLimit.Space // x ∈ Ω })
(t : ↑(Set.Icc 0 (D.tail τ ⋯ hτT).T))
:
theorem
EulerPacketSourceGeometry.Guards.source_normal
{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)
(Ω : Set EulerSmoothLimit.Space)
(h0 : 0 ∈ Ω)
(hΩ : ∀ x ∈ Ω, ‖x‖ ≤ A.radius)
(x : { x : EulerSmoothLimit.Space // x ∈ Ω })
(t : ↑(Set.Icc 0 (D.tail τ ⋯ hτT).T))
:
(A.geometryData Ω h0 hΩ).r x ((A.geometryData Ω h0 hΩ).t₀ + ↑t) = ((D.tail τ ⋯ hτT).normal.field t) ↑x
theorem
EulerPacketSourceGeometry.Guards.exists_geometry_and_growth
{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)
(Ω : Set EulerSmoothLimit.Space)
(h0 : 0 ∈ Ω)
(hΩ : ∀ x ∈ Ω, ‖x‖ ≤ A.radius)
:
∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ) (J :
EulerPacketMovingFrame.PhysicalGeometryConclusion (A.geometryData Ω h0 hΩ) F F₁ Z Z₁),
(∀ (t : ↑(Set.Icc 0 (D.tail τ ⋯ hτT).T)),
0 < (EulerPacketGeometrySourceGrowth.growthProfile (D.tail τ ⋯ hτT) (A.geometryData Ω h0 hΩ) J) t) ∧ (EulerPacketGeometrySourceGrowth.growthProfile (D.tail τ ⋯ hτT) (A.geometryData Ω h0 hΩ) J) ⟨0, ⋯⟩ = 1 ∧ EulerPacketSourcePropagator.PhysicalGrowth (D.tail τ ⋯ hτT) Ω
(⇑(EulerPacketGeometrySourceGrowth.growthProfile (D.tail τ ⋯ hτT) (A.geometryData Ω h0 hΩ) J))
(EulerPacketGeometrySourceGrowth.growthConstant (A.geometryData Ω h0 hΩ))
theorem
EulerPacketSourceGeometry.Guards.exists_physicalGrowth
{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)
(Ω : Set EulerSmoothLimit.Space)
(h0 : 0 ∈ Ω)
(hΩ : ∀ x ∈ Ω, ‖x‖ ≤ A.radius)
:
theorem
EulerPacketSourceGeometry.Guards.halfBall_physicalGrowth
{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.growth_constant_pos
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ 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)
: