Theorem: degree_distribution (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
k : ℕ
⊢ ↑↑μ {ω | sorryAx ℕ true = k} = ↑(p ^ k) * ↑(p ^ (Fintype.card V - 1 - k)) * ↑(Nat.choose (Fintype.card V - 1) k)
Tactic:
sorry
State after:
no goals