The Fréchet--Kolmogorov compactness criterion in Lᵖ

The Fréchet--Kolmogorov (or Kolmogorov--Riesz) theorem is the Lᵖ analogue of Arzelà--Ascoli: it identifies the sets of Lᵖ functions that are relatively compact. This file proves its sufficiency direction, for 1 ≤ p < ∞ and functions on a proper normed additive group E carrying an additive Haar measure, with values in a finite-dimensional real normed space. A family S of Lᵖ functions is totally bounded as soon as

• it is bounded in Lᵖ;
• its translation increments are uniformly small: for every ε > 0 there is a δ > 0 with ‖f(· + h) - f‖_p ≤ ε for every f ∈ S and every ‖h‖ < δ;
• it is uniformly tight in the sense of MeasureTheory.UnifTight.

Neither of the last two hypotheses can be dropped. On ℝ, the concentrating family n ^ (1/p) 1_{[0, 1/n]} is bounded and tight but has translation increments of size of order one at every scale, and the escaping family f(· - n) of translates of a single nonzero f is bounded and has a translation-invariant modulus but is not tight; neither is totally bounded. The Lᵖ bound is carried explicitly, as in the classical statements.

The tightness hypothesis is automatic for a family vanishing almost everywhere off a fixed bounded set, which is the form TauCeti.totallyBounded_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl records. This is the form that Rellich--Kondrachov for W^{1,p}_0(Ω) consumes: extending by zero makes a function vanish off Ω, and its translation increments are controlled by ‖h‖ ‖∇u‖_p through TauCeti.W1p.eLpNorm_value_comp_add_sub_value_le_mul_enorm_gradient. The W^{1,p}(Ω) clause of Lane A.6 additionally needs an extension operator and boundary regularity.

The proof

The two halves of the argument are already available. Smoothing is done by the ball average TauCeti.ballAverage, whose four estimates are in TauCeti/MeasureTheory/Function/Lp/BallAverage.lean: at a fixed scale r the ball averages of the family are uniformly bounded (TauCeti.enorm_ballAverage_le), uniformly equicontinuous (TauCeti.enorm_ballAverage_add_sub_ballAverage_le, packaged for a family as TauCeti.uniformEquicontinuous_ballAverage) and, once r is smaller than the translation modulus of the family at ε, uniformly within ε of the family itself (TauCeti.eLpNorm_ballAverage_sub_le). Compactness of that smoothed family is Mathlib's BoundedContinuousFunction.arzela_ascoli, applied after restricting the ball averages to a large compact closed ball K.

Putting the two together, ‖f - f'‖_p for f' the chosen approximant is split as the Lᵖ seminorm over K plus the one over its complement. Off K tightness bounds each of f and f' separately; on K the difference is compared with the difference of the two ball averages, which is uniformly at most η there, and μ K ^ (1/p) η is made small by the choice of η.

Main declarations

• TauCeti.totallyBounded_of_comp_add_sub_of_unifTight, TauCeti.isCompact_closure_of_comp_add_sub_of_unifTight: the Fréchet--Kolmogorov criterion, in totally bounded and in relatively compact form.
• TauCeti.totallyBounded_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl, TauCeti.isCompact_closure_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl: the criterion for a family vanishing almost everywhere off a fixed bounded set, in totally bounded and in relatively compact form.

References

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

theorem TauCeti.totallyBounded_of_comp_add_sub_of_unifTight {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤) {S : Set ↥(MeasureTheory.Lp F p mu)} {M : ENNReal} (hM : M ≠ ⊤) (hbdd : ∀ f ∈ S, MeasureTheory.eLpNorm (↑↑f) p mu ≤ M) (htrans : ∀ (ε : ENNReal), 0 < ε → ∃ δ > 0, ∀ f ∈ S, ∀ (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun (x : E) => ↑↑f (x + h) - ↑↑f x) p mu ≤ ε) (htight : MeasureTheory.UnifTight (fun (i : ↑S) => ↑↑↑i) p mu) : TotallyBounded S

The Fréchet--Kolmogorov compactness criterion. For 1 ≤ p < ∞, a family S of Lᵖ functions is totally bounded as soon as it is bounded in Lᵖ, its translation increments are uniformly small in Lᵖ, and it is uniformly tight in the sense of MeasureTheory.UnifTight.

Dropping either of the last two hypotheses breaks the conclusion: on ℝ the concentrating family n ^ (1/p) 1_{[0, 1/n]} satisfies all but the smallness of translations, and the escaping family f(· - n) of translates of a single nonzero f satisfies all but tightness, and neither is totally bounded.

theorem TauCeti.isCompact_closure_of_comp_add_sub_of_unifTight {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤) {S : Set ↥(MeasureTheory.Lp F p mu)} {M : ENNReal} (hM : M ≠ ⊤) (hbdd : ∀ f ∈ S, MeasureTheory.eLpNorm (↑↑f) p mu ≤ M) (htrans : ∀ (ε : ENNReal), 0 < ε → ∃ δ > 0, ∀ f ∈ S, ∀ (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun (x : E) => ↑↑f (x + h) - ↑↑f x) p mu ≤ ε) (htight : MeasureTheory.UnifTight (fun (i : ↑S) => ↑↑↑i) p mu) : IsCompact (closure S)

Relative compactness in Lᵖ under the Fréchet--Kolmogorov hypotheses: the closure of an Lᵖ-bounded, uniformly tight family whose translation increments are uniformly small in Lᵖ is compact. This is the relative-compactness form of TauCeti.totallyBounded_of_comp_add_sub_of_unifTight.

theorem TauCeti.totallyBounded_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤) {S : Set ↥(MeasureTheory.Lp F p mu)} {s : Set E} (hs : Bornology.IsBounded s) (hsupp : ∀ f ∈ S, ∀ᵐ (x : E) ∂mu, x ∉ s → ↑↑f x = 0) {M : ENNReal} (hM : M ≠ ⊤) (hbdd : ∀ f ∈ S, MeasureTheory.eLpNorm (↑↑f) p mu ≤ M) (htrans : ∀ (ε : ENNReal), 0 < ε → ∃ δ > 0, ∀ f ∈ S, ∀ (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun (x : E) => ↑↑f (x + h) - ↑↑f x) p mu ≤ ε) : TotallyBounded S

The Fréchet--Kolmogorov criterion for a family vanishing almost everywhere off a fixed bounded set, the form that Rellich--Kondrachov for W^{1,p}_0(Ω) consumes. For such functions the tightness hypothesis is automatic, so an Lᵖ-bounded family whose translation increments are uniformly small in Lᵖ is totally bounded.

theorem TauCeti.isCompact_closure_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤) {S : Set ↥(MeasureTheory.Lp F p mu)} {s : Set E} (hs : Bornology.IsBounded s) (hsupp : ∀ f ∈ S, ∀ᵐ (x : E) ∂mu, x ∉ s → ↑↑f x = 0) {M : ENNReal} (hM : M ≠ ⊤) (hbdd : ∀ f ∈ S, MeasureTheory.eLpNorm (↑↑f) p mu ≤ M) (htrans : ∀ (ε : ENNReal), 0 < ε → ∃ δ > 0, ∀ f ∈ S, ∀ (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun (x : E) => ↑↑f (x + h) - ↑↑f x) p mu ≤ ε) : IsCompact (closure S)

Relative compactness in Lᵖ of a family vanishing almost everywhere off a fixed bounded set whose translation increments are uniformly small: the closure of such an Lᵖ-bounded family is compact. This is the shape in which a compact embedding theorem is stated.