exists_measurableSet_indicator — Mathlib

English

If hf : UnifTight f p μ, then for some ε ≠ 0 there exists a measurable set s with μ s < ∞ such that ∀ i, eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε.

Русский

Если hf: UnifTight f p μ, тогда существует измеримое множество s с μ(s) < ∞ такое, что для всех i выполняется неравенство.

LaTeX

$$$\text{UnifTight}(f,p,\mu) \Rightarrow \forall \varepsilon \neq 0, \exists s\ (\text{MeasurableSet } s \land \mu s < \infty) \land \forall i, eLpNorm((s^c).indicator(f_i))_{p,\mu} \le \varepsilon$$$

Lean4

protected theorem exists_measurableSet_indicator (hf : UnifTight f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∀ i, eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε :=
  let ⟨s, hμs, hsm, hfs⟩ := (hf.eventually_cofinite_indicator hε).exists_measurable_mem_of_smallSets
  ⟨sᶜ, hsm.compl, hμs, by rwa [compl_compl s]⟩

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