The actual normalized parent coordinates used by the packet. Joint regularity, the frame, and inverse regularity are derived from the parent time laws and the literal inverse map.

The child particle velocity matches the physical reconstruction of the actual common correction, including the source spatial scaling.

The constructed child particle velocity is the Eulerian pushforward of the actual graph velocity. The normalized packet formula follows from the literal lifted coefficient, with the physical scale explicit.

theorem EulerPhysicalGraphFlowBounds.Data.physicalDisplacementCoefficient_position {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : x + ((G.physicalDisplacementCoefficient k m ell).field t) x = (EulerSmoothBanachFlow.flowData T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell)).forward (↑t) x

theorem EulerPhysicalGraphFlowBounds.Data.physicalVelocityCoefficient_material {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ((G.physicalVelocityCoefficient k m ell).field t) x = ((EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell).field t) ((EulerSmoothBanachFlow.flowData T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell)).forward (↑t) x)

noncomputable def EulerParentPacketFrames.Parent.graphPushforwardVelocity (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Graph pushforward velocity, constructed using u.

Equations

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

theorem EulerParentPacketFrames.Parent.child_position (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (A.child G k m hgraph nextEll hnext hnext1).position t x = A.position t ((EulerSmoothBanachFlow.flowData A.T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m A.T G.A A.ell)).forward (↑t) x)

theorem EulerParentPacketFrames.Parent.child_velocity_formula (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ((A.child G k m hgraph nextEll hnext hnext1).velocity.field t) x = have y := (EulerSmoothBanachFlow.flowData A.T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m A.T G.A A.ell)).forward (↑t) x; (A.velocity.field t) y + (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(A.displacement.field t)) y) (((EulerGraphInvariantFlow.physicalCoefficient k m A.T G.A A.ell).field t) y)

theorem EulerParentPacketFrames.Parent.child_velocity_pushforward (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u t (A.position t x)) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ((A.child G k m hgraph nextEll hnext hnext1).velocity.field t) x = A.graphPushforwardVelocity G k m Y u t ((A.child G k m hgraph nextEll hnext hnext1).position t x)

theorem EulerParentPacketFrames.Parent.graphPushforwardVelocity_packet (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (κ : ℝ) (z : ↑(Set.Icc 0 A.T) → EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (hlift : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (G.A.field t) q = EulerMetricTransport.transportDirection κ m (z t q)) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.graphPushforwardVelocity G k m Y u t x = u t x + A.ell • κ • ((A.frame.field t) (A.ell⁻¹ • Y t x)) (z t ((EulerGraphInvariantFlow.graphLinear k m) (A.ell⁻¹ • Y t x)))

noncomputable def EulerParentPacketFrames.Parent.correctedPacketVelocity (A : Parent) {P : ℝ} [Fact (0 < P)] {C : EulerAllOrderCorrectionData.Data P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ C) (k : ℝ) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Corrected packet velocity, constructed using u.

Equations

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

noncomputable def EulerParentPacketFrames.Parent.packetInverse (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Packet inverse, given by A.ell⁻¹ • Y (projIcc 0 A.T A.T_pos.le q.1) (A.ell • q.2).

Equations

• A.packetInverse Y q = A.ell⁻¹ • Y (Set.projIcc 0 A.T ⋯ q.1) (A.ell • q.2)

theorem EulerParentPacketFrames.Parent.correctedPacketVelocity_eq_physical (A : Parent) {P : ℝ} [Fact (0 < P)] {C : EulerAllOrderCorrectionData.Data P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ C) (k : ℝ) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.correctedPacketVelocity B k Y u t x = u t x + A.ell • EulerPacketPhysicalTransform.physicalVelocity C.κ k C.direction (fun (q : ℝ × EulerLiftedGradientSpace.Vector3) => SmoothTimeField.realField A.T ⋯ A.frame q.1 q.2) ((EulerAllOrderDriftCorrection.Budget.correctedFieldTower P B).rawField ⋯) (A.packetInverse Y) (↑t, A.ell⁻¹ • x)

theorem EulerParentPacketFrames.Parent.lifted_graph_constraint (A : Parent) {P : ℝ} [Fact (0 < P)] {C : EulerAllOrderCorrectionData.Data P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ C) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : C.approximation = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * C.κ = 1) (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent) : (EulerGraphInvariantFlow.graphConstraint k C.direction) ((G.A.field t) q) = 0

theorem EulerParentPacketFrames.Parent.graphPushforwardVelocity_corrected (A : Parent) {P : ℝ} [Fact (0 < P)] {C : EulerAllOrderCorrectionData.Data P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ C) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : C.approximation = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.graphPushforwardVelocity G k C.direction Y u t x = A.correctedPacketVelocity B k Y u t x

theorem EulerParentPacketFrames.Parent.child_velocity_corrected (A : Parent) {P : ℝ} [Fact (0 < P)] {C : EulerAllOrderCorrectionData.Data P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ C) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : C.approximation = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k C.direction) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (Y u : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u t (A.position t x)) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ((A.child G k C.direction hgraph nextEll hnext hnext1).velocity.field t) x = A.correctedPacketVelocity B k Y u t ((A.child G k C.direction hgraph nextEll hnext hnext1).position t x)

A true particle velocity law and the actual Euler equation determine the particle acceleration. Continuity extends the identity to both endpoints; no acceleration or pressure-force match is assumed.

noncomputable def EulerParentPacketFrames.Parent.realPosition (A : Parent) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Real position, given by x+A.displacement.realField A.T A.T_pos.le t x.

Equations

• A.realPosition t x = x + SmoothTimeField.realField A.T ⋯ A.displacement t x

@[simp]

theorem EulerParentPacketFrames.Parent.realPosition_apply (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.realPosition (↑t) x = A.position t x

theorem EulerParentPacketFrames.Parent.realPosition_joint_continuous (A : Parent) : Continuous (Function.uncurry A.realPosition)

theorem EulerParentPacketFrames.Parent.position_time (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => A.realPosition s x) ((A.velocity.field t) x) (Set.Icc 0 A.T) ↑t

theorem EulerParentPacketFrames.Parent.acceleration_eq_neg_gradient (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u (↑t, A.position t x)) (hdiff : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (heuler : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) (t : ↑(Set.Icc 0 A.T)) (ht : ↑t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : (A.acceleration.field t) x = -gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) (A.position t x)

theorem EulerParentPacketFrames.Parent.acceleration_physical_of_euler (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hforce : Continuous (Function.uncurry force)) (hgradient : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = force t x) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u (↑t, A.position t x)) (hdiff : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (heuler : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (A.acceleration.field t) x = -force t (A.position t x)

Two actual time-derivative pairs give genuine joint C² regularity for a smooth spatial coefficient path on interior times.

theorem SmoothTimeField.jointDerivative_contDiffAt_one {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ A₂ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (hA : TimeDerivative T hT A A₁) (hA₁ : TimeDerivative T hT A₁ A₂) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 1 (Function.uncurry (jointDerivative T hT A A₁)) (t, x)

theorem SmoothTimeField.realField_contDiffAt_two {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ A₂ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (hA : TimeDerivative T hT A A₁) (hA₁ : TimeDerivative T hT A₁ A₂) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 2 (Function.uncurry (realField T hT A)) (t, x)

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentNormalizedGeometry1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentNormalizedGeometry1 = inferInstance

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentNormalizedGeometry2 : NormedSpace ℝ EulerSmoothLimit.Space

Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentNormalizedGeometry2 = inferInstance

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentNormalizedGeometry3 : NormedAddCommGroup (ℝ × EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (ℝ × Space) instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentNormalizedGeometry3 = inferInstance

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentNormalizedGeometry4 : NormedSpace ℝ (ℝ × EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (ℝ × Space) instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentNormalizedGeometry4 = inferInstance

noncomputable def EulerParentPacketFrames.Parent.packetPosition (A : Parent) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Packet position, given by A.ell⁻¹ • A.realPosition q.1 (A.ell • q.2).

Equations

• A.packetPosition q = A.ell⁻¹ • A.realPosition q.1 (A.ell • q.2)

@[simp]

theorem EulerParentPacketFrames.Parent.packetPosition_apply (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.packetPosition (↑t, x) = A.ell⁻¹ • A.position t (A.ell • x)

theorem EulerParentPacketFrames.Parent.realPosition_contDiffAt_two (A : Parent) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : ContDiffAt ℝ 2 (Function.uncurry A.realPosition) (t, x)

theorem EulerParentPacketFrames.Parent.packetPosition_contDiffAt_two (A : Parent) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : ContDiffAt ℝ 2 A.packetPosition (t, x)

theorem EulerParentPacketFrames.Parent.packetPosition_joint_continuous (A : Parent) : Continuous A.packetPosition

theorem EulerParentPacketFrames.Parent.realPosition_hasFDerivAt (A : Parent) (t : ↑(Set.Icc 0 A.T)) (ht : ↑t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : HasFDerivAt (Function.uncurry A.realPosition) ((ContinuousLinearMap.toSpanSingleton ℝ ((A.velocity.field t) x)).coprod (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(A.displacement.field t)) x)) (↑t, x)

noncomputable def EulerParentPacketFrames.Parent.packetPositionDerivative (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ℝ × EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Packet position derivative, given by (toSpanSingleton ℝ (A.ell⁻¹ • A.velocity.field t (A.ell • x))).coprod (A.frame.field t x).

Equations

• A.packetPositionDerivative t x = (ContinuousLinearMap.toSpanSingleton ℝ (A.ell⁻¹ • (A.velocity.field t) (A.ell • x))).coprod ((A.frame.field t) x)

theorem EulerParentPacketFrames.Parent.packetPosition_hasFDerivAt (A : Parent) (t : ↑(Set.Icc 0 A.T)) (ht : ↑t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : HasFDerivAt A.packetPosition (A.packetPositionDerivative t x) (↑t, x)

theorem EulerParentPacketFrames.Parent.packetPosition_spatial (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : HasFDerivAt (fun (y : EulerSmoothLimit.Space) => A.packetPosition (↑t, y)) ((A.frame.field t) x) x

theorem EulerParentPacketFrames.Parent.packetPosition_frame (A : Parent) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : SmoothTimeField.realField A.T ⋯ A.frame t x = fderiv ℝ A.packetPosition (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ EulerSmoothLimit.Space

theorem EulerParentPacketFrames.Parent.packetPosition_frame_eventually (A : Parent) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : (fun (q : ℝ × EulerSmoothLimit.Space) => SmoothTimeField.realField A.T ⋯ A.frame q.1 q.2) =ᶠ[nhds (t, x)] fun (q : ℝ × EulerSmoothLimit.Space) => fderiv ℝ A.packetPosition q ∘SL ContinuousLinearMap.inr ℝ ℝ EulerSmoothLimit.Space

theorem EulerParentPacketFrames.Parent.packetPosition_time (A : Parent) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : (fderiv ℝ A.packetPosition (t, x)) (1, 0) = A.ell⁻¹ • (A.velocity.field ⟨t, ⋯⟩) (A.ell • x)

theorem EulerParentPacketFrames.Parent.packetInverse_left (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (q : ℝ × EulerSmoothLimit.Space) : A.packetInverse Y (q.1, A.packetPosition q) = q.2

theorem EulerParentPacketFrames.Parent.packetInverse_right (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (q : ℝ × EulerSmoothLimit.Space) : A.packetPosition (q.1, A.packetInverse Y q) = q.2

theorem EulerParentPacketFrames.Parent.packetInverse_joint_continuous (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Continuous (Function.uncurry Y)) : Continuous (A.packetInverse Y)

noncomputable def EulerParentPacketFrames.Parent.frameEquiv (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space

Frame equiv, given by ContinuousLinearEquiv.equivOfInverse (A.frame.field t x) (A.inverse.field t x) (A.inverse_left t x) (A.inverse_right t x).

Equations

• A.frameEquiv t x = ContinuousLinearEquiv.equivOfInverse ((A.frame.field t) x) ((A.inverse.field t) x) ⋯ ⋯

noncomputable def EulerParentPacketFrames.Parent.packetLift (A : Parent) (q : ℝ × EulerSmoothLimit.Space) : ℝ × EulerSmoothLimit.Space

Packet lift, given by (q.1,A.packetPosition q).

Equations

• A.packetLift q = (q.1, A.packetPosition q)

noncomputable def EulerParentPacketFrames.Parent.packetInverseLift (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : ℝ × EulerSmoothLimit.Space) : ℝ × EulerSmoothLimit.Space

Packet inverse lift, given by (q.1,A.packetInverse Y q).

Equations

• A.packetInverseLift Y q = (q.1, A.packetInverse Y q)

theorem EulerParentPacketFrames.Parent.packetLift_hasFDerivAt (A : Parent) (t : ↑(Set.Icc 0 A.T)) (ht : ↑t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : HasFDerivAt A.packetLift ↑(EulerSmoothBanachFlow.timeLiftEquiv (A.frameEquiv t x) (A.ell⁻¹ • (A.velocity.field t) (A.ell • x))) (↑t, x)

theorem EulerParentPacketFrames.Parent.packetInverseLift_contDiffAt_two (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : ContDiffAt ℝ 2 (A.packetInverseLift Y) (t, x)