The Erdős–Rényi model #
In this file, we define the Erdős–Rényi model through its marginals.
@[reducible, inline]
abbrev
ErdosRenyi
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
(G : Ω → SimpleGraph α)
(p : NNReal)
(μ : MeasureTheory.Measure Ω := by volume_tac)
:
A sequence iid. real valued Bernoulli random variables with parameter p ≤ 1.
Equations
- ErdosRenyi G p μ = ProbabilityTheory.IsBernoulliSeq (fun (ω : Ω) => (G ω).edgeSet) p μ
Instances For
theorem
ErdosRenyi.le_one
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
:
p ≤ 1
theorem
ErdosRenyi.iIndepFun
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
:
ProbabilityTheory.iIndepFun inferInstance (fun (e : Sym2 α) (ω : Ω) => e ∈ (G ω).edgeSet) μ
theorem
ErdosRenyi.map
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
(e : Sym2 α)
:
MeasureTheory.Measure.map (fun (ω : Ω) => e ∈ (G ω).edgeSet) μ = (PMF.bernoulli' p ⋯).toMeasure
theorem
ErdosRenyi.aemeasurable
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
(e : Sym2 α)
:
AEMeasurable (fun (ω : Ω) => e ∈ (G ω).edgeSet) μ
theorem
ErdosRenyi.nullMeasurableSet
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
(e : Sym2 α)
:
MeasureTheory.NullMeasurableSet {ω : Ω | e ∈ (G ω).edgeSet} μ
theorem
ErdosRenyi.identDistrib
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
(d e : Sym2 α)
:
ProbabilityTheory.IdentDistrib (fun (ω : Ω) => d ∈ (G ω).edgeSet) (fun (ω : Ω) => e ∈ (G ω).edgeSet) μ μ
theorem
ErdosRenyi.meas_edge
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
(e : Sym2 α)
:
theorem
ErdosRenyi.meas
{α : Type u_1}
{Ω : Type u_2}
[MeasurableSpace Ω]
{G : Ω → SimpleGraph α}
{H : SimpleGraph α}
{p : NNReal}
(μ : MeasureTheory.Measure Ω)
(hG : ErdosRenyi G p μ)
[MeasureTheory.IsProbabilityMeasure μ]
[Fintype α]
[DecidableEq α]
[DecidableRel H.Adj]
: