-- 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 ∂ρ
k : ℕ
x✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ ∫ (x : ℝ) in Set.Ioc ↑k ↑(k + 1), 2 / (↑k + 1) * x ^ 2 ∂ρ ≤ ∫ (x : ℝ) in Set.Ioc ↑k ↑(k + 1), 2 * x ∂ρ

Tactic:
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_

Result:
case refine_1
Ω : 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)
⊢ IntegrableOn (fun x => 2 / (↑k + 1) * x ^ 2) (Set.Ioc ↑k ↑(k + 1)) ρ

case refine_2
Ω : 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)
⊢ IntegrableOn (HMul.hMul 2) (Set.Ioc ↑k ↑(k + 1)) ρ

case refine_3
Ω : 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)
⊢ 2 / (↑k + 1) * x ^ 2 ≤ 2 * x

Proof state:
case h.e'_3.h.e'_6
Ω : 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)
⊢ ↑k + 1 = ↑(k + 1)

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 ∂ρ
⊢ ∫ (x : Ω), truncation X (↑K) x ≤ ∫ (a : Ω), X a

Tactic:
exact integral_truncation_le_integral_of_nonneg hint 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 ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
⊢ ∫ (x : ℝ) in ↑0 ..↑K, 2 * x ∂ρ = 2 * ∫ (x : ℝ) in 0 ..↑K, x ∂ρ

Ω : 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 < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

Tactic:
swap

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 < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

Ω : 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 : ℝ) in ↑0 ..↑K, 2 * x ∂ρ = 2 * ∫ (x : ℝ) in 0 ..↑K, 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 ℙ
⊢ ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ

Tactic:
intro n

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 : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, 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 : ℕ
⊢ ∀ k < j, IntervalIntegrable (fun x => x ^ 2) ρ ↑k ↑(k + 1)

Tactic:
intro k _

Result:
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 k : ℕ
a✝ : k < j
⊢ IntervalIntegrable (fun x => x ^ 2) ρ ↑k ↑(k + 1)

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 ∂ρ
⊢ ∫ (x : ℝ) in 0 ..↑K, x ∂ρ ≤ ∫ (a : Ω), X a

Tactic:
rw [← integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]

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 : Ω), truncation X (↑K) x ≤ ∫ (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 ∂ρ
k : ℕ
x✝ : k < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

Tactic:
exact (continuous_const.mul continuous_id').intervalIntegrable _ _

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)
⊢ 0 < ↑(k + 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one]

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
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ 0 < ↑k + 1