Documentation

Graphon.Operations

Operations on Graphons #

Experimental: This module defines basic operations on graphons: pointwise product and properties of the complement (already defined in Basic.lean).

Main definitions #

Main results #

Implementation notes #

The pointwise product W₁ * W₂ represents the AND of independent edge events. If W₁ and W₂ are graphon limits of graph sequences G_n and H_n, then W₁ * W₂ corresponds to the intersection G_n ∩ H_n.

The direct sum operation (combining two graphons on disjoint probability spaces) and operator product (composition via integral operators) are more complex and are not yet implemented.

References #

Pointwise multiplication #

source
noncomputable def Graphon.pointwiseMul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ : Graphon α μ) :
Graphon α μ

Pointwise multiplication of two graphons on the same probability space.

Given graphons W₁, W₂ : α × α → [0,1], their pointwise product is (W₁ * W₂)(x, y) = W₁(x, y) * W₂(x, y).

This represents the AND of independent edge events: if W₁ and W₂ are limits of graph sequences G_n and H_n, then W₁ * W₂ corresponds to the edge-intersection G_n ∩ H_n.

The product of values in [0,1] is again in [0,1], so pointwise multiplication preserves the graphon property.

Equations
Instances For
    source
    theorem Graphon.pointwiseMul_toAEEqFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ : Graphon α μ) :
    (W₁.pointwiseMul W₂).toAEEqFun = W₁.toAEEqFun * W₂.toAEEqFun

    The underlying AEEqFun of a pointwise product.

    source
    theorem Graphon.pointwiseMul_comm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ : Graphon α μ) :
    W₁.pointwiseMul W₂ = W₂.pointwiseMul W₁

    Pointwise multiplication is commutative.

    source
    theorem Graphon.pointwiseMul_assoc {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ W₃ : Graphon α μ) :
    (W₁.pointwiseMul W₂).pointwiseMul W₃ = W₁.pointwiseMul (W₂.pointwiseMul W₃)

    Pointwise multiplication is associative.

    source
    theorem Graphon.pointwiseMul_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) :
    W.pointwiseMul one = W

    Multiplying by the constant 1 graphon is the identity.

    source
    theorem Graphon.pointwiseMul_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) :
    W.pointwiseMul zero = zero

    Multiplying by the constant 0 graphon gives 0.

    source
    theorem Graphon.pointwiseMul_ae_mem_Icc {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ : Graphon α μ) :
    ∀ᵐ (p : α × α) ∂μ.prod μ, ↑(W₁.pointwiseMul W₂).toAEEqFun p ∈ Set.Icc 0 1

    The pointwise product takes values in [0,1] a.e.

    source
    theorem Graphon.compl_pointwiseMul_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ : Graphon α μ) :
    ∀ᵐ (p : α × α) ∂μ.prod μ, ↑(W₁.compl.pointwiseMul W₂).toAEEqFun p + ↑(W₁.pointwiseMul W₂).toAEEqFun p = ↑W₂.toAEEqFun p

    Pointwise multiplication distributes over complement from the right: (1 - W₁) * W₂ + W₁ * W₂ = W₂ (a.e.).

    This is the probabilistic identity: P(not A and B) + P(A and B) = P(B).

    Interaction with homomorphism density #

    source
    theorem Graphon.pointwiseMul_eval_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (W₁ W₂ : Graphon α μ) {v₁ v₂ : V} (hne : v₁ ≠ v₂) :
    ∀ᵐ (x : V → α) ∂MeasureTheory.Measure.pi fun (x : V) => μ, ↑(W₁.pointwiseMul W₂).toAEEqFun (x v₁, x v₂) = ↑W₁.toAEEqFun (x v₁, x v₂) * ↑W₂.toAEEqFun (x v₁, x v₂)

    The pointwise product evaluates to the product of evaluations, a.e. on the pi measure.

    source
    theorem Graphon.homDensity_pointwiseMul_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W₁ W₂ : Graphon α μ) :
    homDensity F (W₁.pointwiseMul W₂) ≤ min (homDensity F W₁) (homDensity F W₂)

    Homomorphism density of the pointwise product is bounded by the minimum of the individual densities.

    More precisely: t(F, W₁ * W₂) ≤ min(t(F, W₁), t(F, W₂)) since each edge probability is the product, which is at most either factor.