Documentation

TauCeti.Geometry.Manifold.Flow.Eulerian

The Eulerian velocity field of a smooth family of diffeomorphisms #

Let φ_t, t ∈ ℝ, be a family of bijections of a manifold M, jointly smooth in (t, x) and with jointly smooth inverses, such as a smooth isotopy. Its Eulerian velocity field is the time-dependent vector field

X_t = (∂_t φ_t) ∘ φ_t⁻¹, that is, X_t(y) = ∂_u|_{u = t} φ_u(φ_t⁻¹ y)

(TauCeti.eulerianField). It is the time-dependent vector field generating the family: every curve u ↦ φ_u x has velocity X_u (φ_u x) (TauCeti.hasMFDerivAt_eulerianField), and the field is jointly C^m when the family is C^(m+1) and its inverses are C^m (TauCeti.contMDiff_eulerianField). Consequently the suspension of X is complete (TauCeti.isCompleteVectorField_timeDependentSuspensionField_eulerianField), and on a Hausdorff boundaryless manifold, where integral curves of a C¹ field are unique, the time-dependent flow of X from time s to time t is φ_t ∘ φ_s⁻¹ (TauCeti.timeDependentFlowOf_eulerianField). This lets every statement about time-dependent flows be applied to smooth isotopies.

The field transforms under the pointwise operations on families as follows. For the pointwise composition (φ ψ)_t = φ_t ∘ ψ_t one has the product velocity identity

X_(φ ψ) = X_φ + (φ_t)_* X_ψ

(TauCeti.eulerianField_trans), and for the pointwise inverse X_(φ⁻¹) = -(φ_t⁻¹)_* X_φ (TauCeti.eulerianField_symm). A constant family has zero velocity (TauCeti.eulerianField_const).

These are the identities used to define the flux of a symplectic isotopy, whose velocity one-forms are the contractions ι_(X_t) ω of the symplectic form with the Eulerian field.

References #

source
noncomputable def TauCeti.eulerianField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [TopologicalSpace M] [ChartedSpace H M] (φ : ℝ → M ≃ M) (t : ℝ) (y : M) :
TangentSpace I y

The Eulerian velocity field of a family φ of bijections of M: the time-dependent vector field X_t(y) = ∂_u|_{u = t} φ_u(φ_t⁻¹ y), that is X_t = (∂_t φ_t) ∘ φ_t⁻¹. For a smooth isotopy it is the time-dependent vector field whose flow is the isotopy.

Instances For
    source
    theorem TauCeti.eulerianField_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} {t : ℝ} (y : M) :
    eulerianField I φ t y = Manifold.curveVelocity I (fun (u : ℝ) => (φ u) ((φ t).symm y)) t

    The Eulerian velocity field at y is the velocity at time t of the curve u ↦ φ_u(φ_t⁻¹ y). This restates the definition, whose body is not exposed.

    source
    @[simp]
    theorem TauCeti.eulerianField_apply_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} {t : ℝ} (x : M) :
    eulerianField I φ t ((φ t) x) = Manifold.curveVelocity I (fun (u : ℝ) => (φ u) x) t

    At the image point φ_t x, the Eulerian velocity field is the velocity at time t of the curve u ↦ φ_u x.

    source
    theorem TauCeti.hasMFDerivAt_eulerianField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} {t : ℝ} {x : M} (h : (MDiffAt fun (u : ℝ) => (φ u) x) t) :
    HasMFDerivAt% (fun (u : ℝ) => (φ u) x) t (ContinuousLinearMap.smulRight 1 (eulerianField I φ t ((φ t) x)))

    The Eulerian field generates the family. If the curve u ↦ φ_u x is differentiable at time t, its velocity there is the Eulerian velocity field at its current position, X_t (φ_t x).

    source
    @[simp]
    theorem TauCeti.eulerianField_const {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (e : M ≃ M) :
    (eulerianField I fun (x : ℝ) => e) = 0

    A constant family has zero Eulerian velocity.

    Products and inverses of families #

    source
    theorem TauCeti.eulerianField_trans {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ ψ : ℝ → M ≃ M} {t : ℝ} {w : M} (hφ : (MDiffAt fun (p : ℝ × M) => (φ p.1) p.2) (t, w)) (hψ : (MDiffAt fun (u : ℝ) => (ψ u) ((ψ t).symm w)) t) :
    eulerianField I (fun (u : ℝ) => (ψ u).trans (φ u)) t ((φ t) w) = eulerianField I φ t ((φ t) w) + (mfderiv% ⇑(φ t) w) (eulerianField I ψ t w)

    The product velocity identity. The Eulerian field of the pointwise composition (φ ψ)_t = φ_t ∘ ψ_t of two families is X_(φ ψ) = X_φ + (φ_t)_* X_ψ: at the point φ_t w, it is the sum of X_φ(φ_t w) and of the image under dφ_t of X_ψ(w).

    source
    theorem TauCeti.eulerianField_symm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} {t : ℝ} {z : M} (hφ : (MDiffAt fun (p : ℝ × M) => (φ p.1).symm p.2) (t, z)) (hφ' : (MDiffAt fun (u : ℝ) => (φ u) ((φ t).symm z)) t) :
    eulerianField I (fun (u : ℝ) => (φ u).symm) t ((φ t).symm z) = -(mfderiv% ⇑(φ t).symm z) (eulerianField I φ t z)

    The inverse velocity identity. The Eulerian field of the pointwise inverse t ↦ φ_t⁻¹ of a family is X_(φ⁻¹) = -(φ_t⁻¹)_* X_φ: at the point φ_t⁻¹ z, it is minus the image under d(φ_t⁻¹) of X_φ(z).

    Smoothness #

    source
    theorem TauCeti.contMDiff_eulerianField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} [IsManifold I 1 M] {m n : WithTop ℕ∞} (hmn : m + 1 ≤ n) (hφ : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I n fun (p : ℝ × M) => (φ p.1) p.2) (hφ' : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I m fun (p : ℝ × M) => (φ p.1).symm p.2) :
    ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent m fun (p : ℝ × M) => ⟨p.2, eulerianField I φ p.1 p.2⟩

    The Eulerian field is jointly smooth. If the family (t, x) ↦ φ_t x is C^n and its inverses (t, y) ↦ φ_t⁻¹ y are C^m, with m + 1 ≤ n, then the Eulerian velocity field is a jointly C^m time-dependent vector field.

    The time-dependent flow of the Eulerian field #

    source
    theorem TauCeti.isCompleteVectorField_timeDependentSuspensionField_eulerianField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} (hφ : ∀ (x : M), MDiff fun (u : ℝ) => (φ u) x) :
    IsCompleteVectorField (timeDependentSuspensionField (eulerianField I φ))

    If every curve u ↦ φ_u x is differentiable, the suspension of the Eulerian field is complete: its time-dependent flow is defined for all pairs of times.

    source
    theorem TauCeti.timeDependentFlowOf_eulerianField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {φ : ℝ → M ≃ M} (hφ : ∀ (x : M), MDiff fun (u : ℝ) => (φ u) x) [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, eulerianField I φ p.1 p.2⟩) (s t : ℝ) (x : M) :
    timeDependentFlowOf (eulerianField I φ) s t x = (φ t) ((φ s).symm x)

    The isotopy is the flow of its Eulerian field. For a family whose curves u ↦ φ_u x are differentiable and whose Eulerian field is jointly C¹, the time-dependent flow of that field from time s to time t is φ_t ∘ φ_s⁻¹.