English
A general auxiliary lemma that provides a uniform bound for eLpNorm across sets under a bound C; this is a precursor to unifIntegrable_of' type statements.
Русский
Обобщенная вспомогательная лемма для ограничений на eLpNorm через константу C.
LaTeX
$$$\text{unifIntegrable_of'}\text{(hp, hp', f, h)}$$$
Lean4
/-- This lemma is superseded by `unifIntegrable_of` which do not require `C` to be positive. -/
theorem unifIntegrable_of' (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → β} (hf : ∀ i, StronglyMeasurable (f i))
(h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, 0 < C ∧ ∀ i, eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
UnifIntegrable f p μ := by
have hpzero := (lt_of_lt_of_le zero_lt_one hp).ne.symm
by_cases hμ : μ Set.univ = 0
· rw [Measure.measure_univ_eq_zero] at hμ
exact hμ.symm ▸ unifIntegrable_zero_meas
intro ε hε
obtain ⟨C, hCpos, hC⟩ := h (ε / 2) (half_pos hε)
refine
⟨(ε / (2 * C)) ^ ENNReal.toReal p, Real.rpow_pos_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos))) _,
fun i s hs hμs => ?_⟩
by_cases hμs' : μ s = 0
· rw [(eLpNorm_eq_zero_iff ((hf i).indicator hs).aestronglyMeasurable hpzero).2 (indicator_meas_zero hμs')]
simp
calc
eLpNorm (Set.indicator s (f i)) p μ ≤
eLpNorm (Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i)) p μ +
eLpNorm (Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ :=
by
refine
le_trans (Eq.le ?_)
(eLpNorm_add_le
(StronglyMeasurable.aestronglyMeasurable
((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
(StronglyMeasurable.aestronglyMeasurable
((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
hp)
congr
change
_ = fun x => (s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) x + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i) x
rw [← Set.indicator_union_of_disjoint]
·
rw [← Set.inter_union_distrib_left,
(by ext; simp [le_or_gt] : {x : α | C ≤ ‖f i x‖₊} ∪ {x : α | ‖f i x‖₊ < C} = Set.univ), Set.inter_univ]
· refine (Disjoint.inf_right' _ ?_).inf_left' _
rw [disjoint_iff_inf_le]
rintro x ⟨hx₁, hx₂⟩
rw [Set.mem_setOf_eq] at hx₁ hx₂
exact False.elim (hx₂.ne (eq_of_le_of_not_lt hx₁ (not_lt.2 hx₂.le)).symm)
_ ≤ eLpNorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ + (C : ℝ≥0∞) * μ s ^ (1 / ENNReal.toReal p) :=
by
refine add_le_add (eLpNorm_mono fun x => norm_indicator_le_of_subset Set.inter_subset_right _ _) ?_
rw [← Set.indicator_indicator]
rw [eLpNorm_indicator_eq_eLpNorm_restrict hs]
have : ∀ᵐ x ∂μ.restrict s, ‖{x : α | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ C :=
by
filter_upwards
simp_rw [norm_indicator_eq_indicator_norm]
exact Set.indicator_le' (fun x (hx : _ < _) => hx.le) fun _ _ => NNReal.coe_nonneg _
refine le_trans (eLpNorm_le_of_ae_bound this) ?_
rw [mul_comm, Measure.restrict_apply' hs, Set.univ_inter, ENNReal.ofReal_coe_nnreal, one_div]
_ ≤ ENNReal.ofReal (ε / 2) + C * ENNReal.ofReal (ε / (2 * C)) :=
by
refine add_le_add (hC i) (mul_le_mul_left' ?_ _)
rwa [one_div, ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hpzero hp'),
ENNReal.ofReal_rpow_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos)))]
_ ≤ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) :=
by
refine add_le_add_left ?_ _
rw [← ENNReal.ofReal_coe_nnreal, ← ENNReal.ofReal_mul (NNReal.coe_nonneg _), ← div_div,
mul_div_cancel₀ _ (NNReal.coe_pos.2 hCpos).ne.symm]
_ ≤ ENNReal.ofReal ε := by rw [← ENNReal.ofReal_add (half_pos hε).le (half_pos hε).le, add_halves]
