The L² pairing of symmetric kernels

The Frieze--Kannan weak regularity argument runs on an L²(μ ⊗ μ) potential, so the block-average step graphons of a refinement chain must be compared in L² and not only in cut norm. This file defines the integrals l2inner μ K L = ∫ K · L and l2sq μ K = ∫ K² at the level of strict symmetric kernels. When μ is finite, bounded kernels are square-integrable, so these integrals are the L²(μ ⊗ μ) integral pairing and squared seminorm on strict representatives. They induce the genuine inner product and norm squared after quotienting by a.e. equality. The integrability of a single kernel over the product carrier is already available as SymmKernel.integrable_uncurry from the basic kernel layer, and everything here is built on it.

Why plain integrals and not Lp. A SymmKernel is a strict everywhere-defined representative, and the whole point of that convention is that a difference K - L is again a literal kernel. Passing through MeasureTheory.Lp would replace each kernel by an a.e. class and force a.e. bookkeeping into a layer that has no need of it; the a.e. view is taken once, later, on the graphon quotient. Kernels are bounded, so when μ is finite the integrals below converge and the expansion l2sq_sub needs no additional side conditions.

Main definitions

• TauCeti.DenseGraphLimits.l2inner is the integral of the product of two symmetric kernels;
• TauCeti.DenseGraphLimits.l2sq is the integral of the square of a symmetric kernel.

Main results

• TauCeti.DenseGraphLimits.SymmKernel.integrable_mul is the integrability behind both;
• TauCeti.DenseGraphLimits.l2sq_sub expands the squared seminorm of a difference — the identity the Pythagoras energy increment is read off from;
• TauCeti.DenseGraphLimits.sq_rectIntegral_le_measureReal_mul_l2sq is the finite-measure rectangle Cauchy--Schwarz bound, and sq_rectIntegral_le_l2sq is its probability specialization;
• TauCeti.DenseGraphLimits.l2sq_le_one_of_abs_le_one bounds the squared seminorm of a kernel with values in [-1, 1] over a probability carrier.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1/2 — l2sq and the analytic energy stack. The l2sq signature and the l2sq_nonneg proof are taken from TauCetiRoadmap/DenseGraphLimits/Suggested.lean (Layer 1/2); the pairing l2inner and its bilinear API are developed here.
• The set-integral Cauchy--Schwarz argument follows Graphon/Regularity.lean in cameronfreer/graphon (Apache 2.0) at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699.

theorem TauCeti.DenseGraphLimits.SymmKernel.integrable_mul {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L : SymmKernel Ω μ) : MeasureTheory.Integrable (fun (p : Ω × Ω) => K p.1 p.2 * L p.1 p.2) (μ.prod μ)

The pointwise product of two symmetric kernels is integrable on the product carrier: both are bounded, and the product measure of a finite measure with itself is finite.

theorem TauCeti.DenseGraphLimits.SymmKernel.integrable_sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) : MeasureTheory.Integrable (fun (p : Ω × Ω) => K p.1 p.2 ^ 2) (μ.prod μ)

A symmetric kernel is square integrable on the product carrier.

noncomputable def TauCeti.DenseGraphLimits.l2inner {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K L : SymmKernel Ω μ) : ℝ

The integral of the product of two symmetric kernels. For finite μ, this is their L²(μ ⊗ μ) integral pairing, which becomes an inner product after quotienting by a.e. equality.

Equations

• TauCeti.DenseGraphLimits.l2inner μ K L = ∫ (p : Ω × Ω), K p.1 p.2 * L p.1 p.2 ∂μ.prod μ

theorem TauCeti.DenseGraphLimits.l2inner_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K L : SymmKernel Ω μ) : l2inner μ K L = ∫ (p : Ω × Ω), K p.1 p.2 * L p.1 p.2 ∂μ.prod μ

The defining equation of l2inner. The definition's body is not exposed across module boundaries, so this is the unfolding lemma downstream modules should use.

noncomputable def TauCeti.DenseGraphLimits.l2sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : ℝ

The integral of the square of a symmetric kernel. For finite μ, this is its squared L²(μ ⊗ μ) seminorm, which becomes a squared norm after quotienting by a.e. equality.

Equations

• TauCeti.DenseGraphLimits.l2sq μ K = ∫ (p : Ω × Ω), K p.1 p.2 ^ 2 ∂μ.prod μ

