MoserEndpoint.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual time-one map is a bijection of physical space. This follows from forward uniqueness and trajectories with terminal data, rather than from assuming that the continuity equation already produces a diffeomorphism.

theorem OAI.ContinuumCoulomb.moser_trajectory_unique_terminal line 13

theorem OAI.ContinuumCoulomb.moser_trajectory_spatial_bound line 37

Source documentation

The usual exponential spatial-dependence bound for these actual curves.

theorem moser_trajectory_spatial_bound {rho : ℝ} (hrho : 0 < rho)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V) (hc : HasCompactSupport V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2) :
    ∃ K : ℝ≥0, ∀ (α β : ℝ → Position),
      (∀ t ∈ Set.Icc (0 : ℝ) 1,
        HasDerivWithinAt α (moserVelocity rho V t (α t)) (Set.Icc (0 : ℝ) 1) t) →
      (∀ t ∈ Set.Icc (0 : ℝ) 1,
        HasDerivWithinAt β (moserVelocity rho V t (β t)) (Set.Icc (0 : ℝ) 1) t) →
      ∀ t ∈ Set.Icc (0 : ℝ) 1,
        dist (α t) (β t) ≤ dist (α 0) (β 0) * Real.exp ((K : ℝ) * t) := by
…

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

theorem OAI.ContinuumCoulomb.moser_time_one_exists line 66

Source documentation

The generated time-one map is globally Lipschitz, bijective, and fixes the complement of the compact well support.

theorem moser_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,
      (∀ 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) ∧
      (∃ C : ℝ≥0, LipschitzWith C (fun x => G x 1)) ∧
      (∀ x, x ∉ tsupport V → G x 1 = x) := by
…

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