The cut norm of a symmetric kernel

This file defines the cut norm of a bounded symmetric kernel on a finite measure space by

‖K‖□ = sup |∫_(S × T) K|,

where the supremum ranges over measurable sets S and T. The file develops the interface needed by the cut-distance and counting-lemma layers: the bound of every rectangle by the cut norm, the seminorm laws, and the comparison with the L¹ norm. The integrals themselves — rectIntegral, testIntegral, partialIntegral and their analytic API — are in Kernel.Integral, so a consumer needing only those does not reach the supremum layer.

The definition uses strict representatives, consistently with SymmKernel. Consequently all pointwise algebra happens before integration; a later layer proves invariance under a.e. equality.

Main definitions

• TauCeti.DenseGraphLimits.cutNorm is the supremum of the absolute rectangle integrals.
• TauCeti.DenseGraphLimits.cutNormSet is the separately roadmap-pinned textbook set-form name for the same quantity.
• TauCeti.DenseGraphLimits.cutNormSigned is the signed cut norm: the same supremum taken over measurable [-1,1]-valued test functions rather than over indicators.

Main results

• abs_rectIntegral_le_cutNorm and cutNorm_le are the introduction and elimination rules for the supremum, and exists_cutNorm_eq_abs_rectIntegral says it is attained on a finite carrier.
• cutNorm_zero, cutNorm_neg, cutNorm_add_le, and cutNorm_smul are the seminorm laws.
• cutNorm_le_integral_abs bounds the cut norm by the L¹ norm, and cutNorm_eq_abs_of_forall_eq computes it for a constant kernel on a probability carrier.
• rectIntegral_comap_preimage and cutNorm_le_cutNorm_comap are the change of variables along a pushforward: a rectangle downstairs pulls back to one upstairs with the same integral, so the cut norm does not increase when a carrier is replaced by one it is a pushforward of.
• abs_testIntegral_le_cutNorm bounds every [0,1]-test integral by the cut norm itself, with no loss of constant — the form the counting lemma consumes, where the weights read off the other edges of a graph are [0,1]-valued.
• abs_testIntegral_le_cutNormSigned and cutNormSigned_le are the corresponding introduction and elimination rules for the signed cut norm.
• cutNorm_le_cutNormSigned and cutNormSigned_le_four_mul_cutNorm are the two sides of the factor sandwich relating the two forms.

References

• L. Lovász, Large Networks and Graph Limits, §8.2.1.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, §4.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the cut norm, its set form, and the signed form; the signatures follow TauCetiRoadmap/DenseGraphLimits/Suggested.lean.
• The definition and rectangle-integral interface follow Graphon/CutNorm.lean in cameronfreer/graphon (Apache 2.0) at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699; the strict-kernel integrability and full seminorm API are developed here.

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

The set form of the cut norm: the supremum of the absolute kernel integrals over measurable rectangles.

Equations

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

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

The cut norm of a symmetric kernel: the supremum over measurable sets S and T of the absolute integral over S × T.

Equations

• TauCeti.DenseGraphLimits.cutNorm μ K = TauCeti.DenseGraphLimits.cutNormSet μ K

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

The signed cut norm: the supremum, over measurable [-1,1]-valued test functions u and v, of |∫∫ u(x) v(y) K(x,y)|.

Relaxing the indicators of cutNorm to [-1,1]-valued functions can only increase the supremum (cutNorm_le_cutNormSigned), and increases it by at most a factor of 4 (cutNormSigned_le_four_mul_cutNorm), so the two forms define the same topology.

[IsFiniteMeasure μ] is required, as for cutNorm, and is not decoration: on an infinite measure the test integrals are unbounded — take μ Lebesgue, K the constant kernel 1, and u = v the indicator of [0, n], giving n² — so the conditionally complete supremum on ℝ would collapse to its junk value 0 for a kernel that is nowhere near zero. Finiteness is what makes abs_testIntegral_le_integral_abs bound the range, and hence what makes this a faithful supremum.

Equations

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

theorem TauCeti.DenseGraphLimits.cutNorm_eq_cutNormSet {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) : cutNorm μ K = cutNormSet μ K

The cut norm is definitionally its separately roadmap-pinned measurable-set form. This is not a simp lemma: cutNorm is the normal form that the rest of the API, and hence the simp set, is stated in.

