Almost-sure convergence of the sampled empirical graphons (issue #71)

The empirical graphons of an explicit W-random infinite graph converge to the class of W almost surely — the pathwise strengthening of the convergence in probability of Graphon/InfiniteSamplingConvergence.lean (issue #57), via Route A of issue #71 (coordinatewise hom-density concentration, Lovász Prop 11.32):

• InfiniteGraph.ae_tendsto_homDensity_restrictFin — per-coordinate Borel–Cantelli: for each fixed finite graph F, the summability bridge InfiniteGraph.tsum_samplerSource_homDensity_tail_ne_top (issue #72, item 1) at each tolerance 1/(m+1) feeds MeasureTheory.ae_eventually_notMem, so almost surely the hom-densities of the initial restrictions converge to t(F, W);
• InfiniteGraph.sampledEmpiricalGraphon_tendsto_ae — almost-sure convergence: intersecting over the countable family Σ q, SimpleGraph (Fin q) gives a full-measure set on which every hom-density converges; the convergence equivalence Graphon.cutDistance_tendsto_iff_homDensity_tendsto (the counting/inverse-counting characterization) upgrades this pathwise to cut-distance convergence, hence to convergence in the graphon space via GraphonSpace.dist_mk.

theorem InfiniteGraph.ae_tendsto_homDensity_restrictFin {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] : ∀ᵐ (ω : (ℕ → α) × (EdgeIndex → ℝ)) ∂samplerSource μ, Filter.Tendsto (fun (n : ℕ) => Graphon.homDensity F (Graphon.ofSimpleGraphOn (restrictFin (n + 1) (sampleInfinite W ω)))) Filter.atTop (nhds (Graphon.homDensity F W))

Per-coordinate Borel–Cantelli (issue #71, Route A, steps 1–3): for each fixed finite graph F, almost every sampled infinite graph has the hom-densities of its initial restrictions converging to t(F, W) — the deviation events at tolerance 1/(m+1) have summable probabilities by the concentration tail of issue #72, item 1.

theorem InfiniteGraph.sampledEmpiricalGraphon_tendsto_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : ∀ᵐ (ω : (ℕ → α) × (EdgeIndex → ℝ)) ∂samplerSource μ, Filter.Tendsto (fun (n : ℕ) => sampledEmpiricalGraphon W n ω) Filter.atTop (nhds (GraphonSpace.mk W))

Almost-sure convergence of the sampled empirical graphons (issue #71, part 2): almost every W-random infinite graph has its empirical graphons converging to the class of W in the graphon space. Route A: intersect the per-coordinate Borel–Cantelli over the countable family of finite graphs, then upgrade pathwise via the convergence equivalence (counting + inverse counting).