Fréchet-Kolmogorov precompactness criterion in L²(ℝⁿ)

A family of L² functions that is uniformly bounded, supported in a fixed ball, and uniformly Lipschitz under translation is totally bounded in L²(ℝⁿ). This is the Fréchet-Kolmogorov (Riesz-Kolmogorov) criterion, the precompactness engine behind the Rellich-Kondrachov compact embedding.

The proof approximates each member of the family by its average over a fixed grid of axis-aligned cubes of side η. The averaging operator lands in the finite-dimensional span of the cube indicators, so its image is totally bounded; the approximation error is controlled by the translation modulus through a cube-averaging estimate that reuses the squared-Tonelli pattern of MeasureTheory.integral_sq_sub_translation_le. A finite net of the averaged family, widened by the uniform approximation error, is a finite net of the original family.

Main results

• MeasureTheory.sq_setIntegral_le: the finite-measure Cauchy-Schwarz bound (∫_s f)² ≤ μ.real s * ∫_s f².
• MeasureTheory.totallyBounded_of_lipschitz_translation: the Fréchet-Kolmogorov criterion.

theorem totallyBounded_of_approx {X : Type u_1} [PseudoMetricSpace X] {S : Set X} (h : ∀ ε > 0, ∃ (T : Set X), TotallyBounded T ∧ ∀ s ∈ S, ∃ t ∈ T, dist s t < ε) : TotallyBounded S

Approximation by totally bounded sets. If every member of S is approximable to arbitrary precision by a totally bounded set, then S is totally bounded.

theorem totallyBounded_of_finiteDimensional_bounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : Submodule ℝ E) [FiniteDimensional ℝ ↥V] {T : Set E} (hTV : T ⊆ ↑V) (hT : Bornology.IsBounded T) : TotallyBounded T

Total boundedness inside a finite-dimensional subspace. A bounded subset of a finite-dimensional subspace of a real normed space is totally bounded in the ambient space.

Finite-measure Cauchy-Schwarz bound

theorem MeasureTheory.sq_setIntegral_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) {f : α → ℝ} (hf : IntegrableOn f s μ) (hf2 : IntegrableOn (fun (x : α) => f x ^ 2) s μ) : (∫ (x : α) in s, f x ∂μ) ^ 2 ≤ μ.real s * ∫ (x : α) in s, f x ^ 2 ∂μ

Finite-measure Cauchy-Schwarz with one constant factor. For a set of finite measure, the square of the integral of f is at most μ.real s times the integral of f ^ 2. This is the general-measure analogue of MeasureTheory.sq_intervalIntegral_le.

L² space, translation, and the squared norm as an integral

@[reducible, inline]

noncomputable abbrev MeasureTheory.EucL2 (n : ℕ) : AddSubgroup (EuclideanSpace ℝ (Fin n) →ₘ[volume] ℝ)

L²(ℝⁿ) with Lebesgue measure.

Equations

• MeasureTheory.EucL2 n = MeasureTheory.Lp ℝ 2 MeasureTheory.volume

theorem MeasureTheory.norm_sq_eq_integral_sq {n : ℕ} (g : ↥(EucL2 n)) : ‖g‖ ^ 2 = ∫ (x : EuclideanSpace ℝ (Fin n)), ↑↑g x ^ 2

The squared L² norm is the integral of the square.

noncomputable def MeasureTheory.transL2 {n : ℕ} (h : EuclideanSpace ℝ (Fin n)) : ↥(EucL2 n) →ₗᵢ[ℝ] ↥(EucL2 n)

Translation by h as a linear isometry of L²(ℝⁿ).

Equations

• MeasureTheory.transL2 h = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => x + h) ⋯

theorem MeasureTheory.coeFn_transL2 {n : ℕ} (h : EuclideanSpace ℝ (Fin n)) (g : ↥(EucL2 n)) : ↑↑((transL2 h) g) =ᵐ[volume] fun (x : EuclideanSpace ℝ (Fin n)) => ↑↑g (x + h)

A translate is represented almost everywhere by the shifted function.

