Lᵖ seminorms on all balls of one radius

For an additive Haar measure μ on a proper normed additive group, the balls B(y, r) of a fixed radius cover every point equally often when y runs over the whole space: by Tonelli's theorem,

∫⁻ y, ∫⁻ x in B(y, r), G x ∂μ ∂μ = μ (B(0, r)) * ∫⁻ x, G x ∂μ.

Applied to G = ‖g‖ₑ ^ p, the p-th powers of the Lᵖ seminorms of g on the balls of radius r integrate to μ (B(0, r)) times the p-th power of its Lᵖ seminorm. Consequently a local estimate ‖g‖_{Lᵖ(B(y, r))} ≤ ‖h‖_{Lᵖ(B(y, R))} holding at (almost) every centre y becomes the global estimate

‖g‖_{Lᵖ} ≤ (μ (B(0, R)) / μ (B(0, r))) ^ (1 / p) ‖h‖_{Lᵖ}.

On a finite-dimensional real normed space of dimension d the volume ratio for R = 2 r is 2 ^ d. In this setting, local estimates of the form ‖g‖_{Lᵖ(B(y, r))} ≤ c₁ ‖f₁‖_{Lᵖ(B(y, 2r))} + c₂ ‖f₂‖_{Lᵖ(B(y, 2r))} at almost every centre give ‖g‖_{Lᵖ} ≤ 2 ^ (d + 1) (c₁ ‖f₁‖_{Lᵖ} + c₂ ‖f₂‖_{Lᵖ}), with a constant independent of r.

This is how interior estimates on balls with constants independent of the centre, such as the Calderón–Zygmund estimates for elliptic equations, pass to estimates on the whole space. It replaces a covering of the space by balls with bounded overlap: averaging over all centres is an exact form of the bounded-overlap count.

Main declarations

• TauCeti.lintegral_setLIntegral_ball: the Tonelli identity above.
• TauCeti.lintegral_eLpNorm_restrict_ball_rpow: its form for Lᵖ seminorms.
• TauCeti.eLpNorm_le_of_ae_eLpNorm_restrict_ball_le: local estimates on balls of one radius give a global estimate.
• TauCeti.lpNorm_le_of_ae_lpNorm_restrict_ball_le_add: the same for local estimates by two functions on concentric balls of radii r and 2 r, with the explicit constant 2 ^ (d + 1).

theorem TauCeti.lintegral_setLIntegral_ball {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {G : E → ENNReal} (hG : AEMeasurable G μ) (r : ℝ) : ∫⁻ (y : E), ∫⁻ (x : E) in Metric.ball y r, G x ∂μ ∂μ = μ (Metric.ball 0 r) * ∫⁻ (x : E), G x ∂μ

Integrating the integrals of G over the balls B(y, r) against μ (dy) gives μ (B(0, r)) times the integral of G: every point lies in the balls whose centres form a ball of the same radius around it.

theorem TauCeti.lintegral_eLpNorm_restrict_ball_rpow {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {g : E → F} (hg : MeasureTheory.AEStronglyMeasurable g μ) (r : ℝ) : ∫⁻ (y : E), MeasureTheory.eLpNorm g p (μ.restrict (Metric.ball y r)) ^ p.toReal ∂μ = μ (Metric.ball 0 r) * MeasureTheory.eLpNorm g p μ ^ p.toReal

The p-th powers of the Lᵖ seminorms of g on the balls B(y, r) integrate, against μ (dy), to μ (B(0, r)) times the p-th power of the Lᵖ seminorm of g.

theorem TauCeti.eLpNorm_le_of_ae_eLpNorm_restrict_ball_le {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {G : Type u_3} [NormedAddCommGroup G] {g : E → F} {h : E → G} (hg : MeasureTheory.AEStronglyMeasurable g μ) (hh : MeasureTheory.AEStronglyMeasurable h μ) {r R : ℝ} (hr : 0 < r) (hle : ∀ᵐ (y : E) ∂μ, MeasureTheory.eLpNorm g p (μ.restrict (Metric.ball y r)) ≤ MeasureTheory.eLpNorm h p (μ.restrict (Metric.ball y R))) : MeasureTheory.eLpNorm g p μ ≤ (μ (Metric.ball 0 R) / μ (Metric.ball 0 r)) ^ p.toReal⁻¹ * MeasureTheory.eLpNorm h p μ

Global estimates from local ones on balls of one radius. If 0 < r and, for almost every centre y, the Lᵖ seminorm of g on B(y, r) is at most that of h on B(y, R), then

‖g‖_{Lᵖ} ≤ (μ (B(0, R)) / μ (B(0, r))) ^ (1 / p) ‖h‖_{Lᵖ}.

theorem TauCeti.lpNorm_le_of_ae_lpNorm_restrict_ball_le_add {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] {p : ENNReal} [NormedSpace ℝ E] [FiniteDimensional ℝ E] {G₁ : Type u_3} {G₂ : Type u_4} [NormedAddCommGroup G₁] [NormedAddCommGroup G₂] (hp1 : 1 ≤ p) (hp : p ≠ ⊤) {g : E → F} {f₁ : E → G₁} {f₂ : E → G₂} (hg : MeasureTheory.MemLp g p μ) (hf₁ : MeasureTheory.MemLp f₁ p μ) (hf₂ : MeasureTheory.MemLp f₂ p μ) {c₁ c₂ r : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hr : 0 < r) (hle : ∀ᵐ (y : E) ∂μ, MeasureTheory.lpNorm g p (μ.restrict (Metric.ball y r)) ≤ c₁ * MeasureTheory.lpNorm f₁ p (μ.restrict (Metric.ball y (2 * r))) + c₂ * MeasureTheory.lpNorm f₂ p (μ.restrict (Metric.ball y (2 * r)))) : MeasureTheory.lpNorm g p μ ≤ 2 ^ (Module.finrank ℝ E + 1) * (c₁ * MeasureTheory.lpNorm f₁ p μ + c₂ * MeasureTheory.lpNorm f₂ p μ)

Global estimates from local ones on concentric balls. Let μ be an additive Haar measure on a finite-dimensional real normed space E, let 1 ≤ p < ∞, and let g, f₁, f₂ be in Lᵖ(μ). If 0 < r, 0 ≤ c₁, 0 ≤ c₂ and, at almost every centre y,

‖g‖_{Lᵖ(B(y, r))} ≤ c₁ ‖f₁‖_{Lᵖ(B(y, 2r))} + c₂ ‖f₂‖_{Lᵖ(B(y, 2r))},

then ‖g‖_{Lᵖ} ≤ 2 ^ (dim E + 1) (c₁ ‖f₁‖_{Lᵖ} + c₂ ‖f₂‖_{Lᵖ}). The constant does not depend on r.