Bollobás' graph containment lemma

This file proves Bollobás' lemma on graph containment.

theorem SimpleGraph.zero_statement {V : Type u_1} {W : Type u_2} {Ω : Type u_3} [Fintype W] {G : ℕ → Ω → SimpleGraph V} (H : SimpleGraph W) [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {p : ℕ → ↑unitInterval} (hH : H.edgeSet.Finite) (hp : (fun (n : ℕ) => ↑(p n)) =o[Filter.atTop] fun (n : ℕ) => ↑n ^ (-↑H.maxEdgeSubdensity⁻¹)) : Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | H.IsContained (G n ω)}) Filter.atTop (nhds 0)

Bollobás' Graph Containment Lemma, zero statement

theorem SimpleGraph.one_statement {V : Type u_1} {W : Type u_2} {Ω : Type u_3} [Fintype W] {G : ℕ → Ω → SimpleGraph V} (H : SimpleGraph W) [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {p : ℕ → ↑unitInterval} (hH : H.edgeSet.Finite) (hp : (fun (n : ℕ) => ↑n ^ (-↑H.maxEdgeSubdensity⁻¹)) =o[Filter.atTop] fun (n : ℕ) => ↑(p n)) : Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | H.IsContained (G n ω)}) Filter.atTop (nhds 1)

Bollobás' Graph Containment Lemma, one statement