English
If hf: UnifTight f p μ, then for any ε ≠ 0, almost all finite-measure small sets s satisfy ∀ i, eLpNorm (s.indicator (f i)) ≤ ε.
Русский
Если hf: UnifTight f p μ, то почти наверняка для малых множеств с конечной мерой выполняется ∀i, eLpNorm (s.indicator(f_i)) ≤ ε.
LaTeX
$$$\text{UnifTight}(f,p,\mu) \Rightarrow \forall \varepsilon \neq 0,\ (\forall^{\rm ord} s \in μ.cofinite.smallSets, \forall i, eLpNorm(s.indicator(f_i))_{p,\mu} \le \varepsilon)$$$
Lean4
theorem eventually_cofinite_indicator (hf : UnifTight f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∀ᶠ s in μ.cofinite.smallSets, ∀ i, eLpNorm (s.indicator (f i)) p μ ≤ ε :=
by
by_cases hε_top : ε = ∞
· subst hε_top; simp
rcases hf (pos_iff_ne_zero.2 (toNNReal_ne_zero.mpr ⟨hε, hε_top⟩)) with ⟨s, hμs, hfs⟩
refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩
· intro s t hst ht i
exact (eLpNorm_mono <| norm_indicator_le_of_subset hst _).trans (ht i)
· rwa [Measure.compl_mem_cofinite, lt_top_iff_ne_top]
