The ball average of an Lᵖ function

The ball average of f at scale r is

A_r f x = ⨍ y in Metric.ball x r, f y ∂μ,

the mean of f over the ball of radius r centred at x. It is the mollification of f by the normalized indicator of a ball, and it is the smoothing operator behind the Fréchet--Kolmogorov compactness criterion in Lᵖ, hence behind Rellich--Kondrachov, Lane A.6 of TauCetiRoadmap/PDE/README.md.

Four estimates are proved here, all for 1 ≤ p < ∞ and an additive Haar measure μ on a proper normed additive group. Writing V = μ (Metric.ball 0 r) for the volume of the ball, they are

‖A_r f x‖ ≤ V ^ (-1/p) ‖f‖_p, ‖A_r f (x + e) - A_r f x‖ ≤ V ^ (-1/p) ‖f(· + e) - f‖_p, ‖A_r f‖_p ≤ ‖f‖_p, ‖A_r f - f‖_p ≤ C whenever ‖f(· + e) - f‖_p ≤ C for every e in the ball of radius r.

For each fixed positive r, these estimates send a family with uniformly small Lᵖ translation increments to a uniformly bounded and uniformly equicontinuous family of ball averages. The equicontinuity bound includes the scale-dependent factor V ^ (-1/p); its remaining modulus is the original family's uniform Lᵖ translation modulus. This is exactly the trade-off that the Fréchet--Kolmogorov criterion exploits: a family of functions whose translates move little in Lᵖ is uniformly close to a family of uniformly equicontinuous ones.

The first two estimates come from a single Hölder bound, TauCeti.enorm_setAverage_le: the average of g over a set s of finite positive measure is at most μ s ^ (-1/p) ‖g‖_p. For the first, apply it to g = f; for the second, apply it to g = f(· + e) - f, using that the ball average commutes with translation.

The last two are Hölder again, now in the translation variable, followed by Tonelli's theorem; they share the analytic core lintegral_enorm_setAverage_rpow_le. For the contraction, apply it to G x e = f (x + e) and use translation invariance on each slice. For the approximation estimate, write the deviation as an average,

A_r f x - f x = ⨍ e in Metric.ball 0 r, (f (x + e) - f x) ∂μ,

so that its p-th power is bounded by V⁻¹ ∫⁻ e in Metric.ball 0 r, ‖f (x + e) - f x‖ₑ ^ p ∂μ. Integrating in x and exchanging the two integrations, the inner integral becomes ‖f(· + e) - f‖_p ^ p, uniformly at most C ^ p, and the factor V⁻¹ cancels against the measure of the ball the translation ranges over.

Both the definition and the estimates are stated for a Banach-space-valued f. The domain is assumed proper, which is what makes balls have finite measure; finite-dimensional real normed spaces are an important special case.

The averages appearing here are the ones the Hardy--Littlewood maximal function TauCeti.maximalFunction takes a supremum of, so ‖A_r f x‖ ≤ M f x for every r > 0. The two are put to opposite uses: the maximal function discards r to get a pointwise majorant of f, while A_r f keeps r as a smoothing scale and is compared with f itself. Nothing below needs the maximal inequality, so the two developments are kept apart.

Main declarations

• TauCeti.ballAverage: the ball average, with TauCeti.ballAverage_congr_ae and TauCeti.ballAverage_eq_setAverage_ball_zero as its basic interface.
• TauCeti.ballAverage_const: the ball average of a constant is that constant, so the normalization is the intended one.
• TauCeti.enorm_setAverage_rpow_le, TauCeti.enorm_setAverage_le: Hölder's bound on an average over a set, in ∫⁻ and in Lᵖ form.
• TauCeti.enorm_ballAverage_le: the L^∞ bound on A_r f.
• TauCeti.eLpNorm_ballAverage_le: A_r is an Lᵖ contraction.
• TauCeti.ballAverage_comp_add, TauCeti.ballAverage_sub_ballAverage: the ball average commutes with translation, and its increment is the ball average of the increment.
• TauCeti.enorm_ballAverage_add_sub_ballAverage_le: the equicontinuity estimate, with modulus the Lᵖ modulus of continuity of f itself.
• TauCeti.uniformEquicontinuous_ballAverage: equicontinuity of the ball averages of a family.
• TauCeti.continuous_ballAverage, TauCeti.memLp_ballAverage: a ball average at positive scale is continuous and remains in Lᵖ.
• TauCeti.ballAverage_sub_self, TauCeti.eLpNorm_ballAverage_sub_le: the deviation of f from its ball average as an average of increments, and the Lᵖ approximation estimate.

