Theorem: expected_degree (RandomGraphs/degree.lean)

State before:
V : Type
Ω : Type u_3
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
p : NNReal
hp : p ≤ 1
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
x✝ : Sort u_1
Degree : x✝
h : sorryAx (Sort u_2) true
v : V
⊢ ∫ (ω : Ω), sorryAx ℝ true ∂μ = (↑(Fintype.card V) - 1) * ↑p
Tactic:
sorry
State after:
no goals