theorem MeasureTheory.norm_sq_transL2_sub {n : ℕ} (h : EuclideanSpace ℝ (Fin n)) (g : ↥(EucL2 n)) : ‖(transL2 h) g - g‖ ^ 2 = ∫ (x : EuclideanSpace ℝ (Fin n)), (↑↑g (x + h) - ↑↑g x) ^ 2

The squared L² norm of a translation difference, as an integral.

Cube grid

def MeasureTheory.cube {n : ℕ} (η : ℝ) (k : Fin n → ℤ) : Set (EuclideanSpace ℝ (Fin n))

The half-open cube of side η at lattice index k, as a subset of EuclideanSpace ℝ (Fin n).

Equations

• MeasureTheory.cube η k = WithLp.ofLp ⁻¹' Set.univ.pi fun (i : Fin n) => Set.Ico (η * ↑(k i)) (η * (↑(k i) + 1))

theorem MeasureTheory.mem_cube {n : ℕ} {η : ℝ} {k : Fin n → ℤ} {x : EuclideanSpace ℝ (Fin n)} : x ∈ cube η k ↔ ∀ (i : Fin n), x.ofLp i ∈ Set.Ico (η * ↑(k i)) (η * (↑(k i) + 1))

Membership of a cube is coordinatewise membership of the defining half-open intervals.

theorem MeasureTheory.measurableSet_cube {n : ℕ} (η : ℝ) (k : Fin n → ℤ) : MeasurableSet (cube η k)

Every cube is measurable.

theorem MeasureTheory.volume_cube {n : ℕ} (η : ℝ) (k : Fin n → ℤ) : volume (cube η k) = ENNReal.ofReal η ^ n

A cube of side η has volume η ^ n, independently of the lattice index.

theorem MeasureTheory.volume_cube_ne_top {n : ℕ} (η : ℝ) (k : Fin n → ℤ) : volume (cube η k) ≠ ⊤

A cube has finite volume, the form the integration lemmas take as a hypothesis.

theorem MeasureTheory.volume_real_cube {n : ℕ} {η : ℝ} (hη : 0 ≤ η) (k : Fin n → ℤ) : volume.real (cube η k) = η ^ n

The volume of a cube of nonnegative side, read as a real number.

