The actual composed child coefficients form the next parent data. The next spatial scale can be chosen independently of the current scale.

Actual continuous bounded coefficient paths for the graph-flow displacement, velocity, and acceleration. No extra supremum estimate on the time derivative of the lifted velocity is required.

Actual deformation, first time derivative, and second time derivative as smooth bounded coefficient paths. Every spatial jet is continuous in the sup norm; no third time derivative is used for the acceleration.

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation1 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] E)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation2 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] E)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation2 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation3 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] E))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] E)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation3 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation4 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] E))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] E)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation4 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation5 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] E)

Cache the standard NormedAddCommGroup (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation5 = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation6 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] E)

Cache the standard NormedSpace ℝ (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation6 = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation7 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] E →L[ℝ] E)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] (E →L[ℝ] E)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation7 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation8 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] E →L[ℝ] E)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] (E →L[ℝ] E)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation8 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation9 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] E))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] (E →L[ℝ] E))) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation9 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothBanachFlow.instSmoothFlowDeformation10 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] E))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] (E →L[ℝ] E))) instance to shorten typeclass synthesis.

Equations

• EulerSmoothBanachFlow.instSmoothFlowDeformation10 n = inferInstance

noncomputable def EulerSmoothBanachFlow.accelerationCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) : SmoothTimeField (↑(Set.Icc 0 T)) E E

Acceleration coefficient as an element of SmoothTimeField (Icc (0 : ℝ) T) E E.

Equations

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

@[simp]

theorem EulerSmoothBanachFlow.accelerationCoefficient_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : ((accelerationCoefficient T hT A B R hB hR hsmall hb A₁).field t) x = (accelerationFamily T hT A A₁ x) t

noncomputable def EulerSmoothBanachFlow.deformationCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) : SmoothTimeField (↑(Set.Icc 0 T)) E (E →L[ℝ] E)

Deformation coefficient, given by (SmoothTimeField.boundConstant (ContinuousLinearMap.id ℝ E)).add (displacementCoefficient T hT A B R hB hR hsmall hb).derivative.

Equations

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

@[simp]

theorem EulerSmoothBanachFlow.deformationCoefficient_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (t : ↑(Set.Icc 0 T)) (x : E) : ((deformationCoefficient T hT A B R hB hR hsmall hb).field t) x = fderiv ℝ (fun (y : E) => (flowData T hT A).forward (↑t) y) x

noncomputable def EulerSmoothBanachFlow.deformationTimeCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) : SmoothTimeField (↑(Set.Icc 0 T)) E (E →L[ℝ] E)

Deformation time coefficient, given by (velocityCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁).derivative.

Equations

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

noncomputable def EulerSmoothBanachFlow.deformationSecondCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) : SmoothTimeField (↑(Set.Icc 0 T)) E (E →L[ℝ] E)

Deformation second coefficient, given by (accelerationCoefficient T hT A B R hB hR hsmall hb A₁).derivative.

Equations

• EulerSmoothBanachFlow.deformationSecondCoefficient T hT A B R hB hR hsmall hb A₁ = (EulerSmoothBanachFlow.accelerationCoefficient T hT A B R hB hR hsmall hb A₁).derivative

theorem EulerSmoothBanachFlow.displacementCoefficient_time {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) : SmoothTimeField.TimeDerivative T hT (displacementCoefficient T hT A B R hB hR hsmall hb) (velocityCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁)

theorem EulerSmoothBanachFlow.velocityCoefficient_time {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) : SmoothTimeField.TimeDerivative T hT (velocityCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁) (accelerationCoefficient T hT A B R hB hR hsmall hb A₁)

theorem EulerSmoothBanachFlow.deformationCoefficient_time {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) : SmoothTimeField.TimeDerivative T hT (deformationCoefficient T hT A B R hB hR hsmall hb) (deformationTimeCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁)

theorem EulerSmoothBanachFlow.deformationTimeCoefficient_time {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) : SmoothTimeField.TimeDerivative T hT (deformationTimeCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁) (deformationSecondCoefficient T hT A B R hB hR hsmall hb A₁)

