The physical geometry theorem supplies the actual weighted-growth input used by the source packet budgets. The only bridge hypotheses are literal interval, strain, and normal identities.

noncomputable def EulerPacketGeometrySourceGrowth.growthProfile {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₁) : C(↑(Set.Icc 0 D.T), ℝ)

Growth profile, bundling toFun, continuous_toFun.

Equations

• EulerPacketGeometrySourceGrowth.growthProfile D G H = { toFun := fun (t : ↑(Set.Icc 0 D.T)) => Z (G.a / G.ε * ↑t), continuous_toFun := ⋯ }

theorem EulerPacketGeometrySourceGrowth.growthProfile_eq_physical {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₁) (t : ↑(Set.Icc 0 D.T)) : (growthProfile D G H) t = EulerPacketMovingFrame.physicalProfile Z G.t₀ G.a G.ε (G.t₀ + ↑t)

theorem EulerPacketGeometrySourceGrowth.growthProfile_initial {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₁) : (growthProfile D G H) ⟨0, ⋯⟩ = 1

theorem EulerPacketGeometrySourceGrowth.growthProfile_pos {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)) : 0 < (growthProfile D G H) t

noncomputable def EulerPacketGeometrySourceGrowth.growthConstant {Ω : Set EulerSmoothLimit.Space} (G : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // x ∈ Ω }) : ℝ

Growth constant, given by 560*G.Θ^10/G.ε.

Equations

• EulerPacketGeometrySourceGrowth.growthConstant G = 560 * G.Θ ^ 10 / G.ε

theorem EulerPacketGeometrySourceGrowth.growthConstant_pos {Ω : Set EulerSmoothLimit.Space} (G : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // x ∈ Ω }) : 0 < growthConstant G

theorem EulerPacketGeometrySourceGrowth.physicalGrowth_of_geometry {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₁) (hinterval : G.S = Set.Icc G.t₀ (G.t₀ + D.T)) (hhorizon : G.time G.H = G.t₀ + D.T) (hstrain : ∀ (x : { x : EulerSmoothLimit.Space // x ∈ Ω }) (t : ↑(Set.Icc 0 D.T)), G.M x (G.t₀ + ↑t) = (D.M.field t) ↑x) (hnormal : ∀ (x : { x : EulerSmoothLimit.Space // x ∈ Ω }) (t : ↑(Set.Icc 0 D.T)), G.r x (G.t₀ + ↑t) = (D.normal.field t) ↑x) : EulerPacketSourcePropagator.PhysicalGrowth D Ω (⇑(growthProfile D G H)) (growthConstant G)

theorem EulerPacketGeometrySourceGrowth.exists_growth_of_geometry {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {Ω : Set EulerSmoothLimit.Space} (G : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // x ∈ Ω }) (hinterval : G.S = Set.Icc G.t₀ (G.t₀ + D.T)) (hhorizon : G.time G.H = G.t₀ + D.T) (hstrain : ∀ (x : { x : EulerSmoothLimit.Space // x ∈ Ω }) (t : ↑(Set.Icc 0 D.T)), G.M x (G.t₀ + ↑t) = (D.M.field t) ↑x) (hnormal : ∀ (x : { x : EulerSmoothLimit.Space // x ∈ Ω }) (t : ↑(Set.Icc 0 D.T)), G.r x (G.t₀ + ↑t) = (D.normal.field t) ↑x) : ∃ (g : C(↑(Set.Icc 0 D.T), ℝ)) (C : ℝ), (∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) ∧ g ⟨0, ⋯⟩ = 1 ∧ 0 < C ∧ EulerPacketSourcePropagator.PhysicalGrowth D Ω (⇑g) C

The profile and its physical growth property are derived together from the actual geometry stage. They are ready for the source-budget constructors.