-- Mathlib/Probability/Variance.lean
theorem meas_ge_le_evariance_div_sq {X : Ω → ℝ} (hX : AEStronglyMeasurable X μ) {c : ℝ≥0}
    (hc : c ≠ 0) : μ {ω | ↑c ≤ |X ω - μ[X]|} ≤ evariance X μ / c ^ 2

Proof state:
case h.e'_4.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] = ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Tactic:
simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two,
  ENNReal.rpow_one, evariance]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
⊢ ↑c ≠ 0

Tactic:
rwa [Ne, ENNReal.coe_eq_zero]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ↑c ^ 2

Tactic:
convert meas_ge_le_mul_pow_eLpNorm μ two_ne_zero ENNReal.ofNat_ne_top (hX.sub B) A using 1

Result:
case h.e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {x | ↑c ≤ ↑‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖₊}

case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun x => ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2

Proof state:
case h.e'_3.h.e_6.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = {x | ↑c ≤ ↑‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖₊}

Tactic:
simp only [Pi.sub_apply, ENNReal.coe_le_coe, ← Real.norm_eq_abs, ← coe_nnnorm,
  NNReal.coe_le_coe, ENNReal.ofReal_coe_nnreal]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ ↑(c ^ 2) = ↑c ^ 2

Tactic:
norm_cast

Result:
no goals

Proof state:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 =
    (↑c)⁻¹ ^ ENNReal.toReal 2 *
      ((∫⁻ (x : Ω), ‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^
        ENNReal.toReal 2

Tactic:
simp only [show ENNReal.ofNNReal (c ^ 2) = (ENNReal.ofNNReal c) ^ 2 by norm_cast,
  ENNReal.toReal_ofNat, one_div, Pi.sub_apply]

Result:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Proof state:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Tactic:
rw [div_eq_mul_inv, ENNReal.inv_pow, mul_comm, ENNReal.rpow_two]

Result:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ (↑c)⁻¹ ^ 2 * eVar[X; μ] = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ↑c ^ 2

Tactic:
have B : AEStronglyMeasurable (fun _ : Ω => μ[X]) μ := aestronglyMeasurable_const

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ↑c ^ 2

Proof state:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ (↑c)⁻¹ ^ 2 * eVar[X; μ] = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Tactic:
congr

Result:
case h.e'_4.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] = ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Proof state:
case h.e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {x | ↑c ≤ ↑‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖₊}

Tactic:
congr

Result:
case h.e'_3.h.e_6.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = {x | ↑c ≤ ↑‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖₊}

Proof state:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun x => ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top]

Result:
case h.e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 =
    (↑c)⁻¹ ^ ENNReal.toReal 2 *
      ((∫⁻ (x : Ω), ‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^
        ENNReal.toReal 2

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ↑c ^ 2

Tactic:
have A : (c : ℝ≥0∞) ≠ 0 := by rwa [Ne, ENNReal.coe_eq_zero]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ↑c ^ 2