Generic i.i.d. random sources for samplers (directed umbrella #84, shared infrastructure)

The reusable i.i.d. product sources underlying the explicit graph and digraph samplers, phrased generically (no graph/digraph-specific index types) so the directed sampler need not duplicate the InfiniteGraph-namespaced infrastructure:

• OffDiagPairIndex V — the generic off-diagonal unordered-pair index (one uniform per pair of distinct vertices); InfiniteGraph.EdgeIndex is definitionally OffDiagPairIndex ℕ;
• uniform01 — the uniform probability measure on [0,1], with uniform01_Iic giving the mass of an initial segment, and measurable_decideLe the measurability of thresholding at 1/2;
• iidVertexSource μ — i.i.d. positions ℕ → α with law μ (via Measure.infinitePi);
• iidUniformSource ι — i.i.d. uniforms on [0,1] indexed by an arbitrary type ι;
• Measure.infinitePi_map_comp_equiv — invariance/reindexing under an index equivalence;
• Measure.infinitePi_map_sumPiEquivProdPi — the product decomposition over a sum of possibly infinite index types;
• Measure.infinitePi_map_comp_of_injective — the finite-projection identity: pushing an infinite product forward along precomposition with an injection from a finite index type gives the finite product of the selected factors (the marginal computations of both samplers).

The undirected graph sampler (Graphon.InfiniteSampler) and the directed digraph sampler both draw one vertex position per vertex (iidVertexSource) and one [0,1]-uniform per unordered pair (iidUniformSource (OffDiagPairIndex ℕ)); the categorical-vs-Bernoulli distinction is downstream of the sources.

The off-diagonal unordered-pair index

@[reducible, inline]

abbrev OffDiagPairIndex (V : Type u_1) : Type u_1

The off-diagonal unordered-pair index over a vertex type V: an unordered pair of distinct vertices. The samplers draw one [0,1]-uniform per such pair (loops are separate).

Equations

• OffDiagPairIndex V = { e : Sym2 V // ¬e.IsDiag }

def OffDiagPairIndex.mk {V : Type u_1} {i j : V} (h : i ≠ j) : OffDiagPairIndex V

The off-diagonal pair index on two distinct vertices.

Equations

• OffDiagPairIndex.mk h = ⟨s(i, j), ⋯⟩

@[simp]

theorem OffDiagPairIndex.mk_val {V : Type u_1} {i j : V} (h : i ≠ j) : ↑(mk h) = s(i, j)

@[simp]

theorem OffDiagPairIndex.mk_symm {V : Type u_1} {i j : V} (h : i ≠ j) : mk ⋯ = mk h

The pair index is symmetric in its two vertices.

@[simp]

theorem OffDiagPairIndex.mk_eq_mk {V : Type u_1} {i j i' j' : V} {h : i ≠ j} {h' : i' ≠ j'} : mk h = mk h' ↔ i = i' ∧ j = j' ∨ i = j' ∧ j = i'

Injectivity of the pair index on unordered pairs: two pair indices agree exactly when the underlying vertex pairs agree up to order.

noncomputable def MeasureTheory.uniform01 : Measure ℝ

The uniform distribution on [0,1].

Equations

• MeasureTheory.uniform01 = MeasureTheory.volume.restrict (Set.Icc 0 1)

instance MeasureTheory.instIsProbabilityMeasureRealUniform01 : IsProbabilityMeasure uniform01

theorem MeasureTheory.measurable_decideLe {X : Type u_1} [MeasurableSpace X] {f : X → ℝ} (hf : Measurable f) : Measurable fun (x : X) => decide (f x ≤ 1 / 2)

Thresholding a measurable real at 1/2 is measurable.

theorem MeasureTheory.uniform01_Iic {c : ℝ} (hc : c ∈ Set.Icc 0 1) : uniform01 (Set.Iic c) = ENNReal.ofReal c

The lower-interval mass of the uniform distribution on [0,1].

noncomputable def MeasureTheory.iidVertexSource {α : Type u_1} [MeasurableSpace α] (μ : Measure α) : Measure (ℕ → α)

The vertex source: i.i.d. positions ℕ → α with law μ.

Equations

• MeasureTheory.iidVertexSource μ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ

instance MeasureTheory.instIsProbabilityMeasureForallNatIidVertexSource {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ] : IsProbabilityMeasure (iidVertexSource μ)

noncomputable def MeasureTheory.iidUniformSource (ι : Type u_1) : Measure (ι → ℝ)

The uniform source: i.i.d. uniforms on [0,1], one per index i : ι.

Equations

• MeasureTheory.iidUniformSource ι = MeasureTheory.Measure.infinitePi fun (x : ι) => MeasureTheory.uniform01

instance MeasureTheory.instIsProbabilityMeasureForallRealIidUniformSource (ι : Type u_1) : IsProbabilityMeasure (iidUniformSource ι)

Reindexing invariance of infinite product sources

theorem MeasureTheory.Measure.infinitePi_map_comp_equiv {ι : Type u_1} {α : Type u_2} {γ : Type u_3} [MeasurableSpace γ] (ν : ι → Measure γ) [∀ (i : ι), IsProbabilityMeasure (ν i)] (e : α ≃ ι) : map (fun (x : ι → γ) (a : α) => x (e a)) (infinitePi ν) = infinitePi fun (a : α) => ν (e a)

Precomposition with an index equivalence reindexes an infinite product source: pushing an infinite product of probability measures forward along precomposition with an equivalence of index types gives the reindexed infinite product — the Equiv form of Measure.infinitePi_map_piCongrLeft, and the source-invariance engine of the evaluated-law exchangeability.

theorem MeasureTheory.Measure.infinitePi_map_sumPiEquivProdPi {ι : Type u_1} {ι' : Type u_2} {γ : Type u_3} [MeasurableSpace γ] (ν : ι ⊕ ι' → Measure γ) [∀ (i : ι ⊕ ι'), IsProbabilityMeasure (ν i)] : map (⇑(MeasurableEquiv.sumPiEquivProdPi fun (x : ι ⊕ ι') => γ)) (infinitePi ν) = (infinitePi fun (i : ι) => ν (Sum.inl i)).prod (infinitePi fun (i : ι') => ν (Sum.inr i))

Splitting an infinite product over a sum of index types gives a product of infinite products. This is the possibly-infinite counterpart of measurePreserving_sumPiEquivProdPi, whose statement is for finite Measure.pi.

Finite projections of infinite product sources

theorem MeasureTheory.Measure.infinitePi_map_comp_of_injective {ι : Type u_1} {δ : Type u_2} {γ : Type u_3} [MeasurableSpace γ] (ν : ι → Measure γ) [∀ (i : ι), IsProbabilityMeasure (ν i)] [Fintype δ] {f : δ → ι} (hf : Function.Injective f) : map (fun (x : ι → γ) (d : δ) => x (f d)) (infinitePi ν) = Measure.pi fun (d : δ) => ν (f d)

Pushing an infinite product of probability measures forward along precomposition with an injection from a finite index type gives the finite product of the selected factors — Measure.infinitePi_map_restrict for an arbitrary injection (constant-fiber form; Mathlib upstreaming candidate, issue #24).

theorem MeasureTheory.Measure.infinitePi_map_prodMk_of_disjoint {ι : Type u_1} {δ₁ : Type u_2} {δ₂ : Type u_3} {γ : Type u_4} [MeasurableSpace γ] (ν : ι → Measure γ) [∀ (i : ι), IsProbabilityMeasure (ν i)] [Fintype δ₁] [Fintype δ₂] {f : δ₁ → ι} {g : δ₂ → ι} (hf : Function.Injective f) (hg : Function.Injective g) (hd : ∀ (a : δ₁) (b : δ₂), f a ≠ g b) : map (fun (x : ι → γ) => (fun (a : δ₁) => x (f a), fun (b : δ₂) => x (g b))) (infinitePi ν) = (Measure.pi fun (a : δ₁) => ν (f a)).prod (Measure.pi fun (b : δ₂) => ν (g b))

Disjoint finite projections of an infinite product source are independent (product form): pushing an infinite product of probability measures forward along a pair of precompositions with injections from finite index types with disjoint ranges gives the product of the two finite products — the factorization behind dissociation of sampler pushforwards.