-- Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
theorem integral_eq_tsum (p : PMF α) (f : α → E) (hf : Integrable f p.toMeasure) :
    ∫ a, f a ∂(p.toMeasure) = ∑' a, (p a).toReal • f a := calc
  _ = ∫ a in p.support, f a ∂(p.toMeasure)

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α), f a ∂p.toMeasure = ∫ (a : α) in p.support, f a ∂p.toMeasure

Tactic:
rw [restrict_toMeasure_support p]

Result:
no goals

Proof state:
case e_f.h.e_a.e_a
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : ↑p.support
⊢ p.toMeasure {↑x} = p ↑x

Tactic:
apply PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ IntegrableOn f p.support p.toMeasure

Tactic:
rwa [IntegrableOn, restrict_toMeasure_support p]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : α
h1 : x ∈ Function.support fun a => (p a).toReal
h2 : p x = 0
⊢ (fun a => (p a).toReal) x = 0

Tactic:
simp [h2]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α) in p.support, f a ∂p.toMeasure = ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a

Tactic:
apply integral_countable f p.support_countable

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ IntegrableOn f p.support p.toMeasure

Proof state:
case e_f.h
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : ↑p.support
⊢ (p.toMeasure {↑x}).toReal • f ↑x = (p ↑x).toReal • f ↑x

Tactic:
congr 2

Result:
case e_f.h.e_a.e_a
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : ↑p.support
⊢ p.toMeasure {↑x} = p ↑x

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a = ∑' (a : ↑p.support), (p ↑a).toReal • f ↑a

Tactic:
congr with x

Result:
case e_f.h
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : ↑p.support
⊢ (p.toMeasure {↑x}).toReal • f ↑x = (p ↑x).toReal • f ↑x