theorem TauCeti.DenseGraphLimits.cutNormSet_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) : cutNormSet μ K = ⨆ (S : Set Ω), ⨆ (_ : MeasurableSet S), ⨆ (T : Set Ω), ⨆ (_ : MeasurableSet T), |SymmKernel.rectIntegral μ K S T|

The set-form cut norm is the iterated supremum over measurable rectangles.

theorem TauCeti.DenseGraphLimits.cutNorm_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {K : SymmKernel Ω μ} {C : ℝ} (h : ∀ (S : Set Ω), MeasurableSet S → ∀ (T : Set Ω), MeasurableSet T → |SymmKernel.rectIntegral μ K S T| ≤ C) : cutNorm μ K ≤ C

To prove an upper bound on the cut norm, it suffices to prove it for every measurable rectangle.

theorem TauCeti.DenseGraphLimits.abs_rectIntegral_le_cutNorm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) {S T : Set Ω} (hS : MeasurableSet S) (hT : MeasurableSet T) : |SymmKernel.rectIntegral μ K S T| ≤ cutNorm μ K

Every measurable rectangle integral is bounded by the cut norm.

theorem TauCeti.DenseGraphLimits.cutNorm_le_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {K : SymmKernel Ω μ} {C : ℝ} : cutNorm μ K ≤ C ↔ ∀ (S : Set Ω), MeasurableSet S → ∀ (T : Set Ω), MeasurableSet T → |SymmKernel.rectIntegral μ K S T| ≤ C

The cut norm is at most C exactly when every measurable rectangle integral is.

theorem TauCeti.DenseGraphLimits.exists_lt_abs_rectIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) {c : ℝ} (h : c < cutNorm μ K) : ∃ (S : Set Ω) (T : Set Ω), MeasurableSet S ∧ MeasurableSet T ∧ c < |SymmKernel.rectIntegral μ K S T|

Any strict lower bound on the cut norm is exceeded by some measurable rectangle integral.

theorem TauCeti.DenseGraphLimits.exists_cutNorm_eq_abs_rectIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [Finite Ω] [MeasurableSingletonClass Ω] (K : SymmKernel Ω μ) : ∃ (S : Set Ω) (T : Set Ω), cutNorm μ K = |SymmKernel.rectIntegral μ K S T|

On a finite carrier the cut norm is attained. When the carrier is finite and every subset of it is measurable, the supremum defining the cut norm is a maximum over rectangles.

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

The cut norm is nonnegative.

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

The cut norm is bounded by the integral of the absolute value of the kernel.

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

The cut norm is bounded by the L¹ seminorm of the kernel, read as a real number. This is cutNorm_le_integral_abs in the eLpNorm language of L¹ convergence.

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

A pointwise bound on a kernel bounds its cut norm, on a probability carrier.

The rectangle integrals defining the cut norm are integrals over subsets of a probability space, so no factor for the total mass appears.

theorem TauCeti.DenseGraphLimits.cutNorm_eq_abs_of_forall_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] {K : SymmKernel Ω μ} {c : ℝ} (hK : ∀ (x y : Ω), K x y = c) : cutNorm μ K = |c|

A kernel with the constant value c has cut norm |c| on a probability carrier: the whole square is an extremal rectangle.

@[simp]

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

The zero kernel has cut norm zero.

@[simp]

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

Negating a kernel does not change its cut norm.

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

Reversing a difference does not change its cut norm: ‖K - L‖□ = ‖L - K‖□.

Deliberately not @[simp]: neither argument order is a meaningful canonical form, so there is nothing for such a rule to normalize towards.

theorem TauCeti.DenseGraphLimits.cutNorm_add_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L : SymmKernel Ω μ) : cutNorm μ (K + L) ≤ cutNorm μ K + cutNorm μ L

The cut norm satisfies the triangle inequality.

theorem TauCeti.DenseGraphLimits.cutNorm_sub_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L : SymmKernel Ω μ) : cutNorm μ (K - L) ≤ cutNorm μ K + cutNorm μ L

The cut norm of a difference is at most the sum of the two cut norms.

theorem TauCeti.DenseGraphLimits.cutNorm_sub_le_cutNorm_sub_add_cutNorm_sub {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K L M : SymmKernel Ω μ) : cutNorm μ (K - M) ≤ cutNorm μ (K - L) + cutNorm μ (L - M)

