Theorem: SciLean.Rand.flip.integral (SciLean/Core/Rand/Distributions/Flip.lean)

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ ∫' x, f x ∂(flip θ).ℙ = θ • f true + (1 - θ) • f false
Tactic:
simp [rand_simp,flip.measure]
State after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ ∫' x,
      f
        x ∂(ENNReal.ofReal (Scalar.toReal R θ) • Measure.dirac true +
        ENNReal.ofReal (Scalar.toReal R (1 - θ)) • Measure.dirac false) =
    θ • f true + (1 - θ) • f false

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ ∫' x,
      f
        x ∂(ENNReal.ofReal (Scalar.toReal R θ) • Measure.dirac true +
        ENNReal.ofReal (Scalar.toReal R (1 - θ)) • Measure.dirac false) =
    θ • f true + (1 - θ) • f false
Tactic:
sorry_proof
State after:
no goals