Kernel Operators from Graphons

This file defines the integral operator associated with a graphon and proves basic properties.

Experimental: This module provides a pointwise kernel operator definition. The full L² operator API (continuous linear map, Hilbert-Schmidt, compactness) is future work.

Main definitions

• Graphon.kernelOpFun — Pointwise kernel operator (T_W f)(x) = ∫ W(x,y) f(y) dμ(y)

Main results

• Graphon.kernelOpFun_symmetric — Symmetry of the bilinear form
• Graphon.kernelOpFun_bound_ae — Pointwise bound by ‖f‖₁

Implementation notes

The kernel operator is central to spectral theory of graphons. Background facts (not yet formalized here):

• T_W is a Hilbert-Schmidt operator (hence compact) when W ∈ L²
• T_W is self-adjoint since W is symmetric
• The eigenvalues of T_W are related to homomorphism densities

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 7.5

The kernel operator

noncomputable def Graphon.kernelOpFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (f : α → ℝ) (x : α) : ℝ

The kernel operator applied to a function.

Given a graphon W : α × α → ℝ and a function f : α → ℝ, the kernel operator produces (T_W f)(x) = ∫ W(x,y) f(y) dμ(y).

This is the basic building block for the L² operator.

Note on well-definedness: This definition evaluates W.toAEEqFun (x, y) pointwise. Since W is only defined a.e., the section W(x, ·) may depend on the representative for a null set of x values. A more robust definition would construct an L²-valued operator directly. For graphons on standard probability spaces, this issue is typically resolved by working with canonical representatives.

Equations

• W.kernelOpFun f x = ∫ (y : α), ↑W.toAEEqFun (x, y) * f y ∂μ

theorem Graphon.graphon_abs_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, |↑W.toAEEqFun p| ≤ 1

Graphon values are bounded by 1 in absolute value (a.e.).

theorem Graphon.graphon_section_integrable_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (f : α → ℝ) (hf : MeasureTheory.Integrable f μ) : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (y : α) => ↑W.toAEEqFun (x, y) * f y) μ

Section integrability: for a.e. x, the section y ↦ W(x,y) * f(y) is integrable.

This follows from Fubini's theorem applied to the integrable function W * (f ∘ snd).

theorem Graphon.kernelOpFun_add_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (f g : α → ℝ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (x : α) ∂μ, W.kernelOpFun (f + g) x = W.kernelOpFun f x + W.kernelOpFun g x

The kernel operator is linear in the function argument (a.e. version).

Note: The equality holds for a.e. x, since integrability of sections y ↦ W(x,y) * f(y) only holds for a.e. x via Fubini.

theorem Graphon.kernelOpFun_smul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (c : ℝ) (f : α → ℝ) : W.kernelOpFun (c • f) = c • W.kernelOpFun f

The kernel operator respects scalar multiplication.

theorem Graphon.kernelOpFun_symmetric {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (f g : α → ℝ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : ∫ (x : α), W.kernelOpFun f x * g x ∂μ = ∫ (x : α), f x * W.kernelOpFun g x ∂μ

The kernel operator is symmetric in the inner product sense.

For integrable f, g: ∫ (T_W f) * g = ∫ f * (T_W g).

This follows from the symmetry of W: W(x,y) = W(y,x) a.e.

Proof outline:

1. LHS = ∫ x, (∫ y, W(x,y) f(y)) g(x) dμ(x) = ∫∫ W(x,y) f(y) g(x) dμ(y) dμ(x) (Fubini)
2. RHS = ∫ x, f(x) (∫ y, W(x,y) g(y)) dμ(x) = ∫∫ W(x,y) f(x) g(y) dμ(y) dμ(x) (Fubini)
3. Swap (x,y) in RHS and use W(y,x) = W(x,y) a.e.

The proof requires integral_integral and integral_prod_symm from Mathlib.MeasureTheory.Integral.Prod.

theorem Graphon.kernelOpFun_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (f : α → ℝ) : zero.kernelOpFun f = 0

The kernel operator of the zero graphon is zero.

Note: This holds pointwise (not just a.e.) because zero.toAEEqFun = AEEqFun.const 0 evaluates to 0 everywhere when the measure is nonzero.

theorem Graphon.kernelOpFun_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (f : α → ℝ) : one.kernelOpFun f = fun (x : α) => ∫ (y : α), f y ∂μ

The kernel operator of the one graphon equals the integral of f.

Note: This holds pointwise (not just a.e.) because one.toAEEqFun = AEEqFun.const 1 evaluates to 1 everywhere when the measure is nonzero.

theorem Graphon.kernelOpFun_bound_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (f : α → ℝ) (hf : MeasureTheory.Integrable f μ) : ∀ᵐ (x : α) ∂μ, |W.kernelOpFun f x| ≤ ∫ (y : α), |f y| ∂μ

Bound on the kernel operator output (a.e. version).

For f ∈ L², for a.e. x, |(T_W f)(x)| ≤ ‖f‖_L¹ since |W| ≤ 1 a.e.

Note: The bound holds for a.e. x (not all x), since graphon values are only guaranteed to be in [0,1] a.e. on the product measure, and sections inherit this property a.e. via Fubini.

L² operator (future work)

The full development of the L² operator T_W : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ requires:

1. Showing kernelOpFun maps L² to L² (uses L² boundedness)
2. Constructing the ContinuousLinearMap
3. Proving self-adjointness in the inner product sense
4. Hilbert-Schmidt property and compactness

These are not yet implemented.