The triangle inequality for the cut norm of differences.

@[simp]

theorem TauCeti.DenseGraphLimits.cutNorm_smul {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (c : ℝ) (K : SymmKernel Ω μ) : cutNorm μ (c • K) = |c| * cutNorm μ K

The cut norm is absolutely homogeneous.

theorem TauCeti.DenseGraphLimits.cutNorm_le_cutNorm_comap {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {α : Type u_2} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] {f : α → Ω} (hf : MeasureTheory.MeasurePreserving f ν μ) (K : SymmKernel Ω μ) : cutNorm μ K ≤ cutNorm ν (K.comap f ⋯ ν)

The cut norm does not increase along a pushforward. If f pushes ν forward to μ, then the cut norm of K over μ is at most the cut norm of its pullback over ν.

Every measurable rectangle downstairs pulls back to a measurable rectangle upstairs with the same integral (rectIntegral_comap_preimage), so the upstairs supremum ranges over at least as much. The swap application obtains equality by applying this bound in both directions. The common-carrier application only needs the stated inequality and identifies the pulled-back kernel outright.

theorem TauCeti.DenseGraphLimits.abs_testIntegral_le_cutNorm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) {u v : Ω → ℝ} (hu : Measurable u) (hv : Measurable v) (hu1 : ∀ (x : Ω), u x ∈ Set.Icc 0 1) (hv1 : ∀ (y : Ω), v y ∈ Set.Icc 0 1) : |SymmKernel.testIntegral μ K u v| ≤ cutNorm μ K

Every [0,1]-test integral is bounded by the cut norm. The pairing is affine in each test function, so replacing a [0,1]-valued test function by a suitable indicator only increases the absolute pairing; doing so on both sides lands on a measurable rectangle. Unlike the [-1,1]-valued case (cutNormSigned_le_four_mul_cutNorm) there is no factor of 4, which is what makes this the form the counting lemma consumes.

theorem TauCeti.DenseGraphLimits.cutNormSigned_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) : cutNormSigned μ K = ⨆ (u : Ω → ℝ), ⨆ (_ : Measurable u), ⨆ (_ : ∀ (x : Ω), u x ∈ Set.Icc (-1) 1), ⨆ (v : Ω → ℝ), ⨆ (_ : Measurable v), ⨆ (_ : ∀ (y : Ω), v y ∈ Set.Icc (-1) 1), |SymmKernel.testIntegral μ K u v|

The signed cut norm is the iterated supremum over measurable [-1,1]-valued test functions.

theorem TauCeti.DenseGraphLimits.abs_testIntegral_le_cutNormSigned {Ω : 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) : |SymmKernel.testIntegral μ K u v| ≤ cutNormSigned μ K

Every [-1,1]-test integral is bounded by the signed cut norm. This is the introduction rule for the supremum, mirroring abs_rectIntegral_le_cutNorm.

theorem TauCeti.DenseGraphLimits.cutNormSigned_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {K : SymmKernel Ω μ} {C : ℝ} (h : ∀ (u v : Ω → ℝ), Measurable u → Measurable v → (∀ (x : Ω), u x ∈ Set.Icc (-1) 1) → (∀ (y : Ω), v y ∈ Set.Icc (-1) 1) → |SymmKernel.testIntegral μ K u v| ≤ C) : cutNormSigned μ K ≤ C

To prove an upper bound on the signed cut norm, it suffices to prove it for every pair of measurable [-1,1]-valued test functions. Nonnegativity of the bound is not a hypothesis: it follows by testing against the zero function.

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

The signed cut norm is nonnegative.

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

The signed cut norm is bounded by the L¹ norm of the kernel, as the cut norm is.

theorem TauCeti.DenseGraphLimits.cutNorm_le_cutNormSigned {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) : cutNorm μ K ≤ cutNormSigned μ K

Lower side of the factor sandwich. The cut norm is at most the signed cut norm: indicators are [-1,1]-valued test functions, so the signed supremum ranges over more pairs.

theorem TauCeti.DenseGraphLimits.cutNormSigned_le_four_mul_cutNorm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (K : SymmKernel Ω μ) : cutNormSigned μ K ≤ 4 * cutNorm μ K

Upper side of the factor sandwich. Relaxing indicators to [-1,1]-valued test functions increases the cut norm by at most a factor of 4.