The first normal stage supplies its forward packet budget from the actual amplification geometry. The large parent shear needs no short-time assumption of the form CM*T≤1/2.

noncomputable def EulerPacketSourceGeometry.ForwardGuards.sourceGrowthProfile {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : C(↑(Set.Icc 0 D.T), ℝ)

Source growth profile, given by (G.halfBall_controlledGrowth hball).choose.

Equations

• G.sourceGrowthProfile hball = ⋯.choose

theorem EulerPacketSourceGeometry.ForwardGuards.sourceGrowthProfile_positive {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) : 0 < (G.sourceGrowthProfile hball) t

theorem EulerPacketSourceGeometry.ForwardGuards.sourceGrowthProfile_initial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : (G.sourceGrowthProfile hball) ⟨0, ⋯⟩ = 1

theorem EulerPacketSourceGeometry.ForwardGuards.sourceGrowthProfile_propagator {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : EulerPacketSourcePropagator.PhysicalGrowth D EulerPacketParentPhysicalBudgets.halfBall (⇑(G.sourceGrowthProfile hball)) (560 * P.horizon ^ 10 / P.epsilon)

theorem EulerPacketSourceGeometry.ForwardGuards.sourceGrowthProfile_amplitude {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) : G.primaryAmplitude hball * (G.sourceGrowthProfile hball) t ≤ 8 * Real.exp 6 * G.δ * G.hchild

theorem EulerPacketSourceGeometry.ForwardGuards.primaryAmplitude_bound {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : G.primaryAmplitude hball ≤ 8 * Real.exp 6 * G.δ * G.hchild

theorem EulerPacketSourceGeometry.ForwardGuards.growth_constant_pos {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : 0 < 560 * P.horizon ^ 10 / P.epsilon

noncomputable def EulerParentPacketFrames.LabelData.geometryForwardRaw {A : Parent} (L : LabelData A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) : EulerTransversePacketForward.Budget (A.transverseData m hm J support hSupport) (Fin 4) 6

Geometry forward raw, constructed using EulerPacketParentPhysicalBudgets.forwardBudget.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerParentPacketFrames.LabelData.geometryForwardInputs {A : Parent} (L : LabelData A) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) : ForwardInputs (A.meanData H) (A.transverseData m hm J support hSupport)

Geometry forward inputs as an element of ForwardInputs (A.meanData H) (A.transverseData m hm J support hSupport).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerParentPacketFrames.LabelData.geometryForwardInputs_growth {A : Parent} (L : LabelData A) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) : (L.geometryForwardInputs H m hm J support hSupport P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).linear.g = G.sourceGrowthProfile hball