-- Mathlib/Probability/StrongLaw.lean
theorem moment_truncation_eq_intervalIntegral (hf : AEStronglyMeasurable f μ) {A : ℝ} (hA : 0 ≤ A)
    {n : ℕ} (hn : n ≠ 0) : ∫ x, truncation f A x ^ n ∂μ = ∫ y in -A..A, y ^ n ∂Measure.map f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (x : α), (fun z => (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

Tactic:
rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le,
  ← integral_indicator M]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (y : ℝ), (Set.Ioc (-A) A).indicator id y ^ n ∂Measure.map f μ =
    ∫ (x : ℝ), (Set.Ioc (-A) A).indicator (fun x => x ^ n) x ∂Measure.map f μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z => (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

Tactic:
change ∫ x, (fun z => indicator (Set.Ioc (-A) A) id z ^ n) (f x) ∂μ = _

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (x : α), (fun z => (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (y : ℝ), (Set.Ioc (-A) A).indicator id y ^ n ∂Measure.map f μ =
    ∫ (x : ℝ), (Set.Ioc (-A) A).indicator (fun x => x ^ n) x ∂Measure.map f μ

Tactic:
simp only [indicator, zero_pow hn, id, ite_pow]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z => (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)

Tactic:
exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

Tactic:
have M : MeasurableSet (Set.Ioc (-A) A) := measurableSet_Ioc

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