Decay of Coulomb potentials of planar densities

Away from a radius r > 0, the Coulomb kernel is bounded by 1/r.

The far Coulomb contribution of any positive measure is controlled by its mass.

theorem LiebThirring.coulombKernel_le_of_le_norm_sub (x y : Position) {r : ℝ} (hr : 0 < r) (hxy : r ≤ ‖x - y‖) : coulombKernel x y ≤ ENNReal.ofReal (1 / r)

Away from a radius r > 0, the Coulomb kernel is bounded by 1/r.

theorem LiebThirring.lintegral_coulombKernel_compl_ball_le (μ : MeasureTheory.Measure Position) (x : Position) {r : ℝ} (hr : 0 < r) : ∫⁻ (y : Position) in (Metric.ball x r)ᶜ, coulombKernel x y ∂μ ≤ ENNReal.ofReal (1 / r) * μ Set.univ

The far Coulomb contribution of any positive measure is controlled by its mass.

theorem LiebThirring.lintegral_coulombKernel_ball_withDensity_le (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (f : Position → ENNReal) (hf : Measurable f) (B : ℝ) {r : ℝ} (hr : 0 < r) (hfB : ∀ᵐ (y : Position) ∂(planeMeasure F).restrict (Metric.ball x r), f y ≤ ENNReal.ofReal B) : ∫⁻ (y : Position) in Metric.ball x r, coulombKernel x y ∂(planeMeasure F).withDensity f ≤ ENNReal.ofReal B * ENNReal.ofReal (2 * Real.pi * r)

planar integration controls any planar density bounded on the indicated ball.

theorem LiebThirring.coulombPotential_withDensity_planeMeasure_le (n b : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (f : Position → ENNReal) (hf : Measurable f) (B m : ℝ) (hB : 0 ≤ B) (hm : 0 ≤ m) (hfB : ∀ᵐ (y : Position) ∂planeMeasure F, f y ≤ ENNReal.ofReal B) (hmass : ((planeMeasure F).withDensity f) Set.univ ≤ ENNReal.ofReal m) (x : Position) : coulombPotential ((planeMeasure F).withDensity f) x ≤ ENNReal.ofReal (2 * Real.pi * B + m)

Uniform potential bound for a bounded planar density of bounded mass.

theorem LiebThirring.cubic_decay_le_half_radius (A R t : ℝ) (hA : 0 ≤ A) (hR : 0 < R) (ht : 0 ≤ t) (hRt : R / 2 ≤ t) : A / (1 + t) ^ 3 ≤ 8 * A / R ^ 3

Scalar cubic decay bound outside half the observation radius.

theorem LiebThirring.half_norm_le_of_mem_ball (x y : Position) (hy : y ∈ Metric.ball x (‖x‖ / 2)) : ‖x‖ / 2 ≤ ‖y‖

Points in the observation ball of half-radius lie outside half the origin-radius.

theorem LiebThirring.coulombPotential_withDensity_planeMeasure_le_of_norm_pos (n b : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (f : Position → ENNReal) (hf : Measurable f) (A m : ℝ) (hA : 0 ≤ A) (hm : 0 ≤ m) (hfA : ∀ᵐ (y : Position) ∂planeMeasure F, f y ≤ ENNReal.ofReal (A / (1 + ‖y‖) ^ 3)) (hmass : ((planeMeasure F).withDensity f) Set.univ ≤ ENNReal.ofReal m) (x : Position) (hx : 0 < ‖x‖) : coulombPotential ((planeMeasure F).withDensity f) x ≤ ENNReal.ofReal (2 * m / ‖x‖ + 8 * Real.pi * A / ‖x‖ ^ 2)

Large-radius potential estimate from cubic density decay and bounded mass.

theorem LiebThirring.coulomb_decay_majorant_le (A m R : ℝ) (hA : 0 ≤ A) (hR : 1 ≤ R) : 2 * m / R + 8 * Real.pi * A / R ^ 2 ≤ (2 * m + 8 * Real.pi * A) / R

For radii at least one the quadratic tail is absorbed into the linear tail.

theorem LiebThirring.coulombPotential_withDensity_planeMeasure_decay (n b : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (f : Position → ENNReal) (hf : Measurable f) (A B m : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hm : 0 ≤ m) (hfB : ∀ᵐ (y : Position) ∂planeMeasure F, f y ≤ ENNReal.ofReal B) (hfA : ∀ᵐ (y : Position) ∂planeMeasure F, f y ≤ ENNReal.ofReal (A / (1 + ‖y‖) ^ 3)) (hmass : ((planeMeasure F).withDensity f) Set.univ ≤ ENNReal.ofReal m) (x : Position) : coulombPotential ((planeMeasure F).withDensity f) x ≤ ENNReal.ofReal ((4 * Real.pi * B + 6 * m + 16 * Real.pi * A) / (1 + ‖x‖))

The explicit uniform decay bound for a bounded, cubically decaying planar density.

theorem LiebThirring.tendsto_coulombPotential_zero_of_decay (μ : MeasureTheory.Measure Position) (C : ℝ) (hdecay : ∀ (x : Position), coulombPotential μ x ≤ ENNReal.ofReal (C / (1 + ‖x‖))) : Filter.Tendsto (coulombPotential μ) (Bornology.cobounded Position) (nhds 0)

A pointwise inverse-radius potential bound implies decay at spatial infinity.