Actual parent source trajectories supply the older geometric frame. Its matrix derivative is derived from the parent curvature, and its ray and primary velocity are the constructed source trajectories.
noncomputable def
EulerParentPacketFrames.Parent.sourceNormal
(G : Parent)
(m : EulerSmoothLimit.Space)
(t : ℝ)
:
Source normal, given by (G.inverse.realField G.T G.T_pos.le t 0).adjoint m.
Equations
- G.sourceNormal m t = (ContinuousLinearMap.adjoint (SmoothTimeField.realField G.T ⋯ G.inverse t 0)) m
Instances For
theorem
EulerParentPacketFrames.Parent.sourceNormal_apply
(G : Parent)
(m : EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 G.T))
:
theorem
EulerParentPacketFrames.Parent.sourceNormal_equation
(G : Parent)
(m : EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 G.T))
:
HasDerivWithinAt (G.sourceNormal m) (-(ContinuousLinearMap.adjoint (G.centerStrain ↑t)) (G.sourceNormal m ↑t))
(Set.Icc 0 G.T) ↑t
theorem
EulerParentPacketFrames.Parent.sourceNormal_ne_zero
(G : Parent)
(m : EulerSmoothLimit.Space)
(hm : m ≠ 0)
(t : ↑(Set.Icc 0 G.T))
:
noncomputable def
EulerParentPacketFrames.Parent.sourceVelocity
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(η : U)
(t : ℝ)
:
Source velocity, given by EulerPacketForwardFactorization.uncutVelocity (G.transverseData m hm R S hS) η t 0.
Equations
- G.sourceVelocity m hm R S hS η t = EulerPacketForwardFactorization.uncutVelocity (G.transverseData m hm R S hS) η t 0
Instances For
theorem
EulerParentPacketFrames.Parent.source_normal_eq
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(t : ↑(Set.Icc 0 G.T))
:
theorem
EulerParentPacketFrames.Parent.source_strain_eq
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(t : ↑(Set.Icc 0 G.T))
:
theorem
EulerParentPacketFrames.Parent.sourceVelocity_equation
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(η : U)
(t : ↑(Set.Icc 0 G.T))
:
HasDerivWithinAt (G.sourceVelocity m hm R S hS η)
(-(G.centerStrain ↑t) (G.sourceVelocity m hm R S hS η ↑t) + (2 * inner ℝ (G.sourceNormal m ↑t) ((G.centerStrain ↑t) (G.sourceVelocity m hm R S hS η ↑t)) / ‖G.sourceNormal m ↑t‖ ^ 2) • G.sourceNormal m ↑t)
(Set.Icc 0 G.T) ↑t
theorem
EulerParentPacketFrames.Parent.sourceVelocity_ne_zero
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(η : U)
(hη : η ≠ 0)
(t : ↑(Set.Icc 0 G.T))
:
theorem
EulerParentPacketFrames.Parent.sourceVelocity_tangent
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(η : U)
(t : ↑(Set.Icc 0 G.T))
:
theorem
EulerParentPacketFrames.Parent.joined_sourceVelocity
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(s : ℝ)
(hs : 0 < s)
(hsT : s < G.T)
(B : EulerTransversePacketProvider.HistoryData ((G.transverseData m hm R S hS).initial s hs ⋯))
(ξ : U)
(t : ℝ)
:
G.sourceVelocity m hm R S hS (((B.coefficients.labelCoordinate 0) ξ) ⟨0, ⋯⟩) t = EulerPacketPrimaryFactorization.uncutVelocity s hs hsT B ξ t 0
Both primary branches are the same actual homogeneous propagator after inserting their constructed initial coordinate.
theorem
EulerParentPacketFrames.Parent.joined_initialCoordinate_ne_zero
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(s : ℝ)
(hs : 0 < s)
(hsT : s < G.T)
(B : EulerTransversePacketProvider.HistoryData ((G.transverseData m hm R S hS).initial s hs ⋯))
(ξ : U)
(hξ : ξ ≠ 0)
:
noncomputable def
EulerParentPacketFrames.Parent.geometryFrameOfCenterExpansion
(G : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(D : EulerTransversePacketProvider.Data V)
(hTime : D.T = G.T)
(τ : ℝ)
(hτ : 0 ≤ τ)
(η : U)
(hη : η ≠ 0)
(w : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(c CM CH K error : ℝ)
(hCM : 0 ≤ CM)
(hK : 1 ≤ K)
(he : 0 ≤ error)
(hMK : CM ≤ K)
(hHK : CM ^ 2 + CH ≤ K ^ 2)
(hM : ∀ t ∈ Set.Icc τ D.T, ‖G.centerStrain t‖ ≤ CM)
(hH : ∀ t ∈ Set.Icc τ D.T, ‖G.centerCurvature t‖ ≤ CH)
(hupdate : ∀ (t : ↑(Set.Icc 0 D.T)), (D.M.field t) 0 = G.centerStrain ↑t + fderiv ℝ (w ↑t) 0)
(hpacket :
∀ t ∈ Set.Icc τ D.T,
‖fderiv ℝ (w t) 0 - c • ((InnerProductSpace.rankOne ℝ) (G.sourceVelocity m hm R S hS η t)) (G.sourceNormal m t)‖ ≤ error)
:
The only error input is the literal center derivative estimate for the already constructed perturbation. No ray, velocity or matrix ODE is supplied as a hypothesis.
Equations
- One or more equations did not get rendered due to their size.