References

Lane A.6 of TauCetiRoadmap/PDE/README.md; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 4.26 and Lemma 4.3; H. Hanche-Olsen, H. Holden, The Kolmogorov--Riesz compactness theorem, Expo. Math. 28 (2010).

theorem TauCeti.enorm_setAverage_rpow_le {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {mu : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → F} {s : Set α} {q : ℝ} (hq : 1 ≤ q) (hf : MeasureTheory.AEStronglyMeasurable f mu) (hs0 : mu s ≠ 0) (hs : mu s ≠ ⊤) : ‖⨍ (y : α) in s, f y ∂mu‖ₑ ^ q ≤ (mu s)⁻¹ * ∫⁻ (y : α) in s, ‖f y‖ₑ ^ q ∂mu

Hölder's bound on an average, in ∫⁻ form: the q-th power of the average of f over a set s of finite positive measure is at most (μ s)⁻¹ times the integral of ‖f‖ ^ q over s. The single factor (μ s)⁻¹ is what survives after the q-th power of the normalization (μ s)⁻¹ cancels against the (μ s) ^ (q - 1) of Hölder's inequality.

theorem TauCeti.enorm_setAverage_le {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {mu : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → F} {p : ENNReal} {s : Set α} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f mu) (hs0 : mu s ≠ 0) (hs : mu s ≠ ⊤) : ‖⨍ (y : α) in s, f y ∂mu‖ₑ ≤ mu s ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm f p (mu.restrict s)

Hölder's bound on an average: the average of f over a set s of finite positive measure is at most μ s ^ (-1/p) times the Lᵖ seminorm of f on s. At p = 1 this is the bound by the average of ‖f‖, and the volume factor sharpens as p grows because a larger exponent controls the mass of s more efficiently.

noncomputable def TauCeti.ballAverage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (mu : MeasureTheory.Measure E) (r : ℝ) (f : E → F) (x : E) : F

The ball average of f at scale r: the mean of f over the ball of radius r centred at the point.

Equations

• TauCeti.ballAverage mu r f x = ⨍ (y : E) in Metric.ball x r, f y ∂mu

theorem TauCeti.ballAverage_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (mu : MeasureTheory.Measure E) (r : ℝ) (f : E → F) (x : E) : ballAverage mu r f x = ⨍ (y : E) in Metric.ball x r, f y ∂mu

The defining equation of the ball average.

@[simp]

theorem TauCeti.ballAverage_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (mu : MeasureTheory.Measure E) (r : ℝ) (x : E) : ballAverage mu r 0 x = 0

The ball average of the zero function is zero.

theorem TauCeti.ballAverage_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} {f : E → F} {r : ℝ} {g : E → F} {x : E} (hf : MeasureTheory.IntegrableOn f (Metric.ball x r) mu) (hg : MeasureTheory.IntegrableOn g (Metric.ball x r) mu) : ballAverage mu r (f + g) x = ballAverage mu r f x + ballAverage mu r g x

The ball average commutes with addition when both summands are integrable on the ball.

theorem TauCeti.ballAverage_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} {f : E → F} {r : ℝ} {g : E → F} {x : E} (hf : MeasureTheory.IntegrableOn f (Metric.ball x r) mu) (hg : MeasureTheory.IntegrableOn g (Metric.ball x r) mu) : ballAverage mu r (f - g) x = ballAverage mu r f x - ballAverage mu r g x

The ball average commutes with subtraction when both terms are integrable on the ball.

theorem TauCeti.ballAverage_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} {f : E → F} {r : ℝ} (c : ℝ) (x : E) : ballAverage mu r (c • f) x = c • ballAverage mu r f x

The ball average commutes with scalar multiplication.

theorem TauCeti.ballAverage_congr_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} {f : E → F} {r : ℝ} [OpensMeasurableSpace E] {g : E → F} (h : f =ᵐ[mu] g) : ballAverage mu r f = ballAverage mu r g

The ball average depends on f only through its almost-everywhere class.

theorem TauCeti.ballAverage_eq_setAverage_ball_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {r : ℝ} (x : E) : ballAverage mu r f x = ⨍ (e : E) in Metric.ball 0 r, f (x + e) ∂mu

Recentring the ball at the origin: the ball average is the average of f over the translates of the point by the vectors of the ball of radius r.

