Differentiable dependence of a flow on its initial point, and flat Liouville

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Q29(b′) of specs/generator-layer-scoping.md.

Mathlib's Picard–Lindelöf theorem gives existence, uniqueness and Lipschitz dependence of the local flow of a C¹ vector field on the initial point, but not differentiable dependence. This file proves it, with the derivative given by the variational equation, and draws the consequence the corpus needs: a C¹ 2-form whose flat Lie derivative along the field vanishes is pulled back to itself by the local flow (the flat Liouville theorem).

• gronwallBound_zero_le — the Grönwall bound with zero initial gap is at most ε x e^{K x};
• exists_linearODE_solution — the linear ODE Y' = A(t) Y on a Banach space has a solution on a short interval whose length depends only on a bound for ‖A‖ and on ‖Y₀‖ (Picard–Lindelöf on the operator space); exists_linearODE_solution_of_le — on all of [0, T] when T · M · (‖Y₀‖ + 1) ≤ 1; ★ exists_linearODE_solution_Icc — on all of [0, T] with no smallness condition, by concatenating short-time solutions (hasDerivWithinAt_Icc_glue), the step length fixed by the Grönwall bound ‖Y t‖ ≤ ‖Y 0‖ e^{M t} (norm_le_mul_exp_of_linearODE);
• norm_le_exp_of_linearODE — a solution of the operator-valued Y' = A(t) ∘ Y, Y 0 = 1, ‖A‖ ≤ M has ‖Y t‖ ≤ e^{M t}; ★ dist_le_of_linearODE_coeff_close — continuous dependence of a linear ODE's solution on its coefficient: two such solutions whose coefficients are ε-close on [0, T] are within ε e^{M T} · T e^{M T} (Grönwall for approximate trajectories on the operator space);
• ★★ hasFDerivAt_flow_of_variational_timeDependent — differentiable dependence, for a time-dependent field: for f t differentiable on an open set with (t, z) ↦ D(f t)(z) continuous, a flow α confined to a compact and Lipschitz in the initial point, and a solution Y of the variational equation Y' = D(f t)(α x t) ∘ Y, Y 0 = 1, the time-t map is differentiable at x with derivative Y t. The proof is Grönwall's inequality for approximate trajectories (dist_le_of_approx_trajectories_ODE_of_mem): the difference of two trajectories is an approximate solution of the linearised equation, with defect controlled by the mean value inequality and the uniform continuity of (t, z) ↦ D(f t)(z) on a compact thickening; ★★ hasFDerivAt_flow_of_variational is the autonomous case;
• ★ ContDiffAt.exists_localFlow_hasFDerivAt — a C¹ field has a local flow, confined to a prescribed neighbourhood, differentiable in the initial point for a uniform short time;
• ★ exists_flow_hasFDerivAt_of_norm_fderiv_le — the flow of a small time-dependent field up to a prescribed time T (‖D(f t)‖ ≤ M on a ball, M T ≤ 1/2, f t x₀ = 0): trajectories on [0, T] confined to the ball, the Grönwall separation e^{M t}, the variational derivative at every point of the half-ball, and its continuous dependence on the point (x ↦ Dφ_t(x) is continuous, so the time-t map is C¹) — what Moser's trick needs (Darboux, time 1);
• flatLieDeriv — the flat Lie derivative of a 2-form along a field, (L_X ω)(m) = Dω(X)(m) + ω(DX m₀, m₁) + ω(m₀, DX m₁);
• ★ form_invariant_of_flatLieDeriv_eq_zero_timeDependent — flat transport for a time-dependent form and field: along an integral curve with its variational solution, Ω t (α t) (Y t ∘ m) = Ω 0 (α 0) m when ∂ₜΩ + L_{f t} Ω t = 0 (constant_of_has_deriv_right_zero on the product-rule derivative); ★ form_invariant_of_flatLieDeriv_eq_zero is the autonomous case, ω (α t) (Y t ∘ m) = ω (α 0) m when the flat Lie derivative vanishes;
• ★★ ContDiffAt.exists_localFlow_form_invariant — flat Liouville: the local flow pulls the form back to itself, (ω (α x t)).compContinuousLinearMap (D(α · t) x) = ω x, confined to a prescribed neighbourhood.

