Theorem: expected_edge_count (RandomGraphs/erdos_renyi.lean)

State before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∫ (ω : Ω), ↑(NumEdges G (_ : ∀ (e : EdgeType V) (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) e) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p
Tactic:
simp only [NumEdges, SimpleFunc.coe_sum, Finset.sum_apply]
State after:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∫ (ω : Ω), ∑ c : EdgeType V, ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) c) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p

State before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∫ (ω : Ω), ∑ c : EdgeType V, ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) c) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p
Tactic:
rw [integral_finset_sum]
State after:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∑ i : EdgeType V, ∫ (a : Ω), ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) a ∂μ =
    ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω

State before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∑ i : EdgeType V, ∫ (a : Ω), ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) a ∂μ =
    ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Tactic:
simp only [bernoulli_expectation (h.bernoulli_edges), Finset.sum_const, Finset.card_univ, Fintype.card, nsmul_eq_mul]
State after:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ↑(Fintype.card (EdgeType V)) * ↑p = ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω

State before:
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ↑(Fintype.card (EdgeType V)) * ↑p = ↑(Nat.choose n 2) * ↑p

case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Tactic:
rw [Sym2.card_subtype_not_diag, hn]
State after:
case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω

State before:
case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
Tactic:
simp only [Finset.mem_univ, integrable, forall_true_left, Subtype.forall, implies_true]
State after:
no goals