MoserUniformInverse.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform separation of transported nodes: the inverse Lipschitz constant is fixed over the same bounded family as the forward flow.

theorem OAI.ContinuumCoulomb.velocity_lipschitz_of_joint_bound line 12
theorem OAI.ContinuumCoulomb.trajectory_backward_of_lipschitz line 37

theorem OAI.ContinuumCoulomb.moserFlow_family_inverse_bound line 79

Source documentation

One inverse Lipschitz constant works for every actual trajectory family of every potential with the stated six-derivative bound.

theorem moserFlow_family_inverse_bound {rho B : ℝ} (hrho : 0 < rho) (hB : 0 ≤ B) :
    ∃ K : ℝ≥0, 0 < K ∧ ∀ (V : Position → ℝ), ContDiff ℝ 6 V →
      (∀ k ≤ 6, ∀ x, ‖iteratedFDeriv ℝ k V x‖ ≤ B) →
      (∀ x, |manufacturedCharge V x| ≤ rho/2) →
      ∀ G : Position → ℝ → Position, IsUnitTimeFlow (moserVelocity rho V) G →
        AntilipschitzWith K (fun x => G x 1) := by
…

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