-- Mathlib/Probability/Moments/Basic.lean
theorem centralMoment_one [IsZeroOrProbabilityMeasure μ] : centralMoment X 1 μ = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
h_add : X = (fun x => X x - integral μ X) + fun x => integral μ X
⊢ Integrable X μ

Tactic:
rw [h_add]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
h_add : X = (fun x => X x - integral μ X) + fun x => integral μ X
⊢ Integrable ((fun x => X x - integral μ X) + fun x => integral μ X) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
⊢ Integrable X μ

Tactic:
have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
h_add : X = (fun x => X x - integral μ X) + fun x => integral μ X
⊢ Integrable X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
⊢ centralMoment X 1 0 = 0

case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
h_add : X = (fun x => X x - integral μ X) + fun x => integral μ X
⊢ Integrable ((fun x => X x - integral μ X) + fun x => integral μ X) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0

Tactic:
have : ¬Integrable (fun x => X x - integral μ X) μ := by
  refine fun h_sub => h_int ?_
  have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp
  rw [h_add]
  fun_prop

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
this : ¬Integrable (fun x => X x - integral μ X) μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ¬Integrable (fun x => X x - integral μ X) μ

Tactic:
refine fun h_sub => h_int ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
⊢ Integrable X μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ = 0

Tactic:
simp only [measure_univ, ENNReal.one_toReal, sub_self, zero_mul]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
⊢ X = (fun x => X x - integral μ X) + fun x => integral μ X

Tactic:
ext1 x

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
x : Ω
⊢ X x = ((fun x => X x - integral μ X) + fun x => integral μ X) x

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
⊢ centralMoment X 1 0 = 0

Tactic:
simp [centralMoment]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = 0

Tactic:
rw [centralMoment_one' h_int]

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ = 0

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x => X x - integral μ X) μ
x : Ω
⊢ X x = ((fun x => X x - integral μ X) + fun x => integral μ X) x

Tactic:
simp

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
this : ¬Integrable (fun x => X x - integral μ X) μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0

Tactic:
rw [integral_undef this]

Result:
no goals

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0

Tactic:
by_cases h_int : Integrable X μ

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = 0

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0