C^n dependence of a flow on its initial point, for every n ≤ ∞, is Analysis/ODE/FlowSmooth.lean, on top of exists_linearODE_solution_Icc and the C¹ case here.

The local flow solves the equation on [-ε, ε] (what the identification with the manifold flow by uniqueness on an open interval needs); the derivative and the invariance are for forward time t ∈ [0, ε] on a proper space (finite-dimensional in the application), and negative times follow downstream from the group law of the manifold flow. The flat Cartan formula identifying flatLieDeriv with d(ι_X ω) + ι_X dω is Geometry/Manifold/HamiltonianLieDerivative.lean (Q29(c′)); the manifold assembly is Geometry/Manifold/HamiltonianFlowVolume.lean (Q29(d′)).

theorem gronwallBound_zero_le {K ε x : ℝ} (hK : 0 ≤ K) (hε : 0 ≤ ε) (_hx : 0 ≤ x) : gronwallBound 0 K ε x ≤ ε * (x * Real.exp (K * x))

The Grönwall bound with zero initial gap is at most ε x e^{K x}.

theorem exists_linearODE_solution {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (A : ℝ → F →L[ℝ] F) {T M τ : ℝ} (hT : 0 < T) (hA : ∀ (Y : F), ContinuousOn (fun (t : ℝ) => (A t) Y) (Set.Icc 0 T)) (hM : ∀ t ∈ Set.Icc 0 T, ‖A t‖ ≤ M) (Y₀ : F) (hτ0 : 0 < τ) (hτT : τ ≤ T) (hτL : τ * (M * (‖Y₀‖ + 1) + 1) ≤ 1) : ∃ (Y : ℝ → F), Y 0 = Y₀ ∧ ∀ t ∈ Set.Icc 0 τ, HasDerivWithinAt Y ((A t) (Y t)) (Set.Icc 0 τ) t

The linear ODE Y' = A(t) Y has a solution on a short interval whose length depends only on a bound for ‖A‖ and on ‖Y₀‖ (Picard–Lindelöf on the Banach space F).

theorem exists_linearODE_solution_of_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (A : ℝ → F →L[ℝ] F) {T M : ℝ} (hT : 0 < T) (hA : ∀ (Y : F), ContinuousOn (fun (t : ℝ) => (A t) Y) (Set.Icc 0 T)) (hM : ∀ t ∈ Set.Icc 0 T, ‖A t‖ ≤ M) (Y₀ : F) (hTL : T * (M * (‖Y₀‖ + 1)) ≤ 1) : ∃ (Y : ℝ → F), Y 0 = Y₀ ∧ ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y ((A t) (Y t)) (Set.Icc 0 T) t

The linear ODE Y' = A(t) Y has a solution on the whole of [0, T] when T · M · (‖Y₀‖ + 1) ≤ 1, M a bound for ‖A‖ (Picard–Lindelöf on the Banach space F, on the ball of radius 1 about Y₀).

theorem norm_le_mul_exp_of_linearODE {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (A : ℝ → F →L[ℝ] F) {T M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ t ∈ Set.Icc 0 T, ‖A t‖ ≤ M) {Y : ℝ → F} (hY : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y ((A t) (Y t)) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → ‖Y t‖ ≤ ‖Y 0‖ * Real.exp (M * t)

A solution of the linear ODE Y' = A(t) Y with ‖A t‖ ≤ M on [0, T] has ‖Y t‖ ≤ ‖Y 0‖ e^{M t} there (Grönwall against the zero solution).

theorem hasDerivWithinAt_Icc_glue {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {v : ℝ → F → F} {Y₁ Y₂ : ℝ → F} {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) (h₁ : ∀ t ∈ Set.Icc a b, HasDerivWithinAt Y₁ (v t (Y₁ t)) (Set.Icc a b) t) (h₂ : ∀ t ∈ Set.Icc b c, HasDerivWithinAt Y₂ (v t (Y₂ t)) (Set.Icc b c) t) (hj : Y₁ b = Y₂ b) (t : ℝ) : t ∈ Set.Icc a c → HasDerivWithinAt (fun (s : ℝ) => if s ≤ b then Y₁ s else Y₂ s) (v t (if t ≤ b then Y₁ t else Y₂ t)) (Set.Icc a c) t

Two solutions of Y' = v(t, Y) on adjacent intervals [a, b] and [b, c] that agree at b glue to a solution on [a, c].

theorem exists_linearODE_solution_Icc {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (A : ℝ → F →L[ℝ] F) {T M : ℝ} (hT : 0 < T) (hM0 : 0 ≤ M) (hA : ∀ (Y : F), ContinuousOn (fun (t : ℝ) => (A t) Y) (Set.Icc 0 T)) (hM : ∀ t ∈ Set.Icc 0 T, ‖A t‖ ≤ M) (Y₀ : F) : ∃ (Y : ℝ → F), Y 0 = Y₀ ∧ ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y ((A t) (Y t)) (Set.Icc 0 T) t

★ The linear ODE Y' = A(t) Y has a solution on all of [0, T] — no smallness condition. The short-time solutions of exists_linearODE_solution are concatenated (hasDerivWithinAt_Icc_glue), the step length τ being fixed by the Grönwall bound ‖Y t‖ ≤ ‖Y₀‖ e^{M T} that every partial solution obeys.

theorem norm_le_exp_of_linearODE {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A Y : ℝ → E →L[ℝ] E} {T M : ℝ} (hM0 : 0 ≤ M) (hA : ∀ t ∈ Set.Icc 0 T, ‖A t‖ ≤ M) (hY0 : Y 0 = 1) (hYd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y (A t ∘SL Y t) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → ‖Y t‖ ≤ Real.exp (M * t)

A solution of the operator-valued linear ODE Y' = A(t) ∘ Y, Y 0 = 1, with ‖A t‖ ≤ M on [0, T], has ‖Y t‖ ≤ e^{M t} there (Grönwall against the zero solution).

theorem dist_le_of_linearODE_coeff_close {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A B Y Z : ℝ → E →L[ℝ] E} {T M ε : ℝ} (hM0 : 0 ≤ M) (hε : 0 ≤ ε) (hA : ∀ t ∈ Set.Icc 0 T, ‖A t‖ ≤ M) (hB : ∀ t ∈ Set.Icc 0 T, ‖B t‖ ≤ M) (hAB : ∀ t ∈ Set.Icc 0 T, ‖B t - A t‖ ≤ ε) (hY0 : Y 0 = 1) (hYd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y (A t ∘SL Y t) (Set.Icc 0 T) t) (hZ0 : Z 0 = 1) (hZd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Z (B t ∘SL Z t) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → dist (Y t) (Z t) ≤ ε * Real.exp (M * T) * (T * Real.exp (M * T))

★ Continuous dependence of the solution of a linear ODE on its coefficient. Two solutions of Y' = A(t) ∘ Y, Z' = B(t) ∘ Z with Y 0 = Z 0 = 1, ‖A‖, ‖B‖ ≤ M and ‖B − A‖ ≤ ε on [0, T] are within ε e^{M T} · T e^{M T} on [0, T]: Z is an approximate trajectory of Y's equation with defect ‖(B − A) ∘ Z‖ ≤ ε e^{M T}, and Grönwall (dist_le_of_approx_trajectories_ODE_of_mem) bounds the gap.

theorem hasFDerivAt_flow_of_variational_timeDependent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] {f : ℝ → E → E} {U : Set E} (hU : IsOpen U) {T : ℝ} (hT : 0 < T) (hfd : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ U, HasFDerivAt (f t) (fderiv ℝ (f t) z) z) (hDc : ContinuousOn (fun (p : ℝ × E) => fderiv ℝ (f p.1) p.2) (Set.Icc 0 T ×ˢ U)) {K : Set E} (hK : IsCompact K) (hKU : K ⊆ U) {α : E → ℝ → E} {x : E} {ρ : ℝ} (hρ : 0 < ρ) (hα0 : ∀ y ∈ Metric.closedBall x ρ, α y 0 = y) (hαd : ∀ y ∈ Metric.closedBall x ρ, ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (α y) (f t (α y t)) (Set.Icc 0 T) t) (hαK : ∀ y ∈ Metric.closedBall x ρ, ∀ t ∈ Set.Icc 0 T, α y t ∈ K) {L' : NNReal} (hlip : ∀ t ∈ Set.Icc 0 T, LipschitzOnWith L' (fun (x : E) => α x t) (Metric.closedBall x ρ)) {Y : ℝ → E →L[ℝ] E} (hY0 : Y 0 = 1) (hYd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y (fderiv ℝ (f t) (α x t) ∘SL Y t) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → HasFDerivAt (fun (x : E) => α x t) (Y t) x

Differentiable dependence of a flow on the initial point, with the variational equation, for a time-dependent field. Let f t be differentiable on an open U for t ∈ [0, T] with (t, z) ↦ D(f t)(z) continuous, α a flow of f on a closed ball around x for times in [0, T], confined to a compact K ⊆ U and Lipschitz in the initial point uniformly in time, and let Y solve the linear variational equation Y' = D(f t)(α x t) ∘ Y, Y 0 = 1, along the curve of x. Then α · t is differentiable at x with derivative Y t.

theorem hasFDerivAt_flow_of_variational {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] {f : E → E} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ 1 f U) {K : Set E} (hK : IsCompact K) (hKU : K ⊆ U) {α : E → ℝ → E} {x : E} {ρ T : ℝ} (hρ : 0 < ρ) (hT : 0 < T) (hα0 : ∀ y ∈ Metric.closedBall x ρ, α y 0 = y) (hαd : ∀ y ∈ Metric.closedBall x ρ, ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (α y) (f (α y t)) (Set.Icc 0 T) t) (hαK : ∀ y ∈ Metric.closedBall x ρ, ∀ t ∈ Set.Icc 0 T, α y t ∈ K) {L' : NNReal} (hlip : ∀ t ∈ Set.Icc 0 T, LipschitzOnWith L' (fun (x : E) => α x t) (Metric.closedBall x ρ)) {Y : ℝ → E →L[ℝ] E} (hY0 : Y 0 = 1) (hYd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y (fderiv ℝ f (α x t) ∘SL Y t) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → HasFDerivAt (fun (x : E) => α x t) (Y t) x

Differentiable dependence of a flow on the initial point, with the variational equation. Let f be C¹ on an open U, α a flow of f on a closed ball around x for times in [0, T], confined to a compact K ⊆ U and Lipschitz in the initial point uniformly in time, and let Y solve the linear variational equation Y' = Df(α x t) ∘ Y, Y 0 = 1, along the curve of x. Then α · t is differentiable at x with derivative Y t (hasFDerivAt_flow_of_variational_timeDependent for the constant family).

theorem ContDiffAt.exists_localFlow_hasFDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [ProperSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) {s : Set E} (hs : s ∈ nhds x₀) : ∃ (U : Set E), IsOpen U ∧ x₀ ∈ U ∧ U ⊆ s ∧ ContDiffOn ℝ 1 f U ∧ ∃ r > 0, ∃ ε > 0, ∃ (α : E → ℝ → E) (Y : E → ℝ → E →L[ℝ] E), (∀ x ∈ Metric.closedBall x₀ r, α x 0 = x ∧ (∀ t ∈ Set.Icc (-ε) ε, HasDerivWithinAt (α x) (f (α x t)) (Set.Icc (-ε) ε) t) ∧ ∀ (t : ℝ), α x t ∈ U) ∧ ∀ x ∈ Metric.ball x₀ r, Y x 0 = 1 ∧ (∀ t ∈ Set.Icc 0 ε, HasDerivWithinAt (Y x) (fderiv ℝ f (α x t) ∘SL Y x t) (Set.Icc 0 ε) t) ∧ ∀ t ∈ Set.Icc 0 ε, HasFDerivAt (fun (x : E) => α x t) (Y x t) x

A C¹ field has a local flow that is differentiable in the initial point, with the derivative solving the variational equation along the curve. The flow satisfies the equation on [-ε, ε]; the derivative is established for forward times [0, ε].

theorem exists_flow_hasFDerivAt_of_norm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [ProperSpace E] {f : ℝ → E → E} {x₀ : E} {a T M : ℝ} (ha : 0 < a) (hT : 0 < T) {U : Set E} (hU : IsOpen U) (haU : Metric.closedBall x₀ a ⊆ U) (hfc : ContinuousOn (Function.uncurry f) (Set.Icc 0 T ×ˢ U)) (hfd : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ U, HasFDerivAt (f t) (fderiv ℝ (f t) z) z) (hDc : ContinuousOn (fun (p : ℝ × E) => fderiv ℝ (f p.1) p.2) (Set.Icc 0 T ×ˢ U)) (hM0 : 0 ≤ M) (hM : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ Metric.closedBall x₀ a, ‖fderiv ℝ (f t) z‖ ≤ M) (hMT : M * T ≤ 1 / 2) (hf0 : ∀ t ∈ Set.Icc 0 T, f t x₀ = 0) : ∃ (α : E → ℝ → E) (Y : E → ℝ → E →L[ℝ] E), (∀ x ∈ Metric.closedBall x₀ (a / 2), α x 0 = x ∧ (∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc 0 T) t) ∧ ∀ (t : ℝ), α x t ∈ Metric.closedBall x₀ a) ∧ (∀ x ∈ Metric.closedBall x₀ (a / 2), ∀ y ∈ Metric.closedBall x₀ (a / 2), ∀ t ∈ Set.Icc 0 T, dist (α x t) (α y t) ≤ dist x y * Real.exp (M * t)) ∧ (∀ x ∈ Metric.ball x₀ (a / 2), Y x 0 = 1 ∧ (∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (Y x) (fderiv ℝ (f t) (α x t) ∘SL Y x t) (Set.Icc 0 T) t) ∧ ∀ t ∈ Set.Icc 0 T, HasFDerivAt (fun (x : E) => α x t) (Y x t) x) ∧ ∀ t ∈ Set.Icc 0 T, ContinuousOn (fun (x : E) => Y x t) (Metric.ball x₀ (a / 2))

★ The flow of a small time-dependent field, up to time T, with its variational solution and its Grönwall estimate. Let f t be differentiable on an open U ⊇ closedBall x₀ a for t ∈ [0, T], with f and (t, z) ↦ D(f t)(z) continuous on [0, T] × U, ‖D(f t)(z)‖ ≤ M on [0, T] × closedBall x₀ a with M T ≤ 1/2, and f t x₀ = 0. Then every x ∈ closedBall x₀ (a/2) has a trajectory on [0, T] confined to closedBall x₀ a, two trajectories separate by at most e^{M t} times their initial distance, for x ∈ ball x₀ (a/2) the time-t map is differentiable at x with derivative the variational solution Y x t, and x ↦ Y x t is continuous on the half-ball (so the time-t map is C¹ there). (Picard–Lindelöf on [0, T] directly: the field is M a-bounded and M-Lipschitz on the ball, and M a T ≤ a/2; the continuity is dist_le_of_linearODE_coeff_close with the uniform continuity of (t, z) ↦ D(f t)(z) on [0, T] × closedBall x₀ a and the Grönwall separation.)

The flat Lie derivative and Liouville

noncomputable def flatLieDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X : E → E) (Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (z : E) (m : Fin 2 → E) : ℝ

The flat Lie derivative of a 2-form Ω along a vector field X, as a bilinear expression: (L_X Ω)(z)(m) = DΩ(z)(X z)(m) + Ω(z)(DX(z) m₀, m₁) + Ω(z)(m₀, DX(z) m₁).

Equations

• flatLieDeriv X Ω z m = ((fderiv ℝ Ω z) (X z)) m + ∑ i : Fin 2, (Ω z) (Function.update m i ((fderiv ℝ X z) (m i)))

theorem form_invariant_of_flatLieDeriv_eq_zero_timeDependent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {U : Set E} {T : ℝ} {Ω : ℝ → E → E [⋀^Fin 2]→L[ℝ] ℝ} (hΩ : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ U, DifferentiableAt ℝ (Function.uncurry Ω) (t, z)) (hL : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ U, ∀ (m : Fin 2 → E), ((fderiv ℝ (Function.uncurry Ω) (t, z)) (1, f t z)) m + ∑ i : Fin 2, (Ω t z) (Function.update m i ((fderiv ℝ (f t) z) (m i))) = 0) {α : ℝ → E} {x : E} (hα0 : α 0 = x) (hαd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt α (f t (α t)) (Set.Icc 0 T) t) (hαU : ∀ t ∈ Set.Icc 0 T, α t ∈ U) {Y : ℝ → E →L[ℝ] E} (hY0 : Y 0 = 1) (hYd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y (fderiv ℝ (f t) (α t) ∘SL Y t) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (m : Fin 2 → E), ((Ω t (α t)) fun (i : Fin 2) => (Y t) (m i)) = (Ω 0 x) m

Flat transport for a time-dependent form and field. If Ω t is a family of 2-forms, jointly differentiable in (t, z) on [0, T] × U, and ∂ₜΩ + L_{f t} Ω t = 0 there — as the combined condition DΩ(t, z)(1, f t z) m + ∑ᵢ Ω t z (update m i (D(f t)(z) (m i))) = 0 — then along any integral curve α of f with its variational solution Y, Ω t (α t) (Y t ∘ m) = Ω 0 (α 0) m (constant_of_has_deriv_right_zero on the product-rule derivative).

theorem form_invariant_of_flatLieDeriv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → E} {U : Set E} (hU : IsOpen U) {Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} (hΩ : ContDiffOn ℝ 1 Ω U) (hL : ∀ z ∈ U, ∀ (m : Fin 2 → E), flatLieDeriv f Ω z m = 0) {α : ℝ → E} {x : E} {T : ℝ} (hα0 : α 0 = x) (hαd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt α (f (α t)) (Set.Icc 0 T) t) (hαU : ∀ t ∈ Set.Icc 0 T, α t ∈ U) {Y : ℝ → E →L[ℝ] E} (hY0 : Y 0 = 1) (hYd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Y (fderiv ℝ f (α t) ∘SL Y t) (Set.Icc 0 T) t) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (m : Fin 2 → E), ((Ω (α t)) fun (i : Fin 2) => (Y t) (m i)) = (Ω x) m

Flat Liouville. If the flat Lie derivative of a C¹ 2-form along a C¹ field vanishes on an open set, then along any integral curve α with the variational solution Y, the pullback of the form is constant: Ω (α t) (Y t ∘ m) = Ω (α 0) m (form_invariant_of_flatLieDeriv_eq_zero_timeDependent for constant families).

theorem ContDiffAt.exists_localFlow_form_invariant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [ProperSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) {Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} (hΩ : ContDiffAt ℝ 1 Ω x₀) (hL : ∀ᶠ (z : E) in nhds x₀, ∀ (m : Fin 2 → E), flatLieDeriv f Ω z m = 0) {s : Set E} (hs : s ∈ nhds x₀) : ∃ r > 0, ∃ ε > 0, ∃ (α : E → ℝ → E) (Y : E → ℝ → E →L[ℝ] E), (∀ x ∈ Metric.closedBall x₀ r, α x 0 = x ∧ (∀ t ∈ Set.Icc (-ε) ε, HasDerivWithinAt (α x) (f (α x t)) (Set.Icc (-ε) ε) t) ∧ ∀ (t : ℝ), α x t ∈ s) ∧ ∀ x ∈ Metric.ball x₀ r, ∀ t ∈ Set.Icc 0 ε, HasFDerivAt (fun (x : E) => α x t) (Y x t) x ∧ (Ω (α x t)).compContinuousLinearMap (Y x t) = Ω x

★★ Flat Liouville for the local flow of a C¹ field. If the flat Lie derivative of a C¹ 2-form Ω along a C¹ field f vanishes near x₀, the local flow α of f near x₀ is differentiable in the initial point and pulls Ω back to itself: (Ω (α x t)).compContinuousLinearMap (D(α · t) x) = Ω x.