English
Bound on the sum of probabilities that X lies in Ioc(j,N) by a finite expectation-based bound.
Русский
Суммарная вероятность того, что X лежит в Ioc(j,N), ограничена конечной границей, зависящей от E[X].
LaTeX
$$$\sum_{j=0}^{K-1} \mathbb{P}(X \in \mathrm{Ioc}(j,N)) \le \mathrm{ENNReal.ofReal}(\mathbb{E}[X] + 1)$$$
Lean4
theorem sum_prob_mem_Ioc_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) {K : ℕ} {N : ℕ} (hKN : K ≤ N) :
∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} ≤ ENNReal.ofReal (𝔼[X] + 1) :=
by
let ρ : Measure ℝ := Measure.map X ℙ
haveI : IsProbabilityMeasure ρ := Measure.isProbabilityMeasure_map hint.aemeasurable
have A : ∑ j ∈ range K, ∫ _ in j..N, (1 : ℝ) ∂ρ ≤ 𝔼[X] + 1 :=
calc
∑ j ∈ range K, ∫ _ in j..N, (1 : ℝ) ∂ρ = ∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ :=
by
apply sum_congr rfl fun j hj => ?_
rw [intervalIntegral.sum_integral_adjacent_intervals_Ico ((mem_range.1 hj).le.trans hKN)]
intro k _
exact continuous_const.intervalIntegrable _ _
_ = ∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ :=
by
simp_rw [sum_sigma']
refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_ <;> aesop (add simp Nat.lt_succ_iff)
_ ≤ ∑ i ∈ range N, (i + 1) * ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ :=
by
gcongr with i
simp only [Nat.cast_add, Nat.cast_one, sum_const, card_range, nsmul_eq_mul, Nat.cast_min]
refine mul_le_mul_of_nonneg_right (min_le_left _ _) ?_
apply intervalIntegral.integral_nonneg
· simp only [le_add_iff_nonneg_right, zero_le_one]
· simp only [zero_le_one, imp_true_iff]
_ ≤ ∑ i ∈ range N, ∫ x in i..(i + 1 : ℕ), x + 1 ∂ρ :=
by
gcongr with i
have I : (i : ℝ) ≤ (i + 1 : ℕ) := by
simp only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_one]
simp_rw [intervalIntegral.integral_of_le I, ← integral_const_mul]
apply setIntegral_mono_on
· exact continuous_const.integrableOn_Ioc
· exact (continuous_id.add continuous_const).integrableOn_Ioc
· exact measurableSet_Ioc
· intro x hx
simp only [Nat.cast_add, Nat.cast_one, Set.mem_Ioc] at hx
simp [hx.1.le]
_ = ∫ x in 0..N, x + 1 ∂ρ :=
by
rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
· norm_cast
· exact (continuous_id.add continuous_const).intervalIntegrable _ _
_ = ∫ x in 0..N, x ∂ρ + ∫ x in 0..N, 1 ∂ρ :=
by
rw [intervalIntegral.integral_add]
· exact continuous_id.intervalIntegrable _ _
· exact continuous_const.intervalIntegrable _ _
_ = 𝔼[truncation X N] + ∫ x in 0..N, 1 ∂ρ := by
rw [integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]
_ ≤ 𝔼[X] + ∫ x in 0..N, 1 ∂ρ := (add_le_add_right (integral_truncation_le_integral_of_nonneg hint hnonneg) _)
_ ≤ 𝔼[X] + 1 := by
refine add_le_add le_rfl ?_
rw [intervalIntegral.integral_of_le (Nat.cast_nonneg _)]
simp only [integral_const, measureReal_restrict_apply', measurableSet_Ioc, Set.univ_inter,
Algebra.id.smul_eq_mul, mul_one]
rw [← ENNReal.toReal_one]
exact ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one
have B : ∀ a b, ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ _ in Set.Ioc a b, (1 : ℝ) ∂ρ) :=
by
intro a b
rw [ofReal_setIntegral_one ρ _, Measure.map_apply_of_aemeasurable hint.aemeasurable measurableSet_Ioc]
rfl
calc
∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) :=
by simp_rw [B]
_ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp [ENNReal.ofReal_sum_of_nonneg]
_ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) :=
by
congr 1
refine sum_congr rfl fun j hj => ?_
rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
_ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A
