-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j :
  Eq (α := ℝ)
    (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y j) 2 a)
    (∑ j ∈ range K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * ∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j₁ :
  Eq (α := ℝ)
    (∑ j ∈ range K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * ∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        ∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j₂ :
  Eq (α := ℝ)
    (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        ∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range K,
      HMul.hMul (α := ℝ) (∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹)
        (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ))
j₃ :
  LE.le (α := ℝ)
    (∑ k ∈ range K,
      HMul.hMul (α := ℝ) (∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹)
        (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ))
    (∑ k ∈ range K,
      2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j₄ :
  LE.le (α := ℝ)
    (∑ k ∈ range K,
      2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range K, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ)
j₅ :
  ∑ k ∈ range K, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)
⊢ (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          HPow.hPow (β := ℕ) (truncation X (↑j : ℝ)) 2 a) ≤
    HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a)

Tactic:
calc
    ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[Y j ^ 2] =
        ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * ∫ x in 0..j, x ^ 2 ∂ρ := by simp_rw [Y2]
    _ = ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * ∑ k ∈ range j, ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
      congr 1 with j
      congr 1
      rw [intervalIntegral.sum_integral_adjacent_intervals]
      · norm_cast
      intro k _
      exact (continuous_id.pow _).intervalIntegrable _ _
    _ = ∑ k ∈ range K, (∑ j ∈ Ioo k K, ((j : ℝ) ^ 2)⁻¹) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
      simp_rw [mul_sum, sum_mul, sum_sigma']
      refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
        aesop (add unsafe lt_trans)
    _ ≤ ∑ k ∈ range K, 2 / (k + 1 : ℝ) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
      gcongr with k
      · refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _
        simp
      · apply sum_Ioo_inv_sq_le
    _ ≤ ∑ k ∈ range K, ∫ x in k..(k + 1 : ℕ), 2 * x ∂ρ := by
      gcongr with k
      have Ik : (k : ℝ) ≤ (k + 1 : ℕ) := by simp
      rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]
      refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · calc
          2 / (↑k + 1) * x ^ 2 = x / (k + 1) * (2 * x) := by ring
          _ ≤ 1 * (2 * x) := by
              have : 0 < x := k.cast_nonneg.trans_lt hx.1
              gcongr
              exact (div_le_one <| by positivity).2 <| mod_cast hx.2
          _ = 2 * x := by rw [one_mul]
    _ = 2 * ∫ x in (0 : ℝ)..K, x ∂ρ := by
      rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
      swap; · exact (continuous_const.mul continuous_id').intervalIntegrable _ _
      rw [intervalIntegral.integral_const_mul]
      norm_cast
    _ ≤ 2 * 𝔼[X] := mul_le_mul_of_nonneg_left (by
      rw [← integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]
      exact integral_truncation_le_integral_of_nonneg hint hnonneg) zero_le_two

Premises used: Finset.range, zero_le_two, OfNat.ofNat, mul_le_mul_of_nonneg_left