Examples of sample laws: the constant graphon is the binomial random graph (issue #21)

The sample law of the constant graphon with value p is exactly Mathlib's binomial random-graph distribution G(V, p) (SimpleGraph.binomialRandom):

• Graphon.sampleMass_constGraphon — the graphon-side mass computation sampleMass (constGraphon p) G = p^{e(G)} (1-p)^{\binom{k}{2} - e(G)};
• Graphon.sampleLaw_const_eq_binomial — equality of measures with G(Fin k, p), via Measure.ext_of_singleton and Mathlib's binomialRandom_singleton (reused, not reproved);
• endpoint simp corollaries: at p = 0 the law is dirac ⊥, at p = 1 it is dirac ⊤.

This file exists so that the binomial-random-graph import stays out of Graphon/SamplingLaw.lean. The stochastic-block-model law is deliberately deferred (see issue #21).

theorem Graphon.sampleMass_constGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (p : ↑(Set.Icc 0 1)) (G : SimpleGraph (Fin k)) : (constGraphon p).sampleMass G = ↑p ^ G.edgeFinset.card * (1 - ↑p) ^ (k.choose 2 - G.edgeFinset.card)

The sample mass of a constant graphon: every edge is present independently with probability p, so the mass of G is p^{e(G)} (1-p)^{\binom{k}{2} - e(G)}.

theorem Graphon.sampleLaw_const_eq_binomial {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (p : ↑(Set.Icc 0 1)) (k : ℕ) : ↑((constGraphon p).sampleLaw k) = SimpleGraph.binomialRandom (Fin k) p

The constant graphon samples the binomial random graph: the sample law of constGraphon p on k vertices is Mathlib's G(Fin k, p). The singleton mass formula SimpleGraph.binomialRandom_singleton is reused from Mathlib; the graphon-side computation is sampleMass_constGraphon.

@[simp]

theorem Graphon.sampleLaw_const_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : ↑((constGraphon 0).sampleLaw k) = MeasureTheory.Measure.dirac ⊥

At p = 0 the sample law is the point mass at the empty graph.

@[simp]

theorem Graphon.sampleLaw_const_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : ↑((constGraphon 1).sampleLaw k) = MeasureTheory.Measure.dirac ⊤

At p = 1 the sample law is the point mass at the complete graph.