English
The UnifTight condition is equivalent to a bound by real ε with eLpNorm ≤ ε for all i outside a finite-measure set.
Русский
Условие UnifTight эквивалентно ограничению на Real ε: для каждого ε>0 существует множество, где для всех i нормa ≤ ε.
LaTeX
$$$\text{UnifTight}(f,p,\mu) \iff \forall \varepsilon\in\mathbb{R}, \varepsilon>0 \Rightarrow \exists s:\mathsf{Set}\,\alpha,\ \mu(s)\neq\infty \land \forall i, eLpNorm( (s^c).indicator(f_i) )_{p,\mu} \le \operatorname{ofReal}(\varepsilon)$$$
Lean4
theorem unifTight_iff_real {_ : MeasurableSpace α} (f : ι → α → β) (p : ℝ≥0∞) (μ : Measure α) :
UnifTight f p μ ↔ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s : Set α, μ s ≠ ∞ ∧ ∀ i, eLpNorm (sᶜ.indicator (f i)) p μ ≤ .ofReal ε :=
by
refine ⟨fun hut rε hrε ↦ hut (Real.toNNReal_pos.mpr hrε), fun hut ε hε ↦ ?_⟩
obtain ⟨s, hμs, hfε⟩ := hut hε
use s, hμs; intro i
exact (hfε i).trans_eq (ofReal_coe_nnreal (p := ε))
