OAI/Analysis/CoulombTransport/CoulombEstimates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.CoulombEstimates.abs_inv_sub_inv_le line 15

   Source documentation

   The reciprocal is uniformly Lipschitz away from zero.

   theorem abs_inv_sub_inv_le {a b eta L : ℝ}
       (heta : 0 < eta) (ha : eta ≤ a) (hb : eta ≤ b)
       (hL : |a - b| ≤ L) :
       |a⁻¹ - b⁻¹| ≤ L / eta ^ 2 := by
   …

2. theorem OAI.Problem356.CoulombEstimates.abs_dist_sub_dist_le line 31

   Source documentation

   Moving both endpoints by at most delta changes distance by at most 2 * delta.

   theorem abs_dist_sub_dist_le {E : Type uE} [PseudoMetricSpace E]
       {x y x' y' : E} {delta : ℝ}
       (hx : dist x x' ≤ delta) (hy : dist y y' ≤ delta) :
       |dist x y - dist x' y'| ≤ 2 * delta := by
   …

3. theorem OAI.Problem356.CoulombEstimates.abs_inv_dist_sub_inv_dist_le line 47

   Source documentation

   Coulomb pair interaction has a quantitative oscillation estimate on separated products.

   theorem abs_inv_dist_sub_inv_dist_le {E : Type uE} [PseudoMetricSpace E]
       {x y x' y' : E} {eta delta : ℝ}
       (heta : 0 < eta) (hxy : eta ≤ dist x y) (hxy' : eta ≤ dist x' y')
       (hx : dist x x' ≤ delta) (hy : dist y y' ≤ delta) :
       |(dist x y)⁻¹ - (dist x' y')⁻¹| ≤ (2 * delta) / eta ^ 2 :=
   …

4. def OAI.Problem356.CoulombEstimates.realCost line 55

   Source documentation

   Real-valued three-particle Coulomb cost on an arbitrary metric space.

   def realCost {E : Type uE} [PseudoMetricSpace E] (x y z : E) : ℝ :=
   …

5. theorem OAI.Problem356.CoulombEstimates.realCost_le line 59

   Source documentation

   Uniform boundedness of the Coulomb cost on a separated triple.

   theorem realCost_le {E : Type uE} [PseudoMetricSpace E]
       {x y z : E} {eta : ℝ} (heta : 0 < eta)
       (hxy : eta ≤ dist x y) (hxz : eta ≤ dist x z) (hyz : eta ≤ dist y z) :
       realCost x y z ≤ 3 / eta := by
   …

   Mentions: OAI.Problem356.CoulombEstimates.realCost

6. theorem OAI.Problem356.CoulombEstimates.abs_realCost_sub_realCost_le line 72

   Source documentation

   Oscillation of the three-particle Coulomb cost on separated, small cells.

   theorem abs_realCost_sub_realCost_le {E : Type uE} [PseudoMetricSpace E]
       {x y z x' y' z' : E} {eta delta : ℝ}
       (heta : 0 < eta)
       (hxy : eta ≤ dist x y) (hxz : eta ≤ dist x z) (hyz : eta ≤ dist y z)
       (hxy' : eta ≤ dist x' y') (hxz' : eta ≤ dist x' z') (hyz' : eta ≤ dist y' z')
       (hx : dist x x' ≤ delta) (hy : dist y y' ≤ delta) (hz : dist z z' ≤ delta) :
       |realCost x y z - realCost x' y' z'| ≤ (6 * delta) / eta ^ 2 := by
   …

   Mentions: OAI.Problem356.CoulombEstimates.realCost

7. theorem OAI.Problem356.CoulombEstimates.coulombCost_eq_ofReal_realCost line 99

   Source documentation

   The real formula agrees with the extended-valued cost away from collisions.

   theorem coulombCost_eq_ofReal_realCost {x y z : E3}
       (hxy : 0 < dist x y) (hxz : 0 < dist x z) (hyz : 0 < dist y z) :
       coulombCost (x, (y, z)) = ENNReal.ofReal (realCost x y z) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost, OAI.Problem356.CoulombEstimates.realCost

8. theorem OAI.Problem356.CoulombEstimates.coulombCost_le_of_separated line 111

   Source documentation

   The exact extended-valued Coulomb cost is uniformly bounded on separated triples.

   theorem coulombCost_le_of_separated {x y z : E3} {eta : ℝ}
       (heta : 0 < eta)
       (hxy : eta ≤ dist x y) (hxz : eta ≤ dist x z) (hyz : eta ≤ dist y z) :
       coulombCost (x, (y, z)) ≤ ENNReal.ofReal (3 / eta) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost

9. theorem OAI.Problem356.CoulombEstimates.coulombCost_lt_top_of_separated line 120

   Source documentation

   Separated triples have finite Coulomb cost.

   theorem coulombCost_lt_top_of_separated {x y z : E3} {eta : ℝ}
       (heta : 0 < eta)
       (hxy : eta ≤ dist x y) (hxz : eta ≤ dist x z) (hyz : eta ≤ dist y z) :
       coulombCost (x, (y, z)) < ⊤ :=
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost

10. theorem OAI.Problem356.CoulombEstimates.coulombCost_le_add_of_separated line 127

    Source documentation

    One-sided extended-valued oscillation bound, suitable for lower integrals.

    theorem coulombCost_le_add_of_separated {x y z x' y' z' : E3} {eta delta : ℝ}
        (heta : 0 < eta)
        (hxy : eta ≤ dist x y) (hxz : eta ≤ dist x z) (hyz : eta ≤ dist y z)
        (hxy' : eta ≤ dist x' y') (hxz' : eta ≤ dist x' z') (hyz' : eta ≤ dist y' z')
        (hx : dist x x' ≤ delta) (hy : dist y y' ≤ delta) (hz : dist z z' ≤ delta) :
        coulombCost (x, (y, z)) ≤ coulombCost (x', (y', z')) +
          ENNReal.ofReal ((6 * delta) / eta ^ 2) := by
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost

11. def OAI.Problem356.CoulombEstimates.Separated line 149

    Source documentation

    Pairwise separation of the coordinates of a triple.

    def Separated (eta : ℝ) (t : Triple) : Prop :=
    …

    Mentions: OAI.Problem356.Triple

12. theorem OAI.Problem356.CoulombEstimates.lintegral_coulombCost_le_of_ae_separated line 153

    Source documentation

    A lower-integral bound requiring only almost-everywhere separation.

    theorem lintegral_coulombCost_le_of_ae_separated (mu : Measure Triple) {eta : ℝ}
        (heta : 0 < eta) (hsep : ∀ᵐ t ∂mu, Separated eta t) :
        (∫⁻ t, coulombCost t ∂mu) ≤ ENNReal.ofReal (3 / eta) * mu Set.univ := by
    …

    Mentions: OAI.Problem356.Triple, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.coulombCost

13. theorem OAI.Problem356.CoulombEstimates.lintegral_coulombCost_lt_top_of_ae_separated line 165

    Source documentation

    On finite measures, almost-everywhere separation guarantees finite cost.

    theorem lintegral_coulombCost_lt_top_of_ae_separated (mu : Measure Triple)
        [IsFiniteMeasure mu] {eta : ℝ}
        (heta : 0 < eta) (hsep : ∀ᵐ t ∂mu, Separated eta t) :
        (∫⁻ t, coulombCost t ∂mu) < ⊤ :=
    …

    Mentions: OAI.Problem356.Triple, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.coulombCost

14. theorem OAI.Problem356.CoulombEstimates.graphCost_le_of_ae_separated line 173

    Source documentation

    A uniform graph-cost bound; no regularity of the maps is needed for this bound.

    theorem graphCost_le_of_ae_separated (mu : Measure E3) {T2 T3 : E3 → E3} {eta : ℝ}
        (heta : 0 < eta) (hsep : ∀ᵐ x ∂mu, Separated eta (x, (T2 x, T3 x))) :
        graphCost mu T2 T3 ≤ ENNReal.ofReal (3 / eta) * mu Set.univ := by
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.graphCost

15. theorem OAI.Problem356.CoulombEstimates.graphCost_lt_top_of_ae_separated line 185

    Source documentation

    The finite-cost condition in finite Monge approximation follows from separation.

    theorem graphCost_lt_top_of_ae_separated (mu : Measure E3) [IsFiniteMeasure mu]
        {T2 T3 : E3 → E3} {eta : ℝ}
        (heta : 0 < eta) (hsep : ∀ᵐ x ∂mu, Separated eta (x, (T2 x, T3 x))) :
        graphCost mu T2 T3 < ⊤ :=
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.graphCost

16. theorem OAI.Problem356.CoulombEstimates.lintegral_coulombCost_le_add_of_ae_close line 193

    Source documentation

    Integrating the pointwise oscillation bound under a common parametrization.

    theorem lintegral_coulombCost_le_add_of_ae_close
        {A : Type uA} [MeasurableSpace A] (mu : Measure A) {P Q : A → Triple} {eta delta : ℝ}
        (heta : 0 < eta)
        (hsepP : ∀ᵐ a ∂mu, Separated eta (P a))
        (hsepQ : ∀ᵐ a ∂mu, Separated eta (Q a))
        (hclose : ∀ᵐ a ∂mu, dist (P a).1 (Q a).1 ≤ delta ∧
          dist (P a).2.1 (Q a).2.1 ≤ delta ∧ dist (P a).2.2 (Q a).2.2 ≤ delta) :
        (∫⁻ a, coulombCost (P a) ∂mu) ≤ (∫⁻ a, coulombCost (Q a) ∂mu) +
          ENNReal.ofReal ((6 * delta) / eta ^ 2) * mu Set.univ := by
    …

    Mentions: OAI.Problem356.Triple, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.coulombCost