Documentation

TauCeti.Combinatorics.DenseGraphLimits.StepGraphon.Energy

The graphon partition energy #

The Frieze--Kannan weak regularity argument is a potential argument: refine a measurable finite partition as long as the block-average step graphon fails to approximate the graphon in cut norm, and bound the number of refinements by the growth of an L² potential that is trapped in [0, 1]. This file builds that potential.

graphonPartitionEnergy μ P hP W is the L²(μ ⊗ μ) norm squared of the block-average step graphon stepGraphonAvg, that is of E[W | P ⊗ P]. Its two structural properties are proved here:

Both rest on the same block computation: the energy is a finite sum of block contributions (graphonPartitionEnergy_eq_sum), and a block average over a refinement still reproduces the coarse block integrals (stepGraphonAvg_rectIntegral_of_le_of_le). That last identity needs no hypothesis excluding null parts: a null part of the finer partition cuts out a null rectangle, which contributes zero to both sides whatever value the step graphon takes there. The null-cell convention of stepGraphonAvg is what makes it a well-defined strict [0, 1]-valued representative at all — it is load-bearing for stepGraphonAvg_idem — but it is not what makes this identity true.

This is ‖E[W | P ⊗ P]‖₂² written entirely in terms of finite block averages; the identification with MeasureTheory.condExp belongs to the later a.e. layer, and nothing here needs it. It is also distinct from Mathlib's Finpartition.energy, which is the finite edge-density energy of a finite graph.

Main definitions #

Main results #

References #

source
@[simp]
theorem TauCeti.DenseGraphLimits.stepGraphonAvg_rectIntegral_of_le_of_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {P R Q : Finpartition Set.univ} (p : ↥P.parts) (r : ↥R.parts) (hQ : ∀ q ∈ Q.parts, MeasurableSet q) (hQP : Q ≤ P) (hQR : Q ≤ R) (W : Graphon Ω μ) :
SymmKernel.rectIntegral μ (stepGraphonAvg Q hQ W).toSymmKernel ↑p ↑r = SymmKernel.rectIntegral μ W.toSymmKernel ↑p ↑r

Block averaging over Q reproduces the integral over any rectangle whose two sides are parts of (possibly different) measurable partitions coarser than Q.

source
theorem TauCeti.DenseGraphLimits.l2inner_stepGraphonAvg_eq_sum {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) (K : SymmKernel Ω μ) :
l2inner μ K (stepGraphonAvg P hP W).toSymmKernel = ∑ pq : ↥P.parts × ↥P.parts, SymmKernel.rectIntegral μ K ↑pq.1 ↑pq.2 * ⨍ (z : Ω × Ω) in ↑pq.1 ×ˢ ↑pq.2, W z.1 z.2 ∂μ.prod μ

The L² pairing of any kernel with a block-average step graphon is the finite sum of its block integrals weighted by the block averages of W.

source
noncomputable def TauCeti.DenseGraphLimits.graphonPartitionEnergy {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
ℝ

The graphon partition energy of W over a measurable finite partition P: the L²(μ ⊗ μ) norm squared of the block-average step graphon E[W | P ⊗ P].

This is the analytic potential of the Frieze--Kannan weak regularity argument. It is not Mathlib's Finpartition.energy, which is the finite edge-density energy of a finite graph.

Equations
Instances For
    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ P hP W = l2sq μ (stepGraphonAvg P hP W).toSymmKernel

    The partition energy is the L² norm squared of the block-average step graphon. The definition's body is not exposed across module boundaries, so this is the unfolding lemma downstream modules should use.

    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_eq_sum {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ P hP W = ∑ pq : ↥P.parts × ↥P.parts, SymmKernel.rectIntegral μ W.toSymmKernel ↑pq.1 ↑pq.2 * ⨍ (z : Ω × Ω) in ↑pq.1 ×ˢ ↑pq.2, W z.1 z.2 ∂μ.prod μ

    The partition energy as a finite sum of block contributions: each block contributes the integral of W over it times the average of W on it.

    source
    theorem TauCeti.DenseGraphLimits.l2inner_graphon_stepGraphonAvg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    l2inner μ W.toSymmKernel (stepGraphonAvg P hP W).toSymmKernel = graphonPartitionEnergy μ P hP W

    The projection moment identity: pairing W against its block average equals the self-pairing of that block average, namely the partition energy.

    source
    theorem TauCeti.DenseGraphLimits.l2sq_sub_stepGraphonAvg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    l2sq μ (W.toSymmKernel - (stepGraphonAvg P hP W).toSymmKernel) = l2sq μ W.toSymmKernel - graphonPartitionEnergy μ P hP W

    The defect identity: the L² distance from W to its block average is the remaining gap between the graphon's L² norm squared and the current partition energy.

    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_le_l2sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ P hP W ≤ l2sq μ W.toSymmKernel

    The partition energy never exceeds the L² norm squared of the graphon — the Bessel-type bound following from the projection moment identity.

    source
    theorem TauCeti.DenseGraphLimits.l2inner_stepGraphonAvg_of_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (hQ : ∀ r ∈ Q.parts, MeasurableSet r) (href : Q ≤ P) (W : Graphon Ω μ) :
    l2inner μ (stepGraphonAvg Q hQ W).toSymmKernel (stepGraphonAvg P hP W).toSymmKernel = graphonPartitionEnergy μ P hP W

    Under refinement, the finer block-average step graphon pairs with the coarser one to give exactly the coarser energy: the coarse block average is unchanged by the finer averaging.

    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_increment {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (hQ : ∀ r ∈ Q.parts, MeasurableSet r) (href : Q ≤ P) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ Q hQ W = graphonPartitionEnergy μ P hP W + l2sq μ ((stepGraphonAvg Q hQ W).toSymmKernel - (stepGraphonAvg P hP W).toSymmKernel)

    The L²-Pythagoras energy increment. Refining a partition raises the energy by exactly the L² norm squared of the change in the block-average step graphon. This is the quantitative driver of the Frieze--Kannan iteration.

    Mathlib's refinement order has P ≤ Q mean that P refines Q, so Q ≤ P is the hypothesis that Q is the finer partition.

    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (hQ : ∀ r ∈ Q.parts, MeasurableSet r) (href : Q ≤ P) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ P hP W ≤ graphonPartitionEnergy μ Q hQ W

    The partition energy is monotone under refinement — the ≥ 0 corollary of the Pythagoras increment.

    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    0 ≤ graphonPartitionEnergy μ P hP W

    The partition energy is nonnegative.

    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_stepGraphonAvg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ P hP (stepGraphonAvg P hP W) = graphonPartitionEnergy μ P hP W

    Block averaging does not change the partition energy at the same partition: the block-average step graphon is already constant on the rectangles of P, so averaging it again changes nothing. This is the idempotence identity E(P, E[W|P⊗P]) = E(P, W).

    source
    theorem TauCeti.DenseGraphLimits.graphonPartitionEnergy_le_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) :
    graphonPartitionEnergy μ P hP W ≤ 1

    The partition energy is at most 1, because a graphon is [0, 1]-valued. With graphonPartitionEnergy_mono and graphonPartitionEnergy_nonneg this is the bounded monotone potential the Frieze--Kannan iteration runs on.