exists_nat_measure_lt_two_inv — Mathlib

English

If f converges to g in measure, then for every n there exists N such that for all m ≥ N, the measure of the set where (2)^{-n} ≤ edist(f_m, g) is small (bounded by (1/2)^n).

Русский

Если f сходится по мере к g, то для каждого n существует N, такое что для всех m ≥ N множество {x: (2)^{-n} ≤ edist(f_m(x), g(x))} имеет малую меру, не более чем (1/2)^n.

LaTeX

$$$[\text{TendstoInMeasure}(\mu,f,\,\text{atTop},g)] \Rightarrow \\exists N, \forall m\ge N, \mu\{x : (2)^{-n} \le edist(f_m(x), g(x))\} \le (2^{-1})^{n}$$$

Lean4

theorem exists_nat_measure_lt_two_inv (hfg : TendstoInMeasure μ f atTop g) (n : ℕ) :
    ∃ N, ∀ m ≥ N, μ {x | (2 : ℝ≥0∞)⁻¹ ^ n ≤ edist (f m x) (g x)} ≤ (2⁻¹ : ℝ≥0∞) ^ n :=
  by
  specialize hfg ((2⁻¹ : ℝ≥0∞) ^ n) (ENNReal.pow_pos (by simp) _)
  rw [ENNReal.tendsto_atTop_zero] at hfg
  exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr fun h_zero => by simpa using pow_eq_zero h_zero)

Похожие утверждения