Theorem: Probly.dflip.density_wrt_flip (Probly/Flip.lean)

State before:
θ : ℝ
⊢ DRand.density dflip ↑(flip θ).μ = fun b => if b = true then 1 / θ else 1 / (θ - 1)
Tactic:
sorry
State after:
no goals