MoserFlow.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual integral curves of the manufactured-density field exist through time one. The flow is stationary outside the well support. No transport map or ODE solution is introduced as an assumed analytic input.

theorem OAI.ContinuumCoulomb.moser_trajectory_exists line 14

theorem OAI.ContinuumCoulomb.moser_trajectory_unique line 34

Source documentation

Uniqueness is on the closed transport interval, including both endpoints.

theorem moser_trajectory_unique {rho : ℝ} (hrho : 0 < rho)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V) (hc : HasCompactSupport V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2)
    {α β : ℝ → Position}
    (hα : ∀ t ∈ Set.Icc (0 : ℝ) 1,
      HasDerivWithinAt α (moserVelocity rho V t (α t)) (Set.Icc (0 : ℝ) 1) t)
    (hβ : ∀ t ∈ Set.Icc (0 : ℝ) 1,
      HasDerivWithinAt β (moserVelocity rho V t (β t)) (Set.Icc (0 : ℝ) 1) t)
    (hzero : α 0 = β 0) : Set.EqOn α β (Set.Icc (0 : ℝ) 1) := by
…

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

theorem OAI.ContinuumCoulomb.moser_flow_exists line 59

Source documentation

A single family of actual trajectories, stationary outside the well, with a uniform Lipschitz bound in time.

theorem moser_flow_exists {rho : ℝ} (hrho : 0 < rho)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V) (hc : HasCompactSupport V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2) :
    ∃ (G : Position → ℝ → Position) (L : ℝ≥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) ∧
      (∀ x, LipschitzOnWith L (G x) (Set.Icc (0 : ℝ) 1)) ∧
      (∀ x, x ∉ tsupport V → ∀ t ∈ Set.Icc (0 : ℝ) 1, G x t = x) := by
…

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