Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -1,5 +1,3 @@
-import LeanCamCombi.ExtrProbCombi.BernoulliSeq
-import LeanCamCombi.ExtrProbCombi.BinomialRandomGraph
 import LeanCamCombi.ExtrProbCombi.BollobasContainment
 import LeanCamCombi.ExtrProbCombi.Connectivity
 import LeanCamCombi.ExtrProbCombi.GiantComponent
@@ -12,6 +10,9 @@ import LeanCamCombi.GrowthInGroups.Lecture4
 import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
+import LeanCamCombi.Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
+import LeanCamCombi.Mathlib.Probability.Distributions.Bernoulli
+import LeanCamCombi.Mathlib.Probability.HasLaw
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.PlainCombi.KatonaCircle
 import LeanCamCombi.PlainCombi.LittlewoodOfford

LeanCamCombi/ExtrProbCombi/BernoulliSeq.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import LeanCamCombi.ExtrProbCombi.BinomialRandomGraph
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
+import LeanCamCombi.Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Combinatorics.SimpleGraph.Copy
 import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
@@ -16,25 +16,23 @@ This file proves Bollobás' lemma on graph containment.
 -/
 
 open Asymptotics Filter MeasureTheory
-open scoped MeasureTheory  ENNReal NNReal SimpleGraph Topology
-
-variable {α β Ω : Type*} [Fintype β] {G : ℕ → Ω → SimpleGraph α} (H : SimpleGraph β)
-  [Fintype H.edgeSet] [∀ n ω, DecidableRel (G n ω).Adj] [MeasurableSpace Ω] (μ : Measure Ω)
-  [IsProbabilityMeasure μ] {p : ℕ → ℝ≥0} (hG : ∀ n, IsBinomialRandomGraph (G n) (p n) μ)
+open scoped MeasureTheory  ENNReal NNReal SimpleGraph Topology unitInterval
 
 namespace SimpleGraph
+variable {V W Ω : Type*} [Fintype W] {G : ℕ → Ω → SimpleGraph V} (H : SimpleGraph W)
+  [Fintype H.edgeSet] [∀ n ω, DecidableRel (G n ω).Adj] [MeasurableSpace Ω] (μ : Measure Ω)
+  [IsProbabilityMeasure μ] {p : ℕ → I} (hG : ∀ n, IsBinomialRandom (G n) (p n) μ)
 
-/-- **Bollobás' Graph Containment Lemma, zero statement** -/
+/-- **Bollobás' Graph Containment Lemma**, zero statement -/
 lemma zero_statement
     (hp : (fun n ↦ p n : ℕ → ℝ) =o[atTop] (fun n ↦ n ^ (-H.maxEdgeSubdensity⁻¹ : ℝ) : ℕ → ℝ)) :
     Tendsto (fun n ↦ μ {ω | H ⊑ G n ω}) atTop (𝓝 0) :=
   sorry
 
-/-- **Bollobás' Graph Containment Lemma, one statement** -/
+/-- **Bollobás' Graph Containment Lemma**, one statement -/
 lemma one_statement
     (hp : (fun n ↦ n ^ (-H.maxEdgeSubdensity⁻¹ : ℝ) : ℕ → ℝ) =o[atTop] (fun n ↦ p n : ℕ → ℝ)) :
     Tendsto (fun n ↦ μ {ω | H ⊑ G n ω}) atTop (𝓝 1) :=
   sorry
 
 end SimpleGraph
-  

LeanCamCombi/ExtrProbCombi/BinomialRandomGraph.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import LeanCamCombi.ExtrProbCombi.BinomialRandomGraph
+import LeanCamCombi.Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
 
 /-!
 # Connectivity of the Erdős–Rényi model

LeanCamCombi/ExtrProbCombi/BollobasContainment.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import LeanCamCombi.ExtrProbCombi.BinomialRandomGraph
+import LeanCamCombi.Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
 
 /-!
 # The giant component