noncomputable def EulerPhysicalGraphFlowBounds.Data.coverDisplacementCoefficient {P T : ℝ} [Fact (0 < P)] (G : Data P T) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

Cover displacement coefficient, given by displacementCoefficient T G.time_nonneg G.A G.B G.R G.B_nonneg G.R_pos G.small G.sup_bound.

Equations

• G.coverDisplacementCoefficient = EulerSmoothBanachFlow.displacementCoefficient T ⋯ G.A G.B G.R ⋯ ⋯ ⋯ ⋯

noncomputable def EulerPhysicalGraphFlowBounds.Data.coverVelocityCoefficient {P T : ℝ} [Fact (0 < P)] (G : Data P T) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

Cover velocity coefficient, given by G.A.compDisplacement G.coverDisplacementCoefficient.

Equations

• G.coverVelocityCoefficient = G.A.compDisplacement G.coverDisplacementCoefficient

noncomputable def EulerPhysicalGraphFlowBounds.Data.coverAccelerationCoefficient {P T : ℝ} [Fact (0 < P)] (G : Data P T) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

Cover acceleration coefficient, given by accelerationCoefficient T G.time_nonneg G.A G.B G.R G.B_nonneg G.R_pos G.small G.sup_bound G.A₁.

Equations

• G.coverAccelerationCoefficient = EulerSmoothBanachFlow.accelerationCoefficient T ⋯ G.A G.B G.R ⋯ ⋯ ⋯ ⋯ G.A₁

@[simp]

