MoserFlowRegularity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional flow regularity for the Moser trajectories.

theorem OAI.ContinuumCoulomb.moser_flow_C4 line 12
theorem OAI.ContinuumCoulomb.moser_flow_uniform_derivatives line 25

theorem OAI.ContinuumCoulomb.moser_C4_bilipschitz_flow_exists line 39

Source documentation

All properties concern a single family of actual ODE trajectories.

theorem moser_C4_bilipschitz_flow_exists (hpublished : PublishedC4FlowInput)
    {rho : ℝ} (hrho : 0 < rho) (V : Position → ℝ) (hV : ContDiff ℝ 6 V)
    (hc : HasCompactSupport V) (hbound : ∀ x, |manufacturedCharge V x| ≤ rho/2) :
    ∃ (G : Position → ℝ → Position) (C Cinv : ℝ≥0) (D : ℝ),
      0 < D ∧ IsUnitTimeFlow (moserVelocity rho V) G ∧
      Function.Bijective (fun x => G x 1) ∧
      LipschitzWith C (fun x => G x 1) ∧
      AntilipschitzWith Cinv (fun x => G x 1) ∧
      (∀ x, x ∉ tsupport V → G x 1 = x) ∧
      ContDiff ℝ 4 (fun x => G x 1) ∧
      (∀ r : ℕ, 1 ≤ r → r ≤ 4 → ∀ x,
        ‖iteratedFDeriv ℝ r (fun y => G y 1) x‖ ≤ D) := by
…

Mentions: OAI.ContinuumCoulomb.PublishedC4FlowInput, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.manufacturedCharge, OAI.ContinuumCoulomb.IsUnitTimeFlow, OAI.ContinuumCoulomb.moserVelocity