MoserUniformVelocity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The Moser velocity and flow have a common derivative bound over all potentials with a common order-six bound.

theorem OAI.ContinuumCoulomb.product_four_bound line 14
theorem OAI.ContinuumCoulomb.partial_C4 line 41
theorem OAI.ContinuumCoulomb.partial_joint_bound line 45

theorem OAI.ContinuumCoulomb.moserVelocity_family_derivative_bound line 60

Source documentation

One bound controls all joint velocity derivatives through order four for the entire bounded family of potentials.

theorem moserVelocity_family_derivative_bound {rho B : ℝ} (hrho : 0 < rho) (hB : 0 ≤ B) :
    ∃ C : ℝ, 0 < C ∧ ∀ (V : Position → ℝ), ContDiff ℝ 6 V →
      (∀ k ≤ 6, ∀ x, ‖iteratedFDeriv ℝ k V x‖ ≤ B) →
      (∀ x, |manufacturedCharge V x| ≤ rho/2) →
      ∀ k ≤ 4, ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ x,
        ‖iteratedFDeriv ℝ k (fun p : ℝ × Position => moserVelocity rho V p.1 p.2) (t,x)‖ ≤ C := by
…

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

theorem OAI.ContinuumCoulomb.moserFlow_family_derivative_bound line 131

Source documentation

The variational estimate has a constant fixed before the potential is chosen.

theorem moserFlow_family_derivative_bound (hpublished : PublishedC4FlowInput)
    {rho B : ℝ} (hrho : 0 < rho) (hB : 0 ≤ B) :
    ∃ C : ℝ, 0 < C ∧ ∀ (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 →
      ∀ k : ℕ, 1 ≤ k → k ≤ 4 → ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ x,
        ‖iteratedFDeriv ℝ k (fun y => G y t) x‖ ≤ C := by
…

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