Documentation

TauCeti.Combinatorics.DenseGraphLimits.StepGraphon.Average

Block-averaged step graphons #

This file specializes stepGraphon to the matrix of averages of a graphon over the rectangles of a measurable finite partition. This is the step graphon used by the Frieze--Kannan weak regularity argument: on a block p ×ˢ q, its value is the Mathlib set average of the original graphon over that block.

The set-average convention matters for strict graphon representatives. A nonempty partition part may have measure zero, and Mathlib assigns average zero to a null rectangle. Thus stepGraphonAvg is everywhere [0, 1]-valued without choosing arbitrary values on null blocks. The block-integral theorem below shows that this convention does not change any weighted block contribution.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.DenseGraphLimits.blockAverage {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (W : Graphon Ω μ) (p q : ↥P.parts) :
↑(Set.Icc 0 1)

The average of a graphon over one rectangle of a finite partition, regarded as a point of [0, 1]. This is the canonical block matrix of stepGraphonAvg.

Equations
Instances For
    source
    theorem TauCeti.DenseGraphLimits.blockAverage_comm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (W : Graphon Ω μ) (p q : ↥P.parts) :
    blockAverage P W p q = blockAverage P W q p

    Rectangle averages of a symmetric graphon are symmetric in the two partition parts.

    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.coe_blockAverage {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (W : Graphon Ω μ) (p q : ↥P.parts) :
    ↑(blockAverage P W p q) = ⨍ (z : Ω × Ω) in ↑p ×ˢ ↑q, W z.1 z.2 ∂μ.prod μ

    The rectangle average, as a real number.

    source
    theorem TauCeti.DenseGraphLimits.coe_blockAverage_eq_inv_mul_rectIntegral {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (W : Graphon Ω μ) (p q : ↥P.parts) :
    ↑(blockAverage P W p q) = (μ.real ↑p * μ.real ↑q)⁻¹ * SymmKernel.rectIntegral μ W.toSymmKernel ↑p ↑q

    The rectangle average is the rectangle integral divided by the product of the two part measures. On a null rectangle both sides are zero, since the inverse of 0 is 0.

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

    The block-average step graphon of W with respect to a measurable finite partition P.

    Its value on p ×ˢ q is Mathlib's set average of W over that rectangle. In particular its value is zero when either side of the rectangle has measure zero.

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

      The block-average step graphon is the step graphon of the rectangle averages.

      stepGraphonAvg is a definition whose body is not exposed outside this module, so this is the only way a downstream file can name its block matrix.

      source
      theorem TauCeti.DenseGraphLimits.stepGraphonAvg_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) {p q : ↥P.parts} {x y : Ω} (hx : x ∈ ↑p) (hy : y ∈ ↑q) :
      (stepGraphonAvg P hP W) x y = ⨍ (z : Ω × Ω) in ↑p ×ˢ ↑q, W z.1 z.2 ∂μ.prod μ

      The block-average step graphon takes the average of W over its containing partition rectangle.

      source
      theorem TauCeti.DenseGraphLimits.stepGraphonAvg_apply_of_measure_eq_zero_left {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) {p q : ↥P.parts} {x y : Ω} (hp : μ ↑p = 0) (hx : x ∈ ↑p) (hy : y ∈ ↑q) :
      (stepGraphonAvg P hP W) x y = 0

      On a partition rectangle whose left side is null, the block-average step graphon is zero.

      This is not a simp lemma because the partition parts cannot be inferred from its left-hand side.

      source
      theorem TauCeti.DenseGraphLimits.stepGraphonAvg_apply_of_measure_eq_zero_right {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (W : Graphon Ω μ) {p q : ↥P.parts} {x y : Ω} (hq : μ ↑q = 0) (hx : x ∈ ↑p) (hy : y ∈ ↑q) :
      (stepGraphonAvg P hP W) x y = 0

      On a partition rectangle whose right side is null, the block-average step graphon is zero.

      This is not a simp lemma because the partition parts cannot be inferred from its left-hand side.

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

      Block averaging preserves the integral over each rectangle of the partition. This includes null rectangles: both sides are then zero under Mathlib's set-average convention.

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

      Block averaging with respect to a fixed partition is strictly idempotent. This is equality of strict graphon representatives, not merely almost-everywhere equality: after the first averaging, every null block already has the canonical value zero.

      source
      theorem TauCeti.DenseGraphLimits.stepGraphonAvg_stepGraphon_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (val : ↥P.parts → ↥P.parts → ↑(Set.Icc 0 1)) (hsymm : ∀ (p q : ↥P.parts), val p q = val q p) {p q : ↥P.parts} {x y : Ω} (hp : μ ↑p ≠ 0) (hq : μ ↑q ≠ 0) (hx : x ∈ ↑p) (hy : y ∈ ↑q) :
      (stepGraphonAvg P hP (stepGraphon P hP val hsymm)) x y = ↑(val p q)

      Averaging a step graphon recovers its prescribed value on every rectangle with two non-null sides. The non-null hypotheses are necessary: the strict null-cell convention replaces the value on a null rectangle by zero. This is not a simp lemma because the partition parts cannot be inferred from its left-hand side.