Bridges from the finite subgraph densities to the empirical-graphon formulas (#94, PR 1)

The analytic half of the t/t_inj/t_ind interlude: on the equipartition step graphon of a finite host H, the homomorphism density is SimpleGraph.t and the sampling mass is the normalized exact-pullback count. Split from Graphon.SubgraphDensities so the pure density API keeps a combinatorics-only import closure. PR 2 of #94 adds the collision-comparison forms: the analytic homomorphism density is within k²/n of t_inj, and the sampling mass within k²/n of t_ind — the quantitative content of "sampling ≈ injective sampling".

theorem Graphon.homDensity_ofSimpleGraphOn_eq_t {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {n : ℕ} [NeZero n] (H : SimpleGraph (Fin n)) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : homDensity F (ofSimpleGraphOn H) = F.t H

The homomorphism density of the empirical graphon is t: on the equipartition step graphon of H, the analytic homomorphism density coincides with the combinatorial density.

theorem Graphon.sampleMass_ofSimpleGraphOn_eq_pullbackCount_div {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {n : ℕ} [NeZero n] (H : SimpleGraph (Fin n)) {k : ℕ} (G : SimpleGraph (Fin k)) : (ofSimpleGraphOn H).sampleMass G = ↑(G.pullbackCount H) / ↑n ^ k

The sampling mass of the empirical graphon is the normalized exact-pullback count: the probability that the k-sample of the empirical graphon of H equals G is the proportion of all vertex maps pulling H back to exactly G.

theorem Graphon.abs_homDensity_ofSimpleGraphOn_sub_tInj_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {n : ℕ} [NeZero n] (H : SimpleGraph (Fin n)) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : |homDensity F (ofSimpleGraphOn H) - F.tInj H| ≤ ↑k ^ 2 / ↑n

The analytic collision comparison: the homomorphism density of the empirical graphon is within k²/n of the injective density of the host.

theorem Graphon.abs_sampleMass_ofSimpleGraphOn_sub_tInd_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {n : ℕ} [NeZero n] (H : SimpleGraph (Fin n)) {k : ℕ} (G : SimpleGraph (Fin k)) : |(ofSimpleGraphOn H).sampleMass G - G.tInd H| ≤ ↑k ^ 2 / ↑n

The sampling collision comparison: the sampling mass of the empirical graphon is within k²/n of the induced density of the host.