PairEnergyFinite.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.integrableOn_inv_norm_ball line 12
theorem OAI.Problem356.lintegral_invDistance_zero_ball_lt_top line 21
Source documentation
The Coulomb singularity is integrable on every bounded ball in dimension three.
```
theorem lintegral_invDistance_zero_ball_lt_top (r : ℝ) :
    (∫⁻ x in Metric.ball (0 : E3) r, invDistance 0 x ∂volume) < ⊤ := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.invDistance
def OAI.Problem356.localCoulombKernel line 32
Source documentation
Local part of the singular kernel; the omitted tail is bounded by one.
```
def localCoulombKernel (x : E3) : ℝ≥0∞ :=
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.measurable_localCoulombKernel line 35
theorem OAI.Problem356.lintegral_localCoulombKernel_lt_top line 41
theorem OAI.Problem356.densityMeasure_le_smul_volume_of_le line 46
theorem OAI.Problem356.invDistance_le_localCoulombKernel_add_one line 53

theorem OAI.Problem356.lintegral_invDistance_le_of_measure_le line 64

Source documentation

Uniform control of the Coulomb potential for a probability with bounded density.

theorem lintegral_invDistance_le_of_measure_le (mu : Measure E3)
    [IsProbabilityMeasure mu] {C : ℝ≥0∞}
    (hmu : mu ≤ C • (volume : Measure E3)) (x : E3) :
    (∫⁻ y, invDistance x y ∂mu) ≤
      C * (∫⁻ y : E3, localCoulombKernel y ∂volume) + 1 := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.invDistance, OAI.Problem356.localCoulombKernel

theorem OAI.Problem356.coulombPairEnergy_lt_top_of_measure_le line 83
theorem OAI.Problem356.coulombPairEnergy_densityMeasure_lt_top_of_bounded line 97
theorem OAI.Problem356.coulombPairEnergy_densityMeasure_lt_top line 103
theorem OAI.Problem356.kantorovichValue_densityMeasure_lt_top line 112