-- Mathlib/Probability/StrongLaw.lean
theorem sum_variance_truncation_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) (K : ℕ) :
    ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[truncation X j ^ 2] ≤ 2 * 𝔼[X]

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0 ..↑j, x ^ 2 ∂ρ =
    ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
congr 1 with j

Result:
case e_f.h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
j : ℕ
⊢ (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0 ..↑j, x ^ 2 ∂ρ = (↑j ^ 2)⁻¹ * ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Proof state:
case e_f.h.e_a
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
j : ℕ
⊢ ∫ (x : ℝ) in 0 ..↑j, x ^ 2 ∂ρ = ∫ (x : ℝ) in ↑0 ..↑j, x ^ 2 ∂ρ

Tactic:
norm_cast

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (Y j ^ 2) a = ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0 ..↑j, x ^ 2 ∂ρ

Tactic:
simp_rw [Y2]

Result:
no goals

Proof state:
case refine_2.hf
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ Continuous (HMul.hMul 2)

Tactic:
exact continuous_const.mul continuous_id'

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤
    ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
apply sum_le_sum fun k _ => ?_

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k ∈ range K
⊢ (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ =
    ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
simp_rw [mul_sum, sum_mul, sum_sigma']

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ ∑ x ∈ (range K).sigma range, (↑x.fst ^ 2)⁻¹ * ∫ (x : ℝ) in ↑x.snd..↑(x.snd + 1), x ^ 2 ∂ρ =
    ∑ x ∈ (range K).sigma fun a => Ioo a K, (↑x.snd ^ 2)⁻¹ * ∫ (x : ℝ) in ↑x.fst..↑(x.fst + 1), x ^ 2 ∂ρ

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a

Tactic:
let ρ : Measure ℝ := Measure.map X ℙ

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ 2 * ∫ (x : ℝ) in ↑0 ..↑K, x ∂ρ = 2 * ∫ (x : ℝ) in 0 ..↑K, x ∂ρ

Tactic:
norm_cast

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ 1 * (2 * x) = 2 * x

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (a : Ω), (fun x => Y n x ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ

Tactic:
rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ

Tactic:
change 𝔼[fun x => Y n x ^ 2] = _

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (a : Ω), (fun x => Y n x ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