Compact Embedding D(E_λ) ↪ L²(I)

Defines sequential L² compactness and the form-norm ball (graph-norm bounded, compactly supported). Proves translation equicontinuity of the form-norm ball via the Kolmogorov-Riesz criterion and derives the compact embedding result.

Reference: lamportform.tex, Theorem KR, Lemma 13, Proposition 8 (lines 1061–1157).

Sequential L² compactness

def ConnesLean.IsRelativelyCompactL2 (K : Set (ℝ → ℂ)) : Prop

Sequential compactness in L²: every sequence in K has a subsequence converging in L² norm to some limit function.

This is the sequential characterization of relative compactness in L², used as the target property for the Kolmogorov-Riesz theorem.

Equations

• One or more equations did not get rendered due to their size.

Form-norm ball

def ConnesLean.formNormBall (cutoffLambda : ℝ) (M : ENNReal) : Set (ℝ → ℂ)

The form-norm ball: functions supported in I = [−log λ, log λ] with bounded graph norm ‖φ‖² + E_λ(φ) ≤ M.

This is the unit ball of the graph norm restricted to functions supported in the interval I. The Kolmogorov-Riesz theorem will show this set is relatively compact in L²(I).

Equations

• One or more equations did not get rendered due to their size.

Kolmogorov-Riesz criterion and compact embedding

axiom ConnesLean.kolmogorov_riesz_compact (K : Set (ℝ → ℂ)) (R : ℝ) (h_supp : ∀ φ ∈ K, Function.support φ ⊆ Set.Icc (-R) R) (h_bdd : ∃ M < ⊤, ∀ φ ∈ K, ∫⁻ (u : ℝ), ↑‖φ u‖₊ ^ 2 ≤ M) (h_equi : ∀ (ε : ENNReal), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ φ ∈ K, ∀ (h : ℝ), |h| < δ → ∫⁻ (u : ℝ), ↑‖φ (u - h) - φ u‖₊ ^ 2 < ε) : IsRelativelyCompactL2 K

Kolmogorov-Riesz compactness criterion for compactly supported L² functions. If K is a set of functions supported in [−R, R] with uniformly bounded L² norms and translation equicontinuity, then K is relatively compact in L².

Soundness: Preconditions (compact support, uniform L² bound, translation equicontinuity) are the three standard hypotheses of Kolmogorov-Riesz (Brezis, Corollary 4.27). No structure parameters.

Reference: Brezis, Corollary 4.27. The compact support condition subsumes the general tightness condition.

axiom ConnesLean.formNormBall_equicontinuous (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (M : ENNReal) (hM : M < ⊤) (ε : ENNReal) : 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ φ ∈ formNormBall cutoffLambda M, ∀ (h : ℝ), |h| < δ → ∫⁻ (u : ℝ), ↑‖φ (u - h) - φ u‖₊ ^ 2 < ε

The form-norm ball satisfies translation equicontinuity: for any ε > 0, there exists δ > 0 such that all φ in the form-norm ball satisfy ‖τ_h φ − φ‖₂² < ε whenever |h| < δ.

Soundness: Preconditions are 1 < cutoffLambda and M < ⊤ (finite energy bound), matching Lemma 13's hypotheses. No structure parameters.

Reference: lamportform.tex, Lemma 13 (lines 1078–1127). Uses Plancherel and frequency splitting to convert the form-norm bound into equicontinuity.

Proved theorems

theorem ConnesLean.zero_mem_formNormBall (cutoffLambda : ℝ) (M : ENNReal) : 0 ∈ formNormBall cutoffLambda M

The zero function belongs to the form-norm ball for any M ≥ 0.

theorem ConnesLean.formNormBall_nonempty (cutoffLambda : ℝ) (M : ENNReal) : (formNormBall cutoffLambda M).Nonempty

The form-norm ball is nonempty (contains the zero function).

theorem ConnesLean.formNormBall_monotone (cutoffLambda : ℝ) {M M' : ENNReal} (h : M ≤ M') : formNormBall cutoffLambda M ⊆ formNormBall cutoffLambda M'

The form-norm ball is monotone in M: if M ≤ M', then B(M) ⊆ B(M').

theorem ConnesLean.formNormBall_subset_formDomain (cutoffLambda : ℝ) {M : ENNReal} (hM : M < ⊤) : formNormBall cutoffLambda M ⊆ formDomain cutoffLambda

Every element of the form-norm ball (with M < ⊤) belongs to the form domain.

theorem ConnesLean.formNormBall_isRelativelyCompactL2 (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (M : ENNReal) (hM : M < ⊤) : IsRelativelyCompactL2 (formNormBall cutoffLambda M)

The form-norm ball is relatively compact in L²: the compact embedding D(E_λ) ↪ L²(I). Combines the Kolmogorov-Riesz criterion with the translation equicontinuity of the form-norm ball.

Reference: lamportform.tex, Proposition 8 (lines 1129–1157).