Integrating a symmetric kernel

The integrals of a bounded symmetric kernel that the cut norm and its consumers are built from: over a measurable rectangle, against a pair of test functions, and against one test function with the other variable left free.

rectIntegral K S T = ∫ (S × T) K            testIntegral K u v = ∫∫ u(x) v(y) K(x,y)
partialIntegral K v x = ∫ v(y) K(x,y)

This file is deliberately independent of the cut norm. Several consumers — the block averages of a step graphon, and the L² theory — need rectangle integrals and nothing else, and previously reached the supremum and signed-cut-norm layer to obtain them.

The definitions use strict representatives, consistently with SymmKernel, so all pointwise algebra happens before integration.

Main definitions

• TauCeti.DenseGraphLimits.SymmKernel.rectIntegral — the integral over a rectangle;
• TauCeti.DenseGraphLimits.SymmKernel.testIntegral — the pairing with two test functions, of which a rectangle integral is the indicator case;
• TauCeti.DenseGraphLimits.SymmKernel.partialIntegral — the pairing with one.

Main results

• the additive and scaling laws for rectIntegral, and its L¹ bound;
• rectIntegral_uniformOn_univ — on a finite carrier with the uniform measure, a rectangle integral is a normalized finite sum;
• testIntegral_indicator_one — testing against indicators recovers a rectangle integral;
• testIntegral_eq_integral_partialIntegral — the iterated form.

References

• L. Lovász, Large Networks and Graph Limits, §8.2.1.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, §4.
• The rectangle-integral interface follows Graphon/CutNorm.lean in cameronfreer/graphon (Apache 2.0) at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699; the strict-kernel integrability is developed here.

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

The integral of a symmetric kernel over the rectangle S × T.

Equations

• TauCeti.DenseGraphLimits.SymmKernel.rectIntegral μ K S T = ∫ (p : Ω × Ω) in S ×ˢ T, K p.1 p.2 ∂μ.prod μ

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ K S T = ∫ (p : Ω × Ω) in S ×ˢ T, K p.1 p.2 ∂μ.prod μ

A rectangle integral is the product-measure integral restricted to the rectangle.

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_eq_setIntegral_setIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ K S T = ∫ (x : Ω) in S, ∫ (y : Ω) in T, K x y ∂μ ∂μ

A rectangle integral can be evaluated as an iterated set integral.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_empty_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) (T : Set Ω) : rectIntegral μ K ∅ T = 0

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_empty_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) (S : Set Ω) : rectIntegral μ K S ∅ = 0