theorem TauCeti.DenseGraphLimits.l2sq_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : l2sq μ K = ∫ (p : Ω × Ω), K p.1 p.2 ^ 2 ∂μ.prod μ

The defining equation of l2sq. The definition's body is not exposed across module boundaries, so this is the unfolding lemma downstream modules should use.

theorem TauCeti.DenseGraphLimits.l2sq_eq_l2inner_self {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : l2sq μ K = l2inner μ K K

The squared L² seminorm is the integral pairing of a kernel with itself.

theorem TauCeti.DenseGraphLimits.l2sq_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : 0 ≤ l2sq μ K

The squared L² seminorm is nonnegative: it is the integral of a square.

theorem TauCeti.DenseGraphLimits.l2inner_comm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K L : SymmKernel Ω μ) : l2inner μ K L = l2inner μ L K

The L² integral pairing is symmetric.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_zero_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : l2inner μ 0 K = 0

Pairing the zero kernel on the left with any kernel gives zero.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_zero_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : l2inner μ K 0 = 0

Pairing any kernel with the zero kernel on the right gives zero.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_neg_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K L : SymmKernel Ω μ) : l2inner μ (-K) L = -l2inner μ K L

Negating the left argument negates the pairing.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_neg_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K L : SymmKernel Ω μ) : l2inner μ K (-L) = -l2inner μ K L

Negating the right argument negates the pairing.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_smul_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (c : ℝ) (K L : SymmKernel Ω μ) : l2inner μ (c • K) L = c * l2inner μ K L

Scaling the left argument scales the pairing.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_smul_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (c : ℝ) (K L : SymmKernel Ω μ) : l2inner μ K (c • L) = c * l2inner μ K L

Scaling the right argument scales the pairing.

@[simp]

theorem TauCeti.DenseGraphLimits.l2sq_zero {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : l2sq μ 0 = 0

@[simp]

theorem TauCeti.DenseGraphLimits.l2sq_neg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) : l2sq μ (-K) = l2sq μ K

The squared L² seminorm is unchanged by negation.

@[simp]

theorem TauCeti.DenseGraphLimits.l2sq_smul {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (c : ℝ) (K : SymmKernel Ω μ) : l2sq μ (c • K) = c ^ 2 * l2sq μ K

Scaling a kernel scales its squared L² seminorm by the square of the scalar.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_add_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L M : SymmKernel Ω μ) : l2inner μ (K + L) M = l2inner μ K M + l2inner μ L M

The L² integral pairing is additive in its left argument.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_add_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L M : SymmKernel Ω μ) : l2inner μ K (L + M) = l2inner μ K L + l2inner μ K M

The L² integral pairing is additive in its right argument.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_sub_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L M : SymmKernel Ω μ) : l2inner μ (K - L) M = l2inner μ K M - l2inner μ L M

The L² integral pairing subtracts in its left argument.

@[simp]

theorem TauCeti.DenseGraphLimits.l2inner_sub_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L M : SymmKernel Ω μ) : l2inner μ K (L - M) = l2inner μ K L - l2inner μ K M

The L² integral pairing subtracts in its right argument.

theorem TauCeti.DenseGraphLimits.l2sq_sub {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L : SymmKernel Ω μ) : l2sq μ (K - L) = l2sq μ K - 2 * l2inner μ K L + l2sq μ L

The expansion of the squared L² seminorm of a difference. Read backwards with a vanishing cross term, this is the Pythagoras identity the energy increment uses.

theorem TauCeti.DenseGraphLimits.sq_rectIntegral_le_measureReal_mul_l2sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) (S T : Set Ω) : SymmKernel.rectIntegral μ K S T ^ 2 ≤ (μ.prod μ).real (S ×ˢ T) * l2sq μ K

The square of a kernel's integral over a rectangle is at most the rectangle's measure times the kernel's squared L² seminorm.

theorem TauCeti.DenseGraphLimits.sq_rectIntegral_le_l2sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (K : SymmKernel Ω μ) (S T : Set Ω) : SymmKernel.rectIntegral μ K S T ^ 2 ≤ l2sq μ K

The square of a kernel's integral over any rectangle is at most its squared L² seminorm on a probability carrier.

theorem TauCeti.DenseGraphLimits.l2sq_le_one_of_abs_le_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (K : SymmKernel Ω μ) (h : ∀ (x y : Ω), |K x y| ≤ 1) : l2sq μ K ≤ 1

A kernel with values in [-1, 1] has squared L² seminorm at most 1 over a probability carrier.