English
A bound on the weighted sum of variances of truncations by the original expectation of X.
Русский
Ограничение на взвешенную сумму дисперсий усечений через E[X].
LaTeX
$$$\sum_{j=0}^{K-1} \frac{1}{(j\!:\!\mathbb{R})^2} \mathbb{E}[\operatorname{truncation}(X,j)^2] \le 2 \mathbb{E}[X]$$$
Lean4
theorem sum_variance_truncation_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) (K : ℕ) :
∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[truncation X j ^ 2] ≤ 2 * 𝔼[X] :=
by
set Y := fun n : ℕ => truncation X n
let ρ : Measure ℝ := Measure.map X ℙ
have Y2 : ∀ n, 𝔼[Y n ^ 2] = ∫ x in 0..n, x ^ 2 ∂ρ := by
intro n
change 𝔼[fun x => Y n x ^ 2] = _
rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]
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 only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_one]
· 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
exact continuous_const.mul (continuous_pow 2)
· apply Continuous.integrableOn_Ioc
exact continuous_const.mul continuous_id'
·
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