theorem MeasureTheory.cube_disjoint {n : ℕ} {η : ℝ} (hη : 0 < η) {k k' : Fin n → ℤ} (hk : k ≠ k') : Disjoint (cube η k) (cube η k')

Cubes at distinct lattice indices are disjoint.

theorem MeasureTheory.coord_dist_lt_of_mem_cube {n : ℕ} {η : ℝ} {k : Fin n → ℤ} {x y : EuclideanSpace ℝ (Fin n)} (hx : x ∈ cube η k) (hy : y ∈ cube η k) (i : Fin n) : |x.ofLp i - y.ofLp i| < η

Two points of a common cube differ by less than η in each coordinate.

Displacement box

def MeasureTheory.dbox {n : ℕ} (η : ℝ) : Set (EuclideanSpace ℝ (Fin n))

The open displacement box (-η, η)ⁿ in EuclideanSpace ℝ (Fin n): the set of admissible differences of two points sharing a side-η cube.

Equations

• MeasureTheory.dbox η = WithLp.ofLp ⁻¹' Set.univ.pi fun (x : Fin n) => Set.Ioo (-η) η

theorem MeasureTheory.mem_dbox {n : ℕ} {η : ℝ} {w : EuclideanSpace ℝ (Fin n)} : w ∈ dbox η ↔ ∀ (i : Fin n), w.ofLp i ∈ Set.Ioo (-η) η

Membership of the displacement box is coordinatewise membership of (-η, η).

theorem MeasureTheory.measurableSet_dbox {n : ℕ} (η : ℝ) : MeasurableSet (dbox η)

The displacement box is measurable.

theorem MeasureTheory.volume_dbox {n : ℕ} (η : ℝ) : volume (dbox η) = ENNReal.ofReal (2 * η) ^ n

The displacement box of half-width η has volume (2 η) ^ n.

theorem MeasureTheory.volume_dbox_ne_top {n : ℕ} (η : ℝ) : volume (dbox η) ≠ ⊤

The displacement box has finite volume, the form the integration lemmas take as a hypothesis.

theorem MeasureTheory.volume_real_dbox {n : ℕ} {η : ℝ} (hη : 0 ≤ η) : volume.real (dbox η) = (2 * η) ^ n

The volume of the displacement box of nonnegative half-width, read as a real number.

theorem MeasureTheory.sub_mem_dbox_of_mem_cube {n : ℕ} {η : ℝ} {k : Fin n → ℤ} {x y : EuclideanSpace ℝ (Fin n)} (hx : x ∈ cube η k) (hy : y ∈ cube η k) : y - x ∈ dbox η

The coordinate difference of two points in a common cube lies in the displacement box.

theorem MeasureTheory.normSq_le_of_mem_dbox {n : ℕ} {η : ℝ} {w : EuclideanSpace ℝ (Fin n)} (hw : w ∈ dbox η) : ‖w‖ ^ 2 ≤ ↑n * η ^ 2

A point of the displacement box has squared norm at most n * η ^ 2.

Cube-averaging operator

noncomputable def MeasureTheory.cubeIndicator {n : ℕ} (η : ℝ) (k : Fin n → ℤ) : ↥(EucL2 n)

The L² class of the indicator of the cube cube η k.

Equations

• MeasureTheory.cubeIndicator η k = MeasureTheory.indicatorConstLp 2 ⋯ ⋯ 1

noncomputable def MeasureTheory.cubeCoef {n : ℕ} (η : ℝ) (k : Fin n → ℤ) (g : ↥(EucL2 n)) : ℝ

The average value of g over the cube cube η k.

Equations

• MeasureTheory.cubeCoef η k g = (MeasureTheory.volume.real (MeasureTheory.cube η k))⁻¹ * ∫ (x : EuclideanSpace ℝ (Fin n)) in MeasureTheory.cube η k, ↑↑g x

noncomputable def MeasureTheory.avg {n : ℕ} (η : ℝ) (K : Finset (Fin n → ℤ)) (g : ↥(EucL2 n)) : ↥(EucL2 n)

The cube-averaging operator: the piecewise-constant approximation of g on the grid of side-η cubes indexed by K, as an element of L².

Equations

• MeasureTheory.avg η K g = ∑ k ∈ K, MeasureTheory.cubeCoef η k g • MeasureTheory.cubeIndicator η k

noncomputable def MeasureTheory.stepFun {n : ℕ} (η : ℝ) (K : Finset (Fin n → ℤ)) (g : ↥(EucL2 n)) : EuclideanSpace ℝ (Fin n) → ℝ

The averaging operator as a pointwise piecewise-constant function.

Equations

• MeasureTheory.stepFun η K g x = ∑ k ∈ K, MeasureTheory.cubeCoef η k g * (MeasureTheory.cube η k).indicator (fun (x : EuclideanSpace ℝ (Fin n)) => 1) x

theorem MeasureTheory.coeFn_lp_sum {n : ℕ} {ι : Type u_2} (s : Finset ι) (F : ι → ↥(EucL2 n)) : ↑↑(∑ i ∈ s, F i) =ᵐ[volume] fun (x : EuclideanSpace ℝ (Fin n)) => ∑ i ∈ s, ↑↑(F i) x

The coercion of a finite L² sum is almost everywhere the pointwise sum.

theorem MeasureTheory.coeFn_avg {n : ℕ} (η : ℝ) (K : Finset (Fin n → ℤ)) (g : ↥(EucL2 n)) : ↑↑(avg η K g) =ᵐ[volume] stepFun η K g

The averaging operator agrees almost everywhere with its piecewise-constant representative.

theorem MeasureTheory.avg_mem_span {n : ℕ} (η : ℝ) (K : Finset (Fin n → ℤ)) (g : ↥(EucL2 n)) : avg η K g ∈ Submodule.span ℝ (cubeIndicator η '' ↑K)

The averaging operator lands in the finite-dimensional span of the cube indicators.

theorem MeasureTheory.stepFun_eq_on_cube {n : ℕ} {η : ℝ} (hη : 0 < η) {K : Finset (Fin n → ℤ)} {g : ↥(EucL2 n)} {k₀ : Fin n → ℤ} (hk₀ : k₀ ∈ K) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ cube η k₀) : stepFun η K g x = cubeCoef η k₀ g