theorem EulerPhysicalGraphFlowBounds.Data.coverDisplacementCoefficient_apply {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (G.coverDisplacementCoefficient.field t) x = (EulerSmoothBanachFlow.flowData T ⋯ G.A).forward (↑t) x - x

@[simp]

theorem EulerPhysicalGraphFlowBounds.Data.coverVelocityCoefficient_apply {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (G.coverVelocityCoefficient.field t) x = (EulerSmoothBanachFlow.velocityFamily T ⋯ G.A x) t

@[simp]

theorem EulerPhysicalGraphFlowBounds.Data.coverAccelerationCoefficient_apply {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (G.coverAccelerationCoefficient.field t) x = (EulerSmoothBanachFlow.accelerationFamily T ⋯ G.A G.A₁ x) t

theorem EulerPhysicalGraphFlowBounds.Data.coverDisplacementCoefficient_time {P T : ℝ} [Fact (0 < P)] (G : Data P T) : SmoothTimeField.TimeDerivative T ⋯ G.coverDisplacementCoefficient G.coverVelocityCoefficient

theorem EulerPhysicalGraphFlowBounds.Data.coverVelocityCoefficient_time {P T : ℝ} [Fact (0 < P)] (G : Data P T) : SmoothTimeField.TimeDerivative T ⋯ G.coverVelocityCoefficient G.coverAccelerationCoefficient

noncomputable def EulerPhysicalGraphFlowBounds.Data.physicalDisplacementCoefficient {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3

Physical displacement coefficient, given by physicalCoefficient k m T G.coverDisplacementCoefficient ell.

Equations

• G.physicalDisplacementCoefficient k m ell = EulerGraphInvariantFlow.physicalCoefficient k m T G.coverDisplacementCoefficient ell

noncomputable def EulerPhysicalGraphFlowBounds.Data.physicalVelocityCoefficient {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3

Physical velocity coefficient, given by physicalCoefficient k m T G.coverVelocityCoefficient ell.

Equations

• G.physicalVelocityCoefficient k m ell = EulerGraphInvariantFlow.physicalCoefficient k m T G.coverVelocityCoefficient ell

noncomputable def EulerPhysicalGraphFlowBounds.Data.physicalAccelerationCoefficient {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3

Physical acceleration coefficient, given by physicalCoefficient k m T G.coverAccelerationCoefficient ell.

Equations

• G.physicalAccelerationCoefficient k m ell = EulerGraphInvariantFlow.physicalCoefficient k m T G.coverAccelerationCoefficient ell

theorem EulerPhysicalGraphFlowBounds.Data.physicalDisplacementCoefficient_time {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) : SmoothTimeField.TimeDerivative T ⋯ (G.physicalDisplacementCoefficient k m ell) (G.physicalVelocityCoefficient k m ell)

theorem EulerPhysicalGraphFlowBounds.Data.physicalVelocityCoefficient_time {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) : SmoothTimeField.TimeDerivative T ⋯ (G.physicalVelocityCoefficient k m ell) (G.physicalAccelerationCoefficient k m ell)

theorem EulerPhysicalGraphFlowBounds.Data.physicalDisplacementCoefficient_eq {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ((G.physicalDisplacementCoefficient k m ell).field t) x = (G.displacementField k m ell hell t).field x

theorem EulerPhysicalGraphFlowBounds.Data.physicalVelocityCoefficient_eq {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ((G.physicalVelocityCoefficient k m ell).field t) x = (G.velocityField k m ell hell t).field x

theorem EulerPhysicalGraphFlowBounds.Data.physicalAccelerationCoefficient_eq {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ((G.physicalAccelerationCoefficient k m ell).field t) x = (G.accelerationFieldL2 k m ell hell t).field x

The literal child map X(t,Y(t,a)), its actual velocity, and its actual acceleration, as continuous smooth coefficient paths.

noncomputable def EulerChildParticleTime.firstTerm {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D V : SmoothTimeField K E E) : SmoothTimeField K E E

First term, given by applyField (P.derivative.compDisplacement D) V.

Equations

• EulerChildParticleTime.firstTerm P D V = (P.derivative.compDisplacement D).applyField V

noncomputable def EulerChildParticleTime.secondTerm {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D V : SmoothTimeField K E E) : SmoothTimeField K E E

Second term, given by applyField (applyField (P.derivative.derivative.compDisplacement D) V) V.

Equations

• EulerChildParticleTime.secondTerm P D V = ((P.derivative.derivative.compDisplacement D).applyField V).applyField V

noncomputable def EulerChildParticleTime.displacement {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D : SmoothTimeField K E E) : SmoothTimeField K E E

Displacement, given by (P.compDisplacement D).add D.

Equations

• EulerChildParticleTime.displacement P D = (P.compDisplacement D).add D

noncomputable def EulerChildParticleTime.velocity {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P P₁ D D₁ : SmoothTimeField K E E) : SmoothTimeField K E E

Velocity, given by ((P₁.compDisplacement D).add D₁).add (firstTerm P D D₁).

Equations

• EulerChildParticleTime.velocity P P₁ D D₁ = ((P₁.compDisplacement D).add D₁).add (EulerChildParticleTime.firstTerm P D D₁)

noncomputable def EulerChildParticleTime.acceleration {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P P₁ P₂ D D₁ D₂ : SmoothTimeField K E E) : SmoothTimeField K E E

Acceleration as an element of SmoothTimeField K E E.

Equations

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

@[simp]

theorem EulerChildParticleTime.firstTerm_apply {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D V : SmoothTimeField K E E) (t : K) (x : E) : ((firstTerm P D V).field t) x = (fderiv ℝ (⇑(P.field t)) (x + (D.field t) x)) ((V.field t) x)

@[simp]

theorem EulerChildParticleTime.secondTerm_apply {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D V : SmoothTimeField K E E) (t : K) (x : E) : ((secondTerm P D V).field t) x = ((fderiv ℝ (fderiv ℝ ⇑(P.field t)) (x + (D.field t) x)) ((V.field t) x)) ((V.field t) x)

@[simp]

theorem EulerChildParticleTime.displacement_apply {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D : SmoothTimeField K E E) (t : K) (x : E) : ((displacement P D).field t) x = (P.field t) (x + (D.field t) x) + (D.field t) x

@[simp]

theorem EulerChildParticleTime.velocity_apply {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P P₁ D D₁ : SmoothTimeField K E E) (t : K) (x : E) : ((velocity P P₁ D D₁).field t) x = (P₁.field t) (x + (D.field t) x) + (D₁.field t) x + (fderiv ℝ (⇑(P.field t)) (x + (D.field t) x)) ((D₁.field t) x)

@[simp]

theorem EulerChildParticleTime.acceleration_apply {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P P₁ P₂ D D₁ D₂ : SmoothTimeField K E E) (t : K) (x : E) : ((acceleration P P₁ P₂ D D₁ D₂).field t) x = (P₂.field t) (x + (D.field t) x) + (fderiv ℝ (⇑(P₁.field t)) (x + (D.field t) x)) ((D₁.field t) x) + (fderiv ℝ (⇑(P₁.field t)) (x + (D.field t) x)) ((D₁.field t) x) + ((fderiv ℝ (fderiv ℝ ⇑(P.field t)) (x + (D.field t) x)) ((D₁.field t) x)) ((D₁.field t) x) + (D₂.field t) x + (fderiv ℝ (⇑(P.field t)) (x + (D.field t) x)) ((D₂.field t) x)

theorem EulerChildParticleTime.map_composition {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D : SmoothTimeField K E E) (t : K) (x : E) : x + ((displacement P D).field t) x = x + (D.field t) x + (P.field t) (x + (D.field t) x)

theorem EulerChildParticleTime.displacement_time {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {hT : 0 ≤ T} [CompleteSpace E] {P P₁ D D₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E} (hP : SmoothTimeField.TimeDerivative T hT P P₁) (hD : SmoothTimeField.TimeDerivative T hT D D₁) : SmoothTimeField.TimeDerivative T hT (displacement P D) (velocity P P₁ D D₁)

theorem EulerChildParticleTime.velocity_time {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {hT : 0 ≤ T} [CompleteSpace E] {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) E E} [FiniteDimensional ℝ E] (hP : SmoothTimeField.TimeDerivative T hT P P₁) (hP₁ : SmoothTimeField.TimeDerivative T hT P₁ P₂) (hD : SmoothTimeField.TimeDerivative T hT D D₁) (hD₁ : SmoothTimeField.TimeDerivative T hT D₁ D₂) : SmoothTimeField.TimeDerivative T hT (velocity P P₁ D D₁) (acceleration P P₁ P₂ D D₁ D₂)

Initial identity and determinant one for the actual child coefficient map. These invariants pass directly to the next parent coefficient data.

Exact Jacobian composition for the child displacement.

theorem EulerChildParticleTime.displacement_jacobian {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D : SmoothTimeField K E E) (t : K) (x : E) : ContinuousLinearMap.id ℝ E + fderiv ℝ (⇑((displacement P D).field t)) x = (ContinuousLinearMap.id ℝ E + fderiv ℝ (⇑(P.field t)) (x + (D.field t) x)) ∘SL (ContinuousLinearMap.id ℝ E + fderiv ℝ (⇑(D.field t)) x)

theorem EulerChildParticleTime.displacement_det_one {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (P D : SmoothTimeField K E E) (t : K) (hP : ∀ (y : E), (ContinuousLinearMap.id ℝ E + fderiv ℝ (⇑(P.field t)) y).det = 1) (hD : ∀ (y : E), (ContinuousLinearMap.id ℝ E + fderiv ℝ (⇑(D.field t)) y).det = 1) (x : E) : (ContinuousLinearMap.id ℝ E + fderiv ℝ (⇑((displacement P D).field t)) x).det = 1

theorem EulerPhysicalGraphFlowBounds.Data.physicalDisplacementCoefficient_zero {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (x : EulerLiftedGradientSpace.Vector3) : ((G.physicalDisplacementCoefficient k m ell).field ⟨0, ⋯⟩) x = 0

theorem EulerPhysicalGraphFlowBounds.Data.physicalDisplacementCoefficient_det_one {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (ContinuousLinearMap.id ℝ EulerLiftedGradientSpace.Vector3 + fderiv ℝ (⇑((G.physicalDisplacementCoefficient k m ell).field t)) x).det = 1

theorem EulerPhysicalGraphFlowBounds.Data.childDisplacementCoefficient_zero {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (PD : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3) (hPD : ∀ (x : EulerLiftedGradientSpace.Vector3), (PD.field ⟨0, ⋯⟩) x = 0) (x : EulerLiftedGradientSpace.Vector3) : ((EulerChildParticleTime.displacement PD (G.physicalDisplacementCoefficient k m ell)).field ⟨0, ⋯⟩) x = 0

theorem EulerPhysicalGraphFlowBounds.Data.childDisplacementCoefficient_det_one {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (hell : 0 < ell) (PD : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3) (hPD : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), (ContinuousLinearMap.id ℝ EulerLiftedGradientSpace.Vector3 + fderiv ℝ (⇑(PD.field t)) x).det = 1) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (ContinuousLinearMap.id ℝ EulerLiftedGradientSpace.Vector3 + fderiv ℝ (⇑((EulerChildParticleTime.displacement PD (G.physicalDisplacementCoefficient k m ell)).field t)) x).det = 1

The L² child fields used in the estimates are exactly the actual first and second time derivatives of the composed particle map.

structure EulerChildParticleTime.Representation {T : ℝ} (G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data) (P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space) : Prop

Compatibility of two actual realizations of the six input fields. These are literal value identities, not derivative or output assumptions.

• parentDisplacement (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).parentDisplacement.field x = (P.field t) x
• parentVelocity (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).parentVelocity.field x = (P₁.field t) x
• parentAcceleration (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).parentAcceleration.field x = (P₂.field t) x
• displacement (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).displacement.field x = (D.field t) x
• velocity (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).velocity.field x = (D₁.field t) x
• acceleration (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).acceleration.field x = (D₂.field t) x

theorem EulerChildParticleTime.Representation.childDisplacement {T : ℝ} {G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data} {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space} (H : Representation G P P₁ P₂ D D₁ D₂) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).childDisplacement.field x = ((EulerChildParticleTime.displacement P D).field t) x

theorem EulerChildParticleTime.Representation.childVelocity {T : ℝ} {G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data} {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space} (H : Representation G P P₁ P₂ D D₁ D₂) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).childVelocity.field x = ((EulerChildParticleTime.velocity P P₁ D D₁).field t) x

theorem EulerChildParticleTime.Representation.childAcceleration {T : ℝ} {G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data} {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space} (H : Representation G P P₁ P₂ D D₁ D₂) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (G t).childAcceleration.field x = ((EulerChildParticleTime.acceleration P P₁ P₂ D D₁ D₂).field t) x

theorem EulerChildParticleTime.Representation.displacement_hasDerivWithinAt {T : ℝ} {G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data} {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space} (H : Representation G P P₁ P₂ D D₁ D₂) {hT : 0 ≤ T} (hP : SmoothTimeField.TimeDerivative T hT P P₁) (hD : SmoothTimeField.TimeDerivative T hT D D₁) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (G (Set.projIcc 0 T hT s)).childDisplacement.field x) ((G t).childVelocity.field x) (Set.Icc 0 T) ↑t

theorem EulerChildParticleTime.Representation.velocity_hasDerivWithinAt {T : ℝ} {G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data} {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space} (H : Representation G P P₁ P₂ D D₁ D₂) {hT : 0 ≤ T} (hP : SmoothTimeField.TimeDerivative T hT P P₁) (hP₁ : SmoothTimeField.TimeDerivative T hT P₁ P₂) (hD : SmoothTimeField.TimeDerivative T hT D D₁) (hD₁ : SmoothTimeField.TimeDerivative T hT D₁ D₂) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (G (Set.projIcc 0 T hT s)).childVelocity.field x) ((G t).childAcceleration.field x) (Set.Icc 0 T) ↑t

theorem EulerChildParticleTime.Representation.composition_hasDerivWithinAt {T : ℝ} {G : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data} {P P₁ P₂ D D₁ D₂ : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space} (H : Representation G P P₁ P₂ D D₁ D₂) {hT : 0 ≤ T} (hP : SmoothTimeField.TimeDerivative T hT P P₁) (hD : SmoothTimeField.TimeDerivative T hT D D₁) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => have F := G (Set.projIcc 0 T hT s); x + F.displacement.field x + F.parentDisplacement.field (x + F.displacement.field x)) ((G t).childVelocity.field x) (Set.Icc 0 T) ↑t

theorem EulerParentPacketFrames.Parent.displacement_det_one (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(A.displacement.field t)) x).det = 1

noncomputable def EulerParentPacketFrames.Parent.child (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) : Parent

Child, bundling T, T_pos, ell, ell_pos and the required compatibility proofs.

Equations

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

theorem EulerParentPacketFrames.Parent.child_particleMap (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) : x + ((A.child G k m hgraph nextEll hnext hnext1).displacement.field t) x = have y := (EulerSmoothBanachFlow.flowData A.T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m A.T G.A A.ell)).forward (↑t) x; y + (A.displacement.field t) y

theorem EulerParentPacketFrames.Parent.child_fields_match (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) (E : ↑(Set.Icc 0 A.T) → EulerChildParticleFieldBounds.Data) (hD : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (E t).parentDisplacement.field x = (A.displacement.field t) x) (hV : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (E t).parentVelocity.field x = (A.velocity.field t) x) (hW : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (E t).parentAcceleration.field x = (A.acceleration.field t) x) (hd : ∀ (t : ↑(Set.Icc 0 A.T)), (E t).displacement = G.displacementField k m A.ell ⋯ t) (hv : ∀ (t : ↑(Set.Icc 0 A.T)), (E t).velocity = G.velocityField k m A.ell ⋯ t) (hw : ∀ (t : ↑(Set.Icc 0 A.T)), (E t).acceleration = G.accelerationFieldL2 k m A.ell ⋯ t) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (E t).childDisplacement.field x = ((A.child G k m hgraph nextEll hnext hnext1).displacement.field t) x ∧ (E t).childVelocity.field x = ((A.child G k m hgraph nextEll hnext hnext1).velocity.field t) x ∧ (E t).childAcceleration.field x = ((A.child G k m hgraph nextEll hnext hnext1).acceleration.field t) x

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

Child inverse, given by (flowData A.T G.time_nonneg (physicalCoefficient k m A.T G.A A.ell)).backward t (Y t x).

Equations

• A.childInverse G k m Y t x = (EulerSmoothBanachFlow.flowData A.T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m A.T G.A A.ell)).backward (↑t) (Y t x)

theorem EulerParentPacketFrames.Parent.childInverse_left (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 : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (x + (A.displacement.field t) x) = x) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.childInverse G k m Y t (x + ((A.child G k m hgraph nextEll hnext hnext1).displacement.field t) x) = x

theorem EulerParentPacketFrames.Parent.childInverse_right (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 : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t x + (A.displacement.field t) (Y t x) = x) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.childInverse G k m Y t x + ((A.child G k m hgraph nextEll hnext hnext1).displacement.field t) (A.childInverse G k m Y t x) = x

theorem EulerParentPacketFrames.Parent.childInverse_joint_continuous (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Continuous (Function.uncurry Y)) : Continuous (Function.uncurry (A.childInverse G k m Y))

theorem EulerParentPacketFrames.Parent.child_particleMap_measurePreserving (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) (hparent : ∀ (t : ↑(Set.Icc 0 A.T)), MeasureTheory.MeasurePreserving (fun (x : EulerSmoothLimit.Space) => x + (A.displacement.field t) x) MeasureTheory.volume MeasureTheory.volume) (t : ↑(Set.Icc 0 A.T)) : MeasureTheory.MeasurePreserving (fun (x : EulerSmoothLimit.Space) => x + ((A.child G k m hgraph nextEll hnext hnext1).displacement.field t) x) MeasureTheory.volume MeasureTheory.volume