@[simp]

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

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_comm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (K : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ K S T = rectIntegral μ K T S

Transposing a rectangle does not change the integral of a symmetric kernel.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_zero {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (S T : Set Ω) : rectIntegral μ 0 S T = 0

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_add {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ (K + L) S T = rectIntegral μ K S T + rectIntegral μ L S T

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_neg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ (-K) S T = -rectIntegral μ K S T

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_sub {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ (K - L) S T = rectIntegral μ K S T - rectIntegral μ L S T

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_smul {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (c : ℝ) (K : SymmKernel Ω μ) (S T : Set Ω) : rectIntegral μ (c • K) S T = c * rectIntegral μ K S T

theorem TauCeti.DenseGraphLimits.SymmKernel.abs_rectIntegral_le_integral_abs {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) (S T : Set Ω) : |rectIntegral μ K S T| ≤ ∫ (p : Ω × Ω), |K p.1 p.2| ∂μ.prod μ

The absolute value of any rectangle integral is bounded by the integral of |K| over the whole product space.

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_comap_preimage {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {α : Type u_2} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] {f : α → Ω} (hf : MeasureTheory.MeasurePreserving f ν μ) (K : SymmKernel Ω μ) {S T : Set Ω} (hS : MeasurableSet S) (hT : MeasurableSet T) : rectIntegral ν (K.comap f ⋯ ν) (f ⁻¹' S) (f ⁻¹' T) = rectIntegral μ K S T

Change of variables for a rectangle integral. If f pushes ν forward to μ, then the rectangle integral of K over S × T equals the rectangle integral of the pullback kernel over the preimage rectangle f ⁻¹' S × f ⁻¹' T.

The two rectangles carry the two measures of the type ascriptions, so this is the statement that lets a cut-norm estimate move between a carrier and a pushforward of it.

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_uniformOn_univ {α : Type u_2} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (K : SymmKernel α (ProbabilityTheory.uniformOn Set.univ)) (S T : Finset α) : rectIntegral (ProbabilityTheory.uniformOn Set.univ) K ↑S ↑T = (∑ x ∈ S, ∑ y ∈ T, K x y) / ↑(Fintype.card α) ^ 2

Rectangle integrals on a uniform finite carrier. On a finite carrier with the uniform probability measure, the integral of a kernel over S × T is its sum over the rectangle divided by the square of the number of points.

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

The integral of a symmetric kernel against a pair of test functions: ∫∫ u(x) v(y) K(x,y).

This generalises rectIntegral, which is the case of two indicator functions (testIntegral_indicator_one), and is the quantity the signed cut norm takes a supremum of.

Equations

• TauCeti.DenseGraphLimits.SymmKernel.testIntegral μ K u v = ∫ (p : Ω × Ω), u p.1 * v p.2 * K p.1 p.2 ∂μ.prod μ

theorem TauCeti.DenseGraphLimits.SymmKernel.testIntegral_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) (u v : Ω → ℝ) : testIntegral μ K u v = ∫ (p : Ω × Ω), u p.1 * v p.2 * K p.1 p.2 ∂μ.prod μ

A test integral is the product-measure integral of u ⊗ v · K.

theorem TauCeti.DenseGraphLimits.SymmKernel.integrable_testIntegrand {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) {u v : Ω → ℝ} (hu : Measurable u) (hv : Measurable v) (hu1 : ∀ (x : Ω), u x ∈ Set.Icc (-1) 1) (hv1 : ∀ (y : Ω), v y ∈ Set.Icc (-1) 1) : MeasureTheory.Integrable (fun (p : Ω × Ω) => u p.1 * v p.2 * K p.1 p.2) (μ.prod μ)

The integrand of a test integral is integrable when the test functions are measurable and [-1,1]-valued: it is then dominated pointwise by |K|, which is integrable.

theorem TauCeti.DenseGraphLimits.SymmKernel.abs_testIntegral_le_integral_abs {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) {u v : Ω → ℝ} (hu : Measurable u) (hv : Measurable v) (hu1 : ∀ (x : Ω), u x ∈ Set.Icc (-1) 1) (hv1 : ∀ (y : Ω), v y ∈ Set.Icc (-1) 1) : |testIntegral μ K u v| ≤ ∫ (p : Ω × Ω), |K p.1 p.2| ∂μ.prod μ

Every [-1,1]-test integral is bounded by the L¹ norm of the kernel. This is the bound that makes the signed cut norm's supremum a supremum of a bounded set.

@[simp]

theorem TauCeti.DenseGraphLimits.SymmKernel.testIntegral_indicator_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) {S T : Set Ω} (hS : MeasurableSet S) (hT : MeasurableSet T) : testIntegral μ K (S.indicator 1) (T.indicator 1) = rectIntegral μ K S T

Testing against two indicator functions recovers the rectangle integral. This is what makes the set form of the cut norm a special case of the signed form.

theorem TauCeti.DenseGraphLimits.SymmKernel.testIntegral_comm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (K : SymmKernel Ω μ) (u v : Ω → ℝ) : testIntegral μ K u v = testIntegral μ K v u

Swapping the two test functions of a symmetric kernel leaves the pairing unchanged.

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

The inner integral of a kernel against a single test function, x ↦ ∫ v(y) K(x,y).

This is the partial pairing that the extremal step of the factor sandwich optimises over. When μ is finite and v is measurable and [-1,1]-valued, the partial pairing is measurable and integrable. The definition itself asks nothing of v.

Equations

• TauCeti.DenseGraphLimits.SymmKernel.partialIntegral μ K v x = ∫ (y : Ω), v y * K x y ∂μ

theorem TauCeti.DenseGraphLimits.SymmKernel.partialIntegral_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) (v : Ω → ℝ) (x : Ω) : partialIntegral μ K v x = ∫ (y : Ω), v y * K x y ∂μ

The defining integral of partialIntegral.

theorem TauCeti.DenseGraphLimits.SymmKernel.measurable_partialIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (K : SymmKernel Ω μ) {v : Ω → ℝ} (hv : Measurable v) : Measurable (partialIntegral μ K v)

The partial pairing is measurable in the remaining variable.

theorem TauCeti.DenseGraphLimits.SymmKernel.integrable_partialIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) {v : Ω → ℝ} (hv : Measurable v) (hv1 : ∀ (y : Ω), v y ∈ Set.Icc (-1) 1) : MeasureTheory.Integrable (partialIntegral μ K v) μ

The partial pairing against a [-1,1]-valued test function is integrable.

theorem TauCeti.DenseGraphLimits.SymmKernel.testIntegral_eq_integral_partialIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (K : SymmKernel Ω μ) {u v : Ω → ℝ} (h : MeasureTheory.Integrable (fun (p : Ω × Ω) => u p.1 * v p.2 * K p.1 p.2) (μ.prod μ)) : testIntegral μ K u v = ∫ (x : Ω), u x * partialIntegral μ K v x ∂μ

A test integral is the integral of the left test function against the partial pairing.

Only integrability of the product integrand is needed — that is all Fubini asks. A caller with bounded measurable test functions gets it from integrable_testIntegrand.

theorem TauCeti.DenseGraphLimits.SymmKernel.testIntegral_sub_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) {u₁ u₂ v : Ω → ℝ} (h₁ : MeasureTheory.Integrable (fun (p : Ω × Ω) => u₁ p.1 * v p.2 * K p.1 p.2) (μ.prod μ)) (h₂ : MeasureTheory.Integrable (fun (p : Ω × Ω) => u₂ p.1 * v p.2 * K p.1 p.2) (μ.prod μ)) : testIntegral μ K (u₁ - u₂) v = testIntegral μ K u₁ v - testIntegral μ K u₂ v

The pairing is subtractive in the left test function, given integrability of both pieces.

theorem TauCeti.DenseGraphLimits.SymmKernel.testIntegral_sub_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : SymmKernel Ω μ) {u v₁ v₂ : Ω → ℝ} (h₁ : MeasureTheory.Integrable (fun (p : Ω × Ω) => u p.1 * v₁ p.2 * K p.1 p.2) (μ.prod μ)) (h₂ : MeasureTheory.Integrable (fun (p : Ω × Ω) => u p.1 * v₂ p.2 * K p.1 p.2) (μ.prod μ)) : testIntegral μ K u (v₁ - v₂) = testIntegral μ K u v₁ - testIntegral μ K u v₂

The pairing is subtractive in the right test function, given integrability of both pieces.