On a cube of the grid, the piecewise-constant representative equals that cube's average.

Approximation error as a sum of cube variances

theorem MeasureTheory.integrableOn_cube_sq_sub {n : ℕ} (η : ℝ) (k : Fin n → ℤ) (g : ↥(EucL2 n)) (c : ℝ) : IntegrableOn (fun (y : EuclideanSpace ℝ (Fin n)) => (↑↑g y - c) ^ 2) (cube η k) volume

On any cube the squared deviation of g from a constant is integrable.

theorem MeasureTheory.norm_sq_sub_avg_eq {n : ℕ} {η : ℝ} (hη : 0 < η) {K : Finset (Fin n → ℤ)} {g : ↥(EucL2 n)} (hsupp : ∀ᵐ (x : EuclideanSpace ℝ (Fin n)), x ∉ ⋃ k ∈ K, cube η k → ↑↑g x = 0) : ‖g - avg η K g‖ ^ 2 = ∑ k ∈ K, ∫ (x : EuclideanSpace ℝ (Fin n)) in cube η k, (↑↑g x - cubeCoef η k g) ^ 2

Approximation error as a sum of cube variances. When g is supported in the union of the grid cubes, the squared L² distance from g to its cube-average is the sum over cubes of the squared deviation of g from its average on that cube.

Cube-translation estimate

theorem MeasureTheory.integrableOn_prod_sq_sub {n : ℕ} (g : ↥(EucL2 n)) {s t : Set (EuclideanSpace ℝ (Fin n))} (hμs : volume s ≠ ⊤) (hμt : volume t ≠ ⊤) : IntegrableOn (fun (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) => (↑↑g p.1 - ↑↑g p.2) ^ 2) (s ×ˢ t) (volume.prod volume)

The squared difference (g x - g y) ^ 2 is integrable over a product of finite-measure sets.

theorem MeasureTheory.integrable_prod_displacement {n : ℕ} (g : ↥(EucL2 n)) {D : Set (EuclideanSpace ℝ (Fin n))} (hμD : volume D ≠ ⊤) : Integrable (fun (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) => (↑↑g p.1 - ↑↑g (p.1 + p.2)) ^ 2) (volume.prod (volume.restrict D))

Displacement product integrability. The squared difference (g x - g (x + w)) ^ 2 is integrable over ℝⁿ × D for any finite-measure D of displacements. This is what admits the Tonelli swap in the cube-translation estimate: the w-marginal of the integrand is the constant ‖g‖ ^ 2 (translation is an L² isometry), so integrable_prod_iff' closes.

theorem MeasureTheory.integrableOn_dbox_sq_sub_translate {n : ℕ} {η : ℝ} (g : ↥(EucL2 n)) (x : EuclideanSpace ℝ (Fin n)) : IntegrableOn (fun (w : EuclideanSpace ℝ (Fin n)) => (↑↑g x - ↑↑g (x + w)) ^ 2) (dbox η) volume

The squared difference of g at x and x + w is integrable over the displacement box.

theorem MeasureTheory.inner_displacement_le {n : ℕ} {η : ℝ} (k : Fin n → ℤ) (g : ↥(EucL2 n)) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ cube η k) : ∫ (y : EuclideanSpace ℝ (Fin n)) in cube η k, (↑↑g x - ↑↑g y) ^ 2 ≤ ∫ (w : EuclideanSpace ℝ (Fin n)) in dbox η, (↑↑g x - ↑↑g (x + w)) ^ 2

Displacement substitution. On a cube the integral of the squared difference is at most the integral of the squared translation difference over the displacement box.

