Symmetric kernels

A symmetric kernel on a measure space (Ω, μ) is an honest, everywhere-defined function Ω → Ω → ℝ that is symmetric, jointly measurable, and uniformly bounded. It is the carrier the dense graph limit theory is built on: a graphon is a [0, 1]-valued symmetric kernel, and the cut norm is defined on kernels rather than on graphons precisely so that a difference U - W of two graphons is in its domain.

Strict, not AEEqFun. The kernel carries a genuine function, not an a.e.-equivalence class. The a.e. identification is taken once and later, at GraphonSpace, rather than being built into the basic object. Two things follow, and they are why the roadmap makes this choice. First, the strict kernel is a pointwise ℝ-module — (U - W) x y = U x y - W x y holds on the nose, so cut-norm estimates never carry a null-set side condition. Second, pointwise hypotheses such as ∀ x y, W x y ∈ Set.Icc 0 1 are stateable at all, which an a.e. class cannot support without choosing a representative.

The measure is a phantom parameter. SymmKernel Ω μ does not mention μ in any field: none of symmetry, measurability, or boundedness refers to it. It is carried in the type so that kernels over different measures on the same space are not silently interchangeable, and so that later measure-dependent structure (the cut norm, the GraphonSpace quotient) has somewhere to attach. Consequently the algebra below needs no hypothesis on μ at all — in particular not IsProbabilityMeasure.

Main definitions

• TauCeti.DenseGraphLimits.SymmKernel — the strict symmetric kernel structure, with a FunLike coercion, extensionality by the underlying function, and symm / measurable / exists_bound accessors.
• TauCeti.DenseGraphLimits.SymmKernel.comap — the pullback of a kernel along a measurable map, acting on both arguments.

Main results

• AddCommGroup and Module ℝ instances, defined pointwise. The coe_zero, coe_add, coe_neg, coe_sub and coe_smul simp lemmas identify every operation with the corresponding operation on Ω → Ω → ℝ, so the module structure can be computed entirely by simp.
• SymmKernel.integrable_uncurry says that a bounded kernel is integrable on the product of two finite copies of its measure.
• comap_apply evaluates a pullback, and comap_zero / comap_add / comap_neg / comap_sub / comap_smul say that pulling back is linear, so a pullback of a difference of kernels is the difference of the pullbacks. comap_id and comap_comap are the functoriality laws.

Implementation

Each operation must re-establish all three fields. Symmetry and measurability are immediate. Boundedness is where the constants are chosen: C + D for a sum or difference, C for a negation, and |c| * C for a scalar multiple. Since the bound is existential (∃ C, ∀ x y, |K x y| ≤ C) rather than a fixed constant, no sharpness is claimed or needed.

The algebraic instances are then transported along the injective coercion with Function.Injective.addCommGroup and Function.Injective.module, which is what makes the pointwise formulas definitional.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the strict kernel carrier. The Graphon structure, cutNorm, homomorphism densities, and the L⁰-to-strict representative bridge are separate targets and are not built here.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013).

structure TauCeti.DenseGraphLimits.SymmKernel (Ω : Type u_2) [MeasurableSpace Ω] (_μ : MeasureTheory.Measure Ω) : Type u_2

A symmetric kernel: an everywhere-defined symmetric, jointly measurable, uniformly bounded function Ω → Ω → ℝ.

The measure is a phantom parameter — no field mentions it — but it is carried in the type so that kernels over different measures do not unify, and so that the measure-dependent theory built on top has somewhere to attach.

• toFun : Ω → Ω → ℝ

  The underlying function. Use the FunLike coercion rather than this field.

• symm' (x y : Ω) : self.toFun x y = self.toFun y x

  The kernel is symmetric. Stated via SymmKernel.symm.

• meas' : Measurable (Function.uncurry self.toFun)

  The kernel is jointly measurable. Stated via SymmKernel.measurable.

