English
For f, p, μ, UnifTight f p μ holds iff for every ε > 0, there exists a measurable set with finite μ-measure such that for all i, the eLpNorm outside the set is ≤ ε.
Русский
Для всех ε > 0 существует множество измеримых с конечной мерой, такое что для всех i нормa eLpOutside ≤ ε.
LaTeX
$$$\text{UnifTight}(f,p,\mu) \iff \forall \varepsilon>0, \exists s:\mathsf{Set}\,\alpha,\ \mu(s)\neq\infty \land \forall i, eLpNorm((s^c).indicator(f_i))_{p,\mu} \le \varepsilon$$$
Lean4
theorem unifTight_iff_ennreal {_ : MeasurableSpace α} (f : ι → α → β) (p : ℝ≥0∞) (μ : Measure α) :
UnifTight f p μ ↔ ∀ ⦃ε : ℝ≥0∞⦄, 0 < ε → ∃ s : Set α, μ s ≠ ∞ ∧ ∀ i, eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε :=
by
simp only [ENNReal.forall_ennreal, ENNReal.coe_pos]
refine (and_iff_left ?_).symm
simp only [zero_lt_top, le_top, implies_true, and_true, true_implies]
use ∅; simpa only [measure_empty] using zero_ne_top