theorem MeasureTheory.integral_displacement_marginal {n : ℕ} (g : ↥(EucL2 n)) {D : Set (EuclideanSpace ℝ (Fin n))} (hD : MeasurableSet D) (hμD : volume D ≠ ⊤) : ∫ (x : EuclideanSpace ℝ (Fin n)), ∫ (w : EuclideanSpace ℝ (Fin n)) in D, (↑↑g x - ↑↑g (x + w)) ^ 2 = ∫ (w : EuclideanSpace ℝ (Fin n)) in D, ‖(transL2 w) g - g‖ ^ 2

Tonelli marginal. Swapping the order of integration turns the displacement integral into the translation modulus integrated over the displacement set.

theorem MeasureTheory.sum_cube_double_le_translation {n : ℕ} {η : ℝ} (hη : 0 < η) (K : Finset (Fin n → ℤ)) (g : ↥(EucL2 n)) : ∑ k ∈ K, ∫ (x : EuclideanSpace ℝ (Fin n)) (y : EuclideanSpace ℝ (Fin n)) in cube η k, (↑↑g x - ↑↑g y) ^ 2 ≤ ∫ (w : EuclideanSpace ℝ (Fin n)) in dbox η, ‖(transL2 w) g - g‖ ^ 2

Cube-translation bound. Summing the per-cube double integrals over the grid is controlled by the translation modulus integrated over the displacement box.

theorem MeasureTheory.cube_variance_le {n : ℕ} {η : ℝ} (hη : 0 < η) (k : Fin n → ℤ) (g : ↥(EucL2 n)) : ∫ (x : EuclideanSpace ℝ (Fin n)) in cube η k, (↑↑g x - cubeCoef η k g) ^ 2 ≤ (η ^ n)⁻¹ * ∫ (x : EuclideanSpace ℝ (Fin n)) (y : EuclideanSpace ℝ (Fin n)) in cube η k, (↑↑g x - ↑↑g y) ^ 2

Per-cube variance bound (Jensen). The squared deviation of g from its average on a cube is at most the rescaled double integral of the squared difference over that cube.

theorem MeasureTheory.norm_sq_sub_avg_le_translation {n : ℕ} {η : ℝ} (hη : 0 < η) {K : Finset (Fin n → ℤ)} {g : ↥(EucL2 n)} (hsupp : ∀ᵐ (x : EuclideanSpace ℝ (Fin n)), x ∉ ⋃ k ∈ K, cube η k → ↑↑g x = 0) : ‖g - avg η K g‖ ^ 2 ≤ (η ^ n)⁻¹ * ∫ (w : EuclideanSpace ℝ (Fin n)) in dbox η, ‖(transL2 w) g - g‖ ^ 2

Uniform approximation estimate. For g supported in the union of the grid cubes, the squared L² distance from g to its cube-average is controlled by the translation modulus over the displacement box.

theorem MeasureTheory.integrableOn_dbox_translation_modulus {n : ℕ} {η : ℝ} (g : ↥(EucL2 n)) : IntegrableOn (fun (w : EuclideanSpace ℝ (Fin n)) => ‖(transL2 w) g - g‖ ^ 2) (dbox η) volume

The translation modulus is integrable over the displacement box.

theorem MeasureTheory.norm_sq_sub_avg_le_const {n : ℕ} {η : ℝ} (hη : 0 < η) {K : Finset (Fin n → ℤ)} {g : ↥(EucL2 n)} {Λ : ℝ} (hsupp : ∀ᵐ (x : EuclideanSpace ℝ (Fin n)), x ∉ ⋃ k ∈ K, cube η k → ↑↑g x = 0) (hmod : ∀ (h : EuclideanSpace ℝ (Fin n)), ‖(transL2 h) g - g‖ ≤ Λ * ‖h‖) : ‖g - avg η K g‖ ^ 2 ≤ 2 ^ n * ↑n * Λ ^ 2 * η ^ 2

Constant approximation bound. With a uniform Lipschitz translation modulus Λ, the cube-average approximates g within 2 ^ n * n * Λ ^ 2 * η ^ 2 in squared L² norm.