• bdd' : ∃ (C : ℝ), ∀ (x y : Ω), |self.toFun x y| ≤ C

  The kernel is uniformly bounded. Stated via SymmKernel.exists_bound.

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instFunLike {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : FunLike (SymmKernel Ω μ) Ω (Ω → ℝ)

Equations

• TauCeti.DenseGraphLimits.SymmKernel.instFunLike = { coe := TauCeti.DenseGraphLimits.SymmKernel.toFun, coe_injective := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.coe_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (f : Ω → Ω → ℝ) (hs : ∀ (x y : Ω), f x y = f y x) (hm : Measurable (Function.uncurry f)) (hb : ∃ (C : ℝ), ∀ (x y : Ω), |f x y| ≤ C) : ⇑{ toFun := f, symm' := hs, meas' := hm, bdd' := hb } = f

theorem TauCeti.DenseGraphLimits.SymmKernel.ext {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {K L : SymmKernel Ω μ} (h : ∀ (x y : Ω), K x y = L x y) : K = L

theorem TauCeti.DenseGraphLimits.SymmKernel.ext_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {K L : SymmKernel Ω μ} : K = L ↔ ∀ (x y : Ω), K x y = L x y

theorem TauCeti.DenseGraphLimits.SymmKernel.symm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (K : SymmKernel Ω μ) (x y : Ω) : K x y = K y x

A symmetric kernel is symmetric.

theorem TauCeti.DenseGraphLimits.SymmKernel.measurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (K : SymmKernel Ω μ) : Measurable (Function.uncurry ⇑K)

A symmetric kernel is jointly measurable.

theorem TauCeti.DenseGraphLimits.SymmKernel.exists_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (K : SymmKernel Ω μ) : ∃ (C : ℝ), ∀ (x y : Ω), |K x y| ≤ C

A symmetric kernel is uniformly bounded. The constant is not canonical.

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

A bounded symmetric kernel is integrable on the product of two finite copies of its measure.

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instZero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : Zero (SymmKernel Ω μ)

Equations

• TauCeti.DenseGraphLimits.SymmKernel.instZero = { zero := { toFun := fun (x x_1 : Ω) => 0, symm' := ⋯, meas' := ⋯, bdd' := ⋯ } }

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instAdd {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : Add (SymmKernel Ω μ)

Equations

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

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instNeg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : Neg (SymmKernel Ω μ)

Equations

• TauCeti.DenseGraphLimits.SymmKernel.instNeg = { neg := fun (K : TauCeti.DenseGraphLimits.SymmKernel Ω μ) => { toFun := fun (x y : Ω) => -K x y, symm' := ⋯, meas' := ⋯, bdd' := ⋯ } }

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instSub {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : Sub (SymmKernel Ω μ)

Equations

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

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instSMulReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : SMul ℝ (SymmKernel Ω μ)

Equations

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

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instSMulNat {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : SMul ℕ (SymmKernel Ω μ)

Equations

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

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instSMulInt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : SMul ℤ (SymmKernel Ω μ)

Equations

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

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.coe_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : ⇑0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.coe_nsmul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (n : ℕ) (K : SymmKernel Ω μ) : ⇑(n • K) = n • ⇑K

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.coe_zsmul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (n : ℤ) (K : SymmKernel Ω μ) : ⇑(n • K) = n • ⇑K

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instAddCommGroup {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : AddCommGroup (SymmKernel Ω μ)

Equations

• TauCeti.DenseGraphLimits.SymmKernel.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.DenseGraphLimits.SymmKernel.instModuleReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} : Module ℝ (SymmKernel Ω μ)

Equations

• TauCeti.DenseGraphLimits.SymmKernel.instModuleReal = Function.Injective.module ℝ { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

def TauCeti.DenseGraphLimits.SymmKernel.comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (K : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') : SymmKernel Ω' μ'

The pullback of a symmetric kernel along a measurable map f : Ω' → Ω, acting on both arguments: K.comap f hf μ' x y = K (f x) (f y).

Symmetry, measurability and boundedness are all inherited from K, so no hypothesis beyond measurability of f is needed — and none on either measure, since μ and μ' are phantom parameters of the two kernel types. The map comes first, as it does for ProbabilityTheory.Kernel.comap; the target measure μ' trails it as an explicit argument, because it is not determined by the data.

This is how a kernel on one carrier is read on another. Two uses in the dense graph limit theory: the overlaid difference on a coupling of two carriers is the difference of the two pullbacks along the coordinate projections, and the measure-preserving-map form of the cut distance compares pullbacks along maps out of a common carrier.

Equations

• K.comap f hf μ' = { toFun := fun (x y : Ω') => K (f x) (f y), symm' := ⋯, meas' := ⋯, bdd' := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (K : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') (x y : Ω') : (K.comap f hf μ') x y = K (f x) (f y)

Pulling back a kernel evaluates it after applying the map to both arguments.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') : comap 0 f hf μ' = 0

Pulling back the zero kernel gives the zero kernel.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_add {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (K L : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') : (K + L).comap f hf μ' = K.comap f hf μ' + L.comap f hf μ'

Pullback distributes over addition of kernels.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_neg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (K : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') : (-K).comap f hf μ' = -K.comap f hf μ'

Pullback commutes with negation of kernels.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_sub {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (K L : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') : (K - L).comap f hf μ' = K.comap f hf μ' - L.comap f hf μ'

Pullback distributes over subtraction of kernels.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_smul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} [MeasurableSpace Ω'] (c : ℝ) (K : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') : (c • K).comap f hf μ' = c • K.comap f hf μ'

Pullback commutes with scalar multiplication of kernels.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_id {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (K : SymmKernel Ω μ) : K.comap id ⋯ μ = K

Pulling back along the identity is the identity.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.comap_comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} {Ω'' : Type u_3} [MeasurableSpace Ω'] [MeasurableSpace Ω''] (K : SymmKernel Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') (g : Ω'' → Ω') (hg : Measurable g) (μ'' : MeasureTheory.Measure Ω'') : (K.comap f hf μ').comap g hg μ'' = K.comap (f ∘ g) ⋯ μ''

Pullbacks compose contravariantly.