OAI/Analysis/CoulombTransport/LocalPotentialBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.exists_uniform_local_potential_bound line 14

   Source documentation

   Continuity of finitely many potentials at their centers gives one positive radius and one positive absolute bound on every component ball.

   theorem exists_uniform_local_potential_bound {ι : Type uIndex} {X : Type uX} [Fintype ι]
       [PseudoMetricSpace X] (p : ι → X) (v : ι → X → ℝ)
       (hv : ∀ i, ContinuousAt (v i) (p i)) :
       ∃ M : ℝ, 0 < M ∧ ∃ r : ℝ, 0 < r ∧
         ∀ i x, x ∈ ball (p i) r → |v i x| ≤ M := by
   …