theorem TauCeti.ballAverage_comp_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {r : ℝ} (e x : E) : ballAverage mu r (fun (y : E) => f (y + e)) x = ballAverage mu r f (x + e)

The ball average commutes with translation.

@[simp]

theorem TauCeti.ballAverage_const {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {r : ℝ} (hr : 0 < r) (c : F) (x : E) : ballAverage mu r (fun (x : E) => c) x = c

The ball average of a constant is that constant: the normalization is the intended one.

theorem TauCeti.enorm_ballAverage_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f mu) (hr : 0 < r) (x : E) : ‖ballAverage mu r f x‖ₑ ≤ mu (Metric.ball 0 r) ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm f p mu

The L^∞ bound on the ball average: it is controlled by the Lᵖ seminorm of f, at the cost of the volume factor μ (ball 0 r) ^ (-1/p), which blows up as r → 0.

theorem TauCeti.ballAverage_sub_ballAverage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hf : MeasureTheory.MemLp f p mu) (e x : E) : ballAverage mu r f (x + e) - ballAverage mu r f x = ballAverage mu r (fun (y : E) => f (y + e) - f y) x

The increment of the ball average is the ball average of the increment.

theorem TauCeti.enorm_ballAverage_add_sub_ballAverage_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.MemLp f p mu) (hr : 0 < r) (e x : E) : ‖ballAverage mu r f (x + e) - ballAverage mu r f x‖ₑ ≤ mu (Metric.ball 0 r) ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm (fun (y : E) => f (y + e) - f y) p mu

The equicontinuity estimate: the ball average moves by at most the Lᵖ modulus of continuity of f itself, up to the scale-dependent volume factor μ (ball 0 r) ^ (-1/p). Thus, at each fixed positive r, a family whose translates move uniformly little in Lᵖ has uniformly equicontinuous ball averages.

theorem TauCeti.uniformEquicontinuous_ballAverage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} {r : ℝ} {ι : Type u_3} {u : ι → E → F} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hu : ∀ (i : ι), MeasureTheory.MemLp (u i) p mu) (hr : 0 < r) (htrans : ∀ (ε : ENNReal), 0 < ε → ∃ δ > 0, ∀ (i : ι) (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun (x : E) => u i (x + h) - u i x) p mu ≤ ε) : UniformEquicontinuous fun (i : ι) => ballAverage mu r (u i)

At a fixed positive scale, the ball averages of a family of Lᵖ functions whose translation increments are uniformly small in Lᵖ form a uniformly equicontinuous family.

theorem TauCeti.continuous_ballAverage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.MemLp f p mu) (hr : 0 < r) : Continuous (ballAverage mu r f)

At every positive scale, the ball average of an Lᵖ function is continuous.

theorem TauCeti.ballAverage_sub_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hf : MeasureTheory.MemLp f p mu) (hr : 0 < r) (x : E) : ballAverage mu r f x - f x = ⨍ (e : E) in Metric.ball 0 r, f (x + e) - f x ∂mu

Writing the deviation of f from its ball average as an average of increments.

theorem TauCeti.eLpNorm_ballAverage_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f mu) (hr : 0 < r) : MeasureTheory.eLpNorm (ballAverage mu r f) p mu ≤ MeasureTheory.eLpNorm f p mu

The ball average is an Lᵖ contraction, for 1 ≤ p < ∞. This is Minkowski's integral inequality for the normalized indicator of a ball; it is the reason the smoothing operator does not have to be undone quantitatively.

theorem TauCeti.memLp_ballAverage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hf : MeasureTheory.MemLp f p mu) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hr : 0 < r) : MeasureTheory.MemLp (ballAverage mu r f) p mu

At every positive scale, taking the ball average preserves membership in Lᵖ.

theorem TauCeti.eLpNorm_ballAverage_sub_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {f : E → F} {p : ENNReal} {r : ℝ} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : MeasureTheory.MemLp f p mu) (hr : 0 < r) {C : ENNReal} (hC : ∀ e ∈ Metric.ball 0 r, MeasureTheory.eLpNorm (fun (y : E) => f (y + e) - f y) p mu ≤ C) : MeasureTheory.eLpNorm (fun (x : E) => ballAverage mu r f x - f x) p mu ≤ C

The Lᵖ approximation estimate: f is close to its ball average at scale r by no more than the largest Lᵖ translation increment of f over translations of size less than r. This is the half of the Fréchet--Kolmogorov criterion that pays for the smoothing: a family whose translates move uniformly little in Lᵖ is uniformly close to the family of its ball averages.