Generic potential estimates from uniform local Coulomb control

The extended Coulomb kernel is measurable as a function of its second argument.

Outside the unit ball the kernel is at most one.

theorem LiebThirring.measurable_coulombKernel_right (x : Position) : Measurable (coulombKernel x)

The extended Coulomb kernel is measurable as a function of its second argument.

theorem LiebThirring.coulombKernel_le_one_of_not_mem_ball (x y : Position) (hy : y ∉ Metric.ball x 1) : coulombKernel x y ≤ 1

Outside the unit ball the kernel is at most one.

theorem LiebThirring.coulombPotential_le_of_local_bound (μ : MeasureTheory.Measure Position) (C : ℝ) (hlocal : ∀ (x : Position) (ε : ℝ), 0 < ε → ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂μ ≤ ENNReal.ofReal (C * ε)) (x : Position) : coulombPotential μ x ≤ ENNReal.ofReal C + μ Set.univ

Uniform local control at radius one gives a global bound.

theorem LiebThirring.coulombPotential_lt_top_of_local_bound (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (C : ℝ) (hlocal : ∀ (x : Position) (ε : ℝ), 0 < ε → ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂μ ≤ ENNReal.ofReal (C * ε)) (x : Position) : coulombPotential μ x < ⊤

A finite measure with uniform local control has an everywhere finite potential.

theorem LiebThirring.coulombEnergy_lt_top_of_local_bound (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (C : ℝ) (hlocal : ∀ (x : Position) (ε : ℝ), 0 < ε → ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂μ ≤ ENNReal.ofReal (C * ε)) : coulombEnergy μ μ < ⊤

The self-energy is finite under the same uniform local estimate.

noncomputable def LiebThirring.cappedCoulombKernel (r : ℝ) (x y : Position) : ENNReal

Continuous capped Coulomb kernel, with a positive cap radius.

Equations

• LiebThirring.cappedCoulombKernel r x y = (ENNReal.ofReal (max r ‖x - y‖))⁻¹

noncomputable def LiebThirring.cappedCoulombPotential (μ : MeasureTheory.Measure Position) (r : ℝ) (x : Position) : ENNReal

Potential of the capped kernel.

Equations

• LiebThirring.cappedCoulombPotential μ r x = ∫⁻ (y : LiebThirring.Position), LiebThirring.cappedCoulombKernel r x y ∂μ

theorem LiebThirring.continuous_cappedCoulombKernel_left (r : ℝ) (y : Position) : Continuous fun (x : Position) => cappedCoulombKernel r x y

theorem LiebThirring.measurable_cappedCoulombKernel_right (r : ℝ) (x : Position) : Measurable (cappedCoulombKernel r x)

theorem LiebThirring.cappedCoulombKernel_le (r : ℝ) (x y : Position) : cappedCoulombKernel r x y ≤ coulombKernel x y

theorem LiebThirring.cappedCoulombKernel_le_cap (r : ℝ) (x y : Position) : cappedCoulombKernel r x y ≤ (ENNReal.ofReal r)⁻¹

theorem LiebThirring.cappedCoulombPotential_le (μ : MeasureTheory.Measure Position) (r : ℝ) (x : Position) : cappedCoulombPotential μ r x ≤ coulombPotential μ x

theorem LiebThirring.continuous_cappedCoulombPotential (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (r : ℝ) (hr : 0 < r) : Continuous (cappedCoulombPotential μ r)

A positive cap radius gives a continuous potential for every finite measure.

theorem LiebThirring.cappedCoulombPotential_lt_top (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (r : ℝ) (hr : 0 < r) (x : Position) : cappedCoulombPotential μ r x < ⊤

theorem LiebThirring.coulombPotential_le_capped_add_of_local_bound (μ : MeasureTheory.Measure Position) (C r : ℝ) (hr : 0 < r) (hlocal : ∀ (x : Position) (ε : ℝ), 0 < ε → ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂μ ≤ ENNReal.ofReal (C * ε)) (x : Position) : coulombPotential μ x ≤ cappedCoulombPotential μ r x + ENNReal.ofReal (C * r)

The potential differs from its capped approximation only in the local ball.

theorem LiebThirring.continuous_toReal_cappedCoulombPotential (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (r : ℝ) (hr : 0 < r) : Continuous fun (x : Position) => (cappedCoulombPotential μ r x).toReal

The real-valued capped potential is continuous.

theorem LiebThirring.dist_toReal_coulombPotential_capped_le (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (C r : ℝ) (hC : 0 ≤ C) (hr : 0 < r) (hlocal : ∀ (x : Position) (ε : ℝ), 0 < ε → ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂μ ≤ ENNReal.ofReal (C * ε)) (x : Position) : dist (coulombPotential μ x).toReal (cappedCoulombPotential μ r x).toReal ≤ C * r

Quantitative uniform approximation in the finite real-valued potential.

theorem LiebThirring.continuous_toReal_coulombPotential_of_local_bound (μ : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure μ] (C : ℝ) (hC : 0 ≤ C) (hlocal : ∀ (x : Position) (ε : ℝ), 0 < ε → ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂μ ≤ ENNReal.ofReal (C * ε)) : Continuous fun (x : Position) => (coulombPotential μ x).toReal

Uniform local control gives continuity of the finite real-valued potential.