The inverse carried by the physical particle map. Preservation of volume follows from the actual determinant, and both time restriction and the packet child propagate the two inverse laws.

structure EulerParentPacketFrames.ParticleInverse (A : Parent) : Type

Particle inverse data, collecting field, left_inverse, right_inverse, continuous.

• field : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space

  Underlying field of ParticleInverse, of type Icc (0 : ℝ) A.T → Space → Space.

• left_inverse (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : self.field t (A.position t x) = x
• right_inverse (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.position t (self.field t x) = x
• continuous : Continuous (Function.uncurry self.field)

theorem EulerParentPacketFrames.Parent.position_contDiff (A : Parent) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ (↑⊤) (A.position t)

theorem EulerParentPacketFrames.Parent.packetPosition_contDiff (A : Parent) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => A.packetPosition (↑t, x)

theorem EulerParentPacketFrames.ParticleInverse.position_bijective {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : Function.Bijective (A.position t)

theorem EulerParentPacketFrames.ParticleInverse.field_initial {A : Parent} (I : ParticleInverse A) (x : EulerSmoothLimit.Space) : I.field A.zeroTime x = x

theorem EulerParentPacketFrames.ParticleInverse.position_measurePreserving {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : MeasureTheory.MeasurePreserving (A.position t) MeasureTheory.volume MeasureTheory.volume

theorem EulerParentPacketFrames.ParticleInverse.field_measurePreserving {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : MeasureTheory.MeasurePreserving (I.field t) MeasureTheory.volume MeasureTheory.volume

noncomputable def EulerParentPacketFrames.ParticleInverse.normalized {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Normalized, given by A.packetInverse I.field (t,x).

Equations

• I.normalized t x = A.packetInverse I.field (↑t, x)

theorem EulerParentPacketFrames.ParticleInverse.normalized_left {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : I.normalized t (A.packetPosition (↑t, x)) = x

theorem EulerParentPacketFrames.ParticleInverse.normalized_right {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.packetPosition (↑t, I.normalized t x) = x

theorem EulerParentPacketFrames.ParticleInverse.normalized_continuous {A : Parent} (I : ParticleInverse A) : Continuous (Function.uncurry I.normalized)

def EulerParentPacketFrames.ParticleInverse.restrictTime {A : Parent} (I : ParticleInverse A) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) : ParticleInverse (A.restrictTime S hS hST)

Restrict time, bundling field, left_inverse, right_inverse, continuous.

Equations

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

noncomputable def EulerParentPacketFrames.ParticleInverse.child {A : Parent} (I : ParticleInverse A) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerSmoothLimit.Space) (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) : ParticleInverse (A.child G k m hgraph nextEll hnext hnext1)

Child, bundling field, left_inverse, right_inverse, continuous.

Equations

• I.child G k m hgraph nextEll hnext hnext1 = { field := A.childInverse G k m I.field, left_inverse := ⋯, right_inverse := ⋯, continuous := ⋯ }