Fréchet-Kolmogorov criterion

theorem MeasureTheory.coord_abs_le_norm {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) : |x.ofLp i| ≤ ‖x‖

Each coordinate of a Euclidean vector is bounded in absolute value by the norm.

theorem MeasureTheory.closedBall_subset_iUnion_cube {n : ℕ} {η : ℝ} (hη : 0 < η) (R : ℝ) : Metric.closedBall 0 R ⊆ ⋃ k ∈ Fintype.piFinset fun (x : Fin n) => Finset.Icc (-(⌈R / η⌉ + 1)) (⌈R / η⌉ + 1), cube η k

Coverage. A closed ball of radius R is covered by the finitely many grid cubes of side η whose lattice index lies in a box scaled to R / η.

theorem MeasureTheory.totallyBounded_of_lipschitz_translation {n : ℕ} (S : Set ↥(EucL2 n)) {R M Λ : ℝ} (hbdd : ∀ g ∈ S, ‖g‖ ≤ M) (hsupp : ∀ g ∈ S, ∀ᵐ (x : EuclideanSpace ℝ (Fin n)), x ∉ Metric.closedBall 0 R → ↑↑g x = 0) (hmod : ∀ g ∈ S, ∀ (h : EuclideanSpace ℝ (Fin n)), ‖(transL2 h) g - g‖ ≤ Λ * ‖h‖) : TotallyBounded S

Fréchet-Kolmogorov precompactness criterion. A family S of L²(ℝⁿ) functions that is uniformly bounded in norm, uniformly supported in a fixed closed ball, and uniformly Lipschitz under translation (with modulus Λ) is totally bounded. This is the precompactness engine behind the Rellich-Kondrachov compact embedding.

Passing a translation modulus to L² limits

The translation modulus that feeds totallyBounded_of_lipschitz_translation is closed under L² limits. This is the bridge from MeasureTheory.integral_sq_sub_translation_le, which supplies the estimate for smooth compactly supported functions, to its consequence on the L² classes of Sobolev functions: a Sobolev function is an L² limit of smooth compactly supported functions whose gradients are uniformly bounded, and the modulus passes to the limit. Both the graph-closure H₀¹ of the elliptic problem and the W^{1,p} structure of the Navier-Stokes development obtain their modulus through this lemma.

theorem MeasureTheory.transL2_sub_le_of_tendsto {n : ℕ} {g : ↥(EucL2 n)} {Λ : ℝ} {gk : ℕ → ↥(EucL2 n)} (htend : Filter.Tendsto gk Filter.atTop (nhds g)) (hmod : ∀ (k : ℕ) (h : EuclideanSpace ℝ (Fin n)), ‖(transL2 h) (gk k) - gk k‖ ≤ Λ * ‖h‖) (h : EuclideanSpace ℝ (Fin n)) : ‖(transL2 h) g - g‖ ≤ Λ * ‖h‖

A uniform translation modulus passes to an L² limit: if every gk k satisfies ‖transL2 h (gk k) - gk k‖ ≤ Λ * ‖h‖ and gk converges to g, then g satisfies the same bound.

theorem MeasureTheory.transL2_sub_le_of_tendsto' {n : ℕ} {g : ↥(EucL2 n)} {Λ : ℝ} {gk : ℕ → ↥(EucL2 n)} {Λk : ℕ → ℝ} (htend : Filter.Tendsto gk Filter.atTop (nhds g)) (hΛ : Filter.Tendsto Λk Filter.atTop (nhds Λ)) (hmod : ∀ (k : ℕ) (h : EuclideanSpace ℝ (Fin n)), ‖(transL2 h) (gk k) - gk k‖ ≤ Λk k * ‖h‖) (h : EuclideanSpace ℝ (Fin n)) : ‖(transL2 h) g - g‖ ≤ Λ * ‖h‖

A sharper limit form of transL2_sub_le_of_tendsto: the per-term moduli Λ k need only converge to Λ, not be uniformly bounded by it. This is the form a Sobolev function uses, since its smooth approximants have gradient norms that converge to, but need not equal, its own.