MoserInverse.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Backward stability gives the separation bound required for mapped quadrature nodes. Compactly supported motion also preserves the enclosing slab.

theorem OAI.ContinuumCoulomb.moser_trajectory_backward_bound line 13

theorem OAI.ContinuumCoulomb.moser_bilipschitz_time_one_exists line 58

Source documentation

Both Lipschitz bounds refer to the actual map generated by the ODE.

theorem moser_bilipschitz_time_one_exists {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),
      (∀ x, G x 0 = x) ∧
      (∀ x, ∀ t ∈ Set.Icc (0 : ℝ) 1,
        HasDerivWithinAt (G x) (moserVelocity rho V t (G x t)) (Set.Icc (0 : ℝ) 1) t) ∧
      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) := by
…

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

theorem OAI.ContinuumCoulomb.moser_time_one_preserves_slab line 77