A genuine determinant-one flow transports continuous spatial L² paths through its actual inverse, preserving the norm exactly.

def EulerFlowL2Transport.inverseHomeomorph (X Y : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hYX : Function.LeftInverse Y X) (hXY : Function.RightInverse Y X) (hX : Continuous X) (hY : Continuous Y) : EulerLiftedGradientSpace.Vector3 ≃ₜ EulerLiftedGradientSpace.Vector3

Inverse homeomorph, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations

• EulerFlowL2Transport.inverseHomeomorph X Y hYX hXY hX hY = { toFun := X, invFun := Y, left_inv := hYX, right_inv := hXY, continuous_toFun := hX, continuous_invFun := hY }

theorem EulerFlowL2Transport.inverse_measurePreserving (X Y : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (F : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hX : ∀ (x : EulerLiftedGradientSpace.Vector3), HasFDerivAt X (F x) x) (hYX : Function.LeftInverse Y X) (hXY : Function.RightInverse Y X) (hY : Continuous Y) (hdet : ∀ (x : EulerLiftedGradientSpace.Vector3), (F x).det = 1) : MeasureTheory.MeasurePreserving Y MeasureTheory.volume MeasureTheory.volume

def EulerFlowL2Transport.inversePath {K : Type u_1} [TopologicalSpace K] (Y : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hY : Continuous (Function.uncurry Y)) : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))

Inverse path, given by (⟨Function.uncurry Y,hY⟩ : C(K × Vector3,Vector3)).curry.

Equations

• EulerFlowL2Transport.inversePath Y hY = { toFun := Function.uncurry Y, continuous_toFun := hY }.curry

theorem EulerFlowL2Transport.inversePath_measurePreserving {K : Type u_1} [TopologicalSpace K] (X Y : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (F : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hX : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), HasFDerivAt (X t) (F t x) x) (hYX : ∀ (t : K), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : K), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), (F t x).det = 1) (t : K) : MeasureTheory.MeasurePreserving (⇑((inversePath Y hY) t)) MeasureTheory.volume MeasureTheory.volume

noncomputable def EulerFlowL2Transport.transportPath {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [NormedAddCommGroup E] (X Y : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (F : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hX : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), HasFDerivAt (X t) (F t x) x) (hYX : ∀ (t : K), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : K), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), (F t x).det = 1) (u : C(K, ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))) : C(K, ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))

No operator-norm continuity of composition is assumed. Joint strong continuity follows from actual continuity and preservation of volume.

Equations

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

theorem EulerFlowL2Transport.transportPath_norm {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [NormedAddCommGroup E] (X Y : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (F : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hX : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), HasFDerivAt (X t) (F t x) x) (hYX : ∀ (t : K), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : K), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), (F t x).det = 1) (u : C(K, ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))) (t : K) : ‖(transportPath X Y F hX hYX hXY hY hdet u) t‖ = ‖u t‖

theorem EulerFlowL2Transport.transportPath_ae {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [NormedAddCommGroup E] (X Y : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (F : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hX : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), HasFDerivAt (X t) (F t x) x) (hYX : ∀ (t : K), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : K), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), (F t x).det = 1) (u : C(K, ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))) (f : K → EulerLiftedGradientSpace.Vector3 → E) (hu : ∀ (t : K), ↑↑(u t) =ᵐ[MeasureTheory.volume] f t) (t : K) : ↑↑((transportPath X Y F hX hYX hXY hY hdet u) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => f t (Y t x)