Finpartition adapter for analytic graphon regularity

This file connects Mathlib's Finpartition (Set.univ : Set α) to the measurable partitions used by the graphon regularity development. A Finpartition excludes the empty set, but a nonempty part may still have measure zero. Such parts are retained by the adapter.

The null-cell convention is therefore part of the API: Graphon.rectAverage agrees exactly with Mathlib's set average, and both assign value zero to a rectangle when either side has measure zero. Consequently every null-cell contribution to the partition energy is zero. No positive-measure hypothesis on partition parts is needed.

Main results

• Finpartition.toMeasurablePartition: the exact-cover adapter;
• Graphon.rectAverage_eq_setAverage: compatibility with Mathlib's set-average convention;
• Graphon.rectAverage_eq_zero_of_measure_eq_zero_left and Graphon.rectAverage_eq_zero_of_measure_eq_zero_right: the null-cell convention;
• Graphon.energy_toMeasurablePartition: the adapted energy is the same finite block sum.

noncomputable def Finpartition.toMeasurablePartition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : Finpartition Set.univ) (hP : ∀ S ∈ P.parts, MeasurableSet S) : MeasurablePartition α μ

Regard a measurable Finpartition of Set.univ as the graphon development's measurable partition. The finite partition covers exactly, hence in particular almost everywhere.

Equations

• P.toMeasurablePartition hP = { parts := P.parts, measurable_parts := hP, pairwiseDisjoint := ⋯, ae_covers := ⋯ }

@[simp]

theorem Finpartition.toMeasurablePartition_parts {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : Finpartition Set.univ) (hP : ∀ S ∈ P.parts, MeasurableSet S) : (P.toMeasurablePartition hP).parts = P.parts

theorem Graphon.rectAverage_eq_setAverage {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (S T : Set α) : W.rectAverage S T = ⨍ (p : α × α) in S ×ˢ T, ↑W.toAEEqFun p ∂μ.prod μ

The project's rectangle average is exactly Mathlib's set average on the rectangle. In particular this identifies the zero-denominator convention rather than merely proving an a.e. statement about the resulting step graphon.

theorem Graphon.rectAverage_eq_zero_of_measure_eq_zero_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (S T : Set α) (hS : μ S = 0) : W.rectAverage S T = 0

A rectangle with a null left side has average zero.

theorem Graphon.rectAverage_eq_zero_of_measure_eq_zero_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (S T : Set α) (hT : μ T = 0) : W.rectAverage S T = 0

A rectangle with a null right side has average zero.

theorem Graphon.energy_toMeasurablePartition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (P : Finpartition Set.univ) (hP : ∀ S ∈ P.parts, MeasurableSet S) : W.energy (P.toMeasurablePartition hP) = ∑ S ∈ P.parts, ∑ T ∈ P.parts, (μ S).toReal * (μ T).toReal * W.rectAverage S T ^ 2

The energy of a measurable Finpartition is the same finite block sum used by the native measurable-partition API. In particular the adapter introduces no normalization factor.