The actual source ray and selected primary satisfy every analytic
field of PhysicalGeometryData. Neighbor errors follow from the source
coefficient derivatives and the genuine stationary-history estimate.
The actual source normal and the same selected terminal coordinate give the scaled neighboring-label initial errors. Their constants only involve coefficient norms, the terminal size, and the stated scaling.
The actual fixed-terminal history estimate controls the scaled neighbor
initial velocity. The loss ε⁻¹ comes from the specified coordinate
rescaling and is independent of the oscillation frequency.
theorem
EulerPacketMovingFrame.scaledVelocity_initial_difference_le
{m v x y : ℝ → EulerSmoothLimit.Space}
{t₀ a ε D : ℝ}
(hm0 : m t₀ ≠ 0)
(hv0 : v t₀ ≠ 0)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hxy : ‖x t₀ - y t₀‖ ≤ D)
:
|scaledVelocity m v x t₀ a ε 0 0 - scaledVelocity m v y t₀ a ε 0 0| + |scaledVelocity m v x t₀ a ε 0 1 - scaledVelocity m v y t₀ a ε 0 1| ≤ 2 * D / ε
theorem
EulerPacketMovingFrame.scaledRay_initial_error
{m v r : ℝ → EulerSmoothLimit.Space}
{s₀ t₀ a ε D : ℝ}
(hs₀ : 0 < s₀)
(hm0 : m t₀ ≠ 0)
(hv0 : v t₀ ≠ 0)
(hmv : inner ℝ (m t₀) (v t₀) = 0)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hr :
‖r t₀ - s₀ • EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m t₀))
(EulerPacketNormalizedPrimary.unit (v t₀))‖ ≤ D)
:
A physical initial-ray error around the chosen normal becomes the
source's scaled ray error with the fixed factor (s₀ ε)⁻¹.
theorem
EulerPacketMovingFrame.frame_pair_operator_difference_le
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{T ε D : ℝ}
(A B : U →L[ℝ] C(↑(Set.Icc 0 T), EulerSmoothLimit.Space))
(ξ : U)
(t : ↑(Set.Icc 0 T))
{p q : EulerSmoothLimit.Space}
(hp : ‖p‖ = 1)
(hq : ‖q‖ = 1)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hAB : ‖A - B‖ ≤ D)
:
theorem
EulerPacketMovingFrame.history_scaled_pair_difference_le
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] EulerSmoothLimit.Space))
(H : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (ξ : U), c * ‖ξ‖ ^ 2 ≤ ‖(Q t) ξ‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerSmoothLimit.Space), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] EulerSmoothLimit.Space))
(G : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(hP : ∀ (t : ↑(Set.Icc 0 T)) (ξ : U), c * ‖ξ‖ ^ 2 ≤ ‖(P t) ξ‖ ^ 2)
(hp : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t)
(hG : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerSmoothLimit.Space), inner ℝ ((G t) z) z ≤ K * ‖z‖ ^ 2)
(hTpos : 0 < T)
(q q₁ d a r : ℝ)
(hQn : ‖Q‖ ≤ q)
(hPn : ‖P‖ ≤ q)
(hQ₁n : ‖Q₁‖ ≤ q₁)
(hP₁n : ‖P₁‖ ≤ q₁)
(hD : T * ‖Q₁‖ + ‖Q‖ ≤ d)
(hD' : T * ‖P₁‖ + ‖P‖ ≤ d)
(hA : 1 + T ^ 2 * ‖H‖ ≤ a)
(hA' : 1 + T ^ 2 * ‖G‖ ≤ a)
(hr : EulerTimeH1FrameTransport.transportCost T Q Q₁ c ≤ r)
(hr' : EulerTimeH1FrameTransport.transportCost T P P₁ c ≤ r)
(L₀ L₁ LH s : ℝ)
(h₀ : ‖Q - P‖ ≤ L₀ * s)
(h₁ : ‖Q₁ - P₁‖ ≤ L₁ * s)
(hHdiff : ‖H - G‖ ≤ LH * s)
(ξ : U)
(t : ↑(Set.Icc 0 T))
{p₀ q₀ : EulerSmoothLimit.Space}
(hp₀ : ‖p₀‖ = 1)
(hq₀ : ‖q₀‖ = 1)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
:
have u := ((EulerTransverseEndpointCoordinates.historyVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ) t;
have v := ((EulerTransverseEndpointCoordinates.historyVelocity T hT P P₁ G c hc hP hp K hK hG hsmall) ξ) t;
|inner ℝ p₀ u / ε - inner ℝ p₀ v / ε| + |inner ℝ q₀ u - inner ℝ q₀ v| ≤ 2 * EulerTransverseHistoryBounds.historyDifferenceCost T c q q₁ d a r L₀ L₁ LH * s * ‖ξ‖ / ε
The two actual stationary histories use the same terminal coordinate
ξ; physical coefficient differences give the scaled initial error.
theorem
EulerPacketActivationHistory.uncutVelocity_activation_difference
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(ξ : U)
(x y : EulerSmoothLimit.Space)
:
‖EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ τ x - EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ τ y‖ ≤ historyLabelDifferenceCost B * ‖x - y‖ * ‖ξ‖
theorem
EulerPacketActivationHistory.actual_scaled_velocity_initial_error
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(m v : ℝ → EulerSmoothLimit.Space)
(hm : m τ ≠ 0)
(hv : v τ ≠ 0)
(ξ : U)
(a ε lam : ℝ)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hu :
EulerPacketMovingFrame.scaledVelocity m v
(fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ s 0) τ a ε 0 0 = -lam)
(hw :
EulerPacketMovingFrame.scaledVelocity m v
(fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ s 0) τ a ε 0 1 = 1)
(x : EulerSmoothLimit.Space)
:
|EulerPacketMovingFrame.scaledVelocity m v
(fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ s x) τ a ε 0 1 - 1| + |EulerPacketMovingFrame.scaledVelocity m v
(fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ s x) τ a ε 0 0 + lam| ≤ 2 * historyLabelDifferenceCost B * ‖x‖ * ‖ξ‖ / ε
theorem
EulerPacketActivationHistory.actual_scaled_ray_initial_error
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(m v : ℝ → EulerSmoothLimit.Space)
(hm : m τ ≠ 0)
(hv : v τ ≠ 0)
(hmv : inner ℝ (m τ) (v τ) = 0)
(hchoice :
D.m₀ = EulerPacketMovingFrame.activationDirection (D.deformationEquiv ⟨τ, ⋯⟩ 0)
(EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m τ))
(EulerPacketNormalizedPrimary.unit (v τ))))
(a ε : ℝ)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(x : EulerSmoothLimit.Space)
:
have s₀ :=
EulerPacketMovingFrame.activationRayScale (D.deformationEquiv ⟨τ, ⋯⟩ 0)
(EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m τ)) (EulerPacketNormalizedPrimary.unit (v τ)));
EulerPacketRay.norm3 (EulerPacketMovingFrame.scaledRay m v (fun (s : ℝ) => (D.normal.field (D.clamp s)) x) s₀ τ a ε 0 0)
(EulerPacketMovingFrame.scaledRay m v (fun (s : ℝ) => (D.normal.field (D.clamp s)) x) s₀ τ a ε 0 1)
(EulerPacketMovingFrame.scaledRay m v (fun (s : ℝ) => (D.normal.field (D.clamp s)) x) s₀ τ a ε 0 2 - 1) ≤ 3 * ‖D.normal.derivative.field‖ * ‖x‖ / (s₀ * ε)
Exact scale normalization from the actual parent frame and shear. The physical interval ends at the chosen scaled horizon; no extension beyond the source time interval is required.
theorem
EulerPacketMovingFrame.activation_coupling_match
(B : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(m v : ℝ → EulerSmoothLimit.Space)
(t₀ ε : ℝ)
:
have a := normalizedCoupling (B t₀) (m t₀) (v t₀);
rescaledFrame B m v t₀ a ε 0 0 1 = a
theorem
EulerPacketMovingFrame.activation_tilt_match
(B : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(m v : ℝ → EulerSmoothLimit.Space)
(t₀ ε : ℝ)
(ha : normalizedCoupling (B t₀) (m t₀) (v t₀) ≠ 0)
(hβ : 0 ≤ normalizedTilt (B t₀) (m t₀) (v t₀))
:
have a := normalizedCoupling (B t₀) (m t₀) (v t₀);
have σ := √(normalizedTilt (B t₀) (m t₀) (v t₀));
rescaledFrame B m v t₀ a ε 0 2 1 = a * σ ^ 2
theorem
EulerPacketMovingFrame.activation_shear_match
(c : ℝ)
(m v : ℝ → EulerSmoothLimit.Space)
(t₀ a : ℝ)
(ha : 0 < a)
(hh : 0 < primaryShear c m v t₀)
:
have ε := √(a / primaryShear c m v t₀);
0 < ε ∧ rescaledShear c m v t₀ a ε 0 = a / ε ^ 2
theorem
EulerPacketMovingFrame.activation_horizon_maps
(t₀ T a ε : ℝ)
(ha : 0 < a)
(hε : 0 < ε)
:
Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 (a * (T - t₀) / ε)) (Set.Icc t₀ T)
noncomputable def
EulerPacketSourceGeometry.sourceMatrix
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(x : EulerSmoothLimit.Space)
(t : ℝ)
:
Source matrix, given by D.M.field (D.clamp t) x.
Equations
- EulerPacketSourceGeometry.sourceMatrix D x t = (D.M.field (D.clamp t)) x
Instances For
noncomputable def
EulerPacketSourceGeometry.sourceRay
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(x : EulerSmoothLimit.Space)
(t : ℝ)
:
Source ray, given by D.normal.field (D.clamp t) x.
Equations
- EulerPacketSourceGeometry.sourceRay D x t = (D.normal.field (D.clamp t)) x
Instances For
theorem
EulerPacketSourceGeometry.sourceMatrix_continuous
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(x : EulerSmoothLimit.Space)
:
Continuous (sourceMatrix D x)
noncomputable def
EulerPacketSourceGeometry.ParentFrame.sourceError
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{P : ParentFrame D τ}
(x : EulerSmoothLimit.Space)
(t : ℝ)
:
Source error, given by sourceMatrix D x t-P.B t-primaryShear P.c P.m P.v t • rankOne ℝ (unit (P.v t)) (unit (P.m t)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketSourceGeometry.Guards.sourceVelocity
{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)
(x : EulerSmoothLimit.Space)
(t : ℝ)
:
Source velocity, given by uncutVelocity τ hτ hτT H A.terminal t x.
Equations
- A.sourceVelocity x t = EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H (EulerPacketSourceGeometry.Guards.terminal hτ hτT P H A) t x
Instances For
theorem
EulerPacketSourceGeometry.Guards.sourceRay_equation
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
(x : EulerSmoothLimit.Space)
(t : ℝ)
(ht : t ∈ Set.Icc τ D.T)
:
HasDerivWithinAt (sourceRay D x) (-(ContinuousLinearMap.adjoint (sourceMatrix D x t)) (sourceRay D x t)) (Set.Icc τ D.T)
t
theorem
EulerPacketSourceGeometry.Guards.sourceVelocity_equation
{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)
(x : EulerSmoothLimit.Space)
(t : ℝ)
(ht : t ∈ Set.Icc τ D.T)
:
HasDerivWithinAt (A.sourceVelocity x)
(-(sourceMatrix D x t) (A.sourceVelocity x t) + (2 * inner ℝ (sourceRay D x t) ((sourceMatrix D x t) (A.sourceVelocity x t)) / ‖sourceRay D x t‖ ^ 2) • sourceRay D x t)
(Set.Icc τ D.T) t
theorem
EulerPacketSourceGeometry.Guards.source_initial_tangent
{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)
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketSourceGeometry.Guards.sourceVelocity_ne_zero
{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)
(x : EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerPacketSourceGeometry.Guards.neighbor_components
{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)
:
‖D.M.derivative.field‖ ≤ P.neighborCost hτ hτT H A.CM A.CH ∧ 3 * ‖D.normal.derivative.field‖ / (P.rayScale hτ hτT * P.epsilon) ≤ P.neighborCost hτ hτT H A.CM A.CH ∧ 2 * EulerPacketActivationHistory.historyLabelDifferenceCost H * P.terminalBound A.CM A.CH / P.epsilon ≤ P.neighborCost hτ hτT H A.CM A.CH
theorem
EulerPacketSourceGeometry.Guards.radius_cost_le_error
{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)
:
theorem
EulerPacketSourceGeometry.Guards.sourceError_bound
{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)
(x : EulerSmoothLimit.Space)
(hx : ‖x‖ ≤ A.radius)
(t : ℝ)
(ht : t ∈ Set.Icc τ D.T)
:
theorem
EulerPacketSourceGeometry.Guards.source_velocity_initial_error
{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)
(x : EulerSmoothLimit.Space)
(hx : ‖x‖ ≤ A.radius)
:
|EulerPacketMovingFrame.scaledVelocity P.m P.v (A.sourceVelocity x) τ P.a P.epsilon 0 1 - 1| + |EulerPacketMovingFrame.scaledVelocity P.m P.v (A.sourceVelocity x) τ P.a P.epsilon 0 0 + slope hτ hτT P H A| ≤ P.totalError hτ hτT H A.CM A.CH A.radius
theorem
EulerPacketSourceGeometry.Guards.source_ray_initial_error
{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)
(x : EulerSmoothLimit.Space)
(hx : ‖x‖ ≤ A.radius)
:
EulerPacketRay.norm3 (EulerPacketMovingFrame.scaledRay P.m P.v (sourceRay D x) (P.rayScale hτ hτT) τ P.a P.epsilon 0 0)
(EulerPacketMovingFrame.scaledRay P.m P.v (sourceRay D x) (P.rayScale hτ hτT) τ P.a P.epsilon 0 1)
(EulerPacketMovingFrame.scaledRay P.m P.v (sourceRay D x) (P.rayScale hτ hτT) τ P.a P.epsilon 0 2 - 1) ≤ P.totalError hτ hτT H A.CM A.CH A.radius
theorem
EulerPacketSourceGeometry.Guards.error_le_scaled_error
{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)
:
noncomputable def
EulerPacketSourceGeometry.Guards.geometryData
{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)
:
Every new analytic component is the actual source field or the selected stationary/forward primary. The parent input and scalar guard record contain none of this record's new-field conclusions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketSourceGeometry.Guards.geometryData_matrix
{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 : ℝ)
:
theorem
EulerPacketSourceGeometry.Guards.geometryData_ray
{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 : ℝ)
:
theorem
EulerPacketSourceGeometry.Guards.geometryData_velocity
{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 : ℝ)
:
(A.geometryData Ω h0 hΩ).w x t = EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H (terminal hτ hτT P H A) t ↑x