PL1/L1UniformIntegrability.lean
All source files · Download exact source
SHA-256: f8095553f60d4628f7fb2d6eee245f811b87baae74a4647ab0c9e92ac7aac620
1import PL1.SchurApproximation2import PL1.DunfordPettis3import PL1.L1Masks4import Mathlib.MeasureTheory.Function.UniformIntegrable5import Mathlib.MeasureTheory.Integral.Bochner.Set6import Mathlib.MeasureTheory.OuterMeasure.BorelCantelli78/-!9# Uniform integrability of weakly convergent scalar L1 sequences1011The disjoint-set argument reduces the substantive compactness step to the12proved Schur theorem for scalar ell1.13-/1415noncomputable section16open Filter MeasureTheory Set17open scoped Topology ENNReal1819namespace PL1.L1UniformIntegrability2021variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}2223/-- A decreasing family carrying a fixed amount of some member of an24integrable sequence yields disjoint annuli carrying a fixed amount of a25subsequence. Each individual member must have vanishing mass on the family. -/26theorem exists_disjoint_annuli27 (f : ℕ → Ω → ℝ) (hf : ∀ n, Integrable (f n) μ)28 (S : ℕ → Set Ω) (hS : ∀ N, MeasurableSet (S N)) (hanti : Antitone S)29 (hlim : ∀ n, Tendsto (fun N => ∫ x in S N, f n x ∂μ) atTop (𝓝 0))30 (ε : ℝ) (hε : 0 < ε)31 (hbad : ∀ N, ∃ n, ε ≤ ∫ x in S N, f n x ∂μ) :32 ∃ n : ℕ → ℕ, (∀ k, k ≤ n k) ∧ ∃ B : ℕ → Set Ω,33 (∀ k, MeasurableSet (B k)) ∧ Pairwise (fun k l => Disjoint (B k) (B l)) ∧34 ∀ k, ε / 2 < ∫ x in B k, f (n k) x ∂μ := by35 classical36 have hstep : ∀ N k : ℕ, ∃ M n P : ℕ,37 N ≤ M ∧ k ≤ n ∧ M < P ∧38 ε ≤ ∫ x in S M, f n x ∂μ ∧ (∫ x in S P, f n x ∂μ) < ε / 2 := by39 intro N k40 have hfinite : ∀ᶠ M in atTop, ∀ j ∈ Finset.range k,41 (∫ x in S M, f j x ∂μ) < ε := by42 apply (eventually_all_finset (Finset.range k)).mpr43 intro j _44 exact (hlim j).eventually_lt_const hε45 obtain ⟨M₀, hM₀⟩ := eventually_atTop.mp hfinite46 let M := max N M₀47 obtain ⟨n, hn⟩ := hbad M48 have hkn : k ≤ n := by49 by_contra h50 exact (not_lt_of_ge hn) (hM₀ M (le_max_right _ _) n (Finset.mem_range.mpr (by omega)))51 obtain ⟨P₀, hP₀⟩ := eventually_atTop.mp ((hlim n).eventually_lt_const (half_pos hε))52 exact ⟨M, n, max (M + 1) P₀, le_max_left _ _, hkn,53 (Nat.lt_succ_self M).trans_le (le_max_left _ _), hn,54 hP₀ _ (le_max_right _ _)⟩55 choose a b c ha hb hc hlarge hsmall using hstep56 let cut : ℕ → ℕ := Nat.rec 0 (fun k N => c N k)57 have hcutstep : ∀ k, cut k < cut (k + 1) := by58 intro k59 exact (ha (cut k) k).trans_lt (hc (cut k) k)60 have hcut : StrictMono cut := strictMono_nat_of_lt_succ hcutstep61 let n : ℕ → ℕ := fun k => b (cut k) k62 let B : ℕ → Set Ω := fun k => S (a (cut k) k) \ S (cut (k + 1))63 refine ⟨n, (fun k => hb _ _), B, (fun k => (hS _).diff (hS _)), ?_, ?_⟩64 · intro k l hkl65 apply Set.disjoint_left.mpr66 intro x hxk hxl67 rcases lt_or_gt_of_ne hkl with hlt | hgt68 · apply hxk.269 exact hanti ((hcut.monotone (Nat.succ_le_of_lt hlt)).trans (ha _ _)) hxl.170 · apply hxl.271 exact hanti ((hcut.monotone (Nat.succ_le_of_lt hgt)).trans (ha _ _)) hxk.172 · intro k73 dsimp [B]74 rw [setIntegral_sdiff (hS _) (hf _).integrableOn (hanti (hc _ _).le)]75 have h₁ := hlarge (cut k) k76 have h₂ := hsmall (cut k) k77 change ε / 2 < (∫ x in S (a (cut k) k), f (b (cut k) k) x ∂μ) -78 ∫ x in S (c (cut k) k), f (b (cut k) k) x ∂μ79 linarith8081section ScalarL18283variable {𝕜 : Type*} [RCLike 𝕜]8485/-- Uniform absolute continuity of the integral norms, in a real-valued form. -/86def UniformSmallSetMass (x : ℕ → Lp 𝕜 1 μ) : Prop :=87 ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ≥0∞, 0 < δ ∧88 ∀ n A, MeasurableSet A → μ A ≤ δ → (∫ a in A, ‖x n a‖ ∂μ) ≤ ε8990/-- Failure of uniform absolute continuity supplies disjoint measurable sets91on which a subsequence retains a positive amount of integral norm. -/92theorem exists_disjoint_sets_of_not_uniformSmallSetMass93 {x : ℕ → Lp 𝕜 1 μ} (hbad : ¬ UniformSmallSetMass x) :94 ∃ ε : ℝ, 0 < ε ∧ ∃ n : ℕ → ℕ, (∀ k, k ≤ n k) ∧95 ∃ B : ℕ → Set Ω, (∀ k, MeasurableSet (B k)) ∧96 Pairwise (fun k l => Disjoint (B k) (B l)) ∧97 ∀ k, ε < ∫ a in B k, ‖x (n k) a‖ ∂μ := by98 classical99 simp only [UniformSmallSetMass] at hbad100 push Not at hbad101 obtain ⟨ε, hε, hbad⟩ := hbad102 have hchoose : ∀ j : ℕ, ∃ n A, MeasurableSet A ∧103 μ A ≤ ENNReal.ofReal ((1 / 2 : ℝ) ^ j) ∧ ε < ∫ a in A, ‖x n a‖ ∂μ := by104 intro j105 exact hbad _ (ENNReal.ofReal_pos.mpr (by positivity))106 choose n A hA hμA hmass using hchoose107 let S : ℕ → Set Ω := fun N => ⋃ j ≥ N, A j108 have hS : ∀ N, MeasurableSet (S N) := fun N => .iUnion fun j => .iUnion fun _ => hA j109 have hanti : Antitone S := by110 intro N M hNM111 exact iUnion₂_subset fun j hj => subset_iUnion₂_of_subset j (hNM.trans hj) (Subset.refl _)112 have hsum : ∑' j, μ (A j) ≠ ∞ := by113 apply ne_top_of_le_ne_top _ (ENNReal.tsum_le_tsum hμA)114 exact (summable_geometric_of_abs_lt_one (by norm_num : |(1 / 2 : ℝ)| < 1)).tsum_ofReal_ne_top115 have hnull : μ (⋂ N, S N) = 0 := by116 have hh := measure_limsup_atTop_eq_zero hsum117 simpa only [limsup_eq_iInf_iSup_of_nat, Set.iSup_eq_iUnion, Set.iInf_eq_iInter, S] using hh118 have hlim : ∀ n, Tendsto (fun N => ∫ a in S N, ‖x n a‖ ∂μ) atTop (𝓝 0) := by119 intro n120 have h := tendsto_setIntegral_of_antitone hS hanti121 ⟨0, (L1.integrable_coeFn (x n)).norm.integrableOn⟩122 simpa only [setIntegral_measure_zero _ hnull] using h123 have hlarge : ∀ N, ∃ n, ε ≤ ∫ a in S N, ‖x n a‖ ∂μ := by124 intro N125 refine ⟨n N, (hmass N).le.trans ?_⟩126 apply setIntegral_mono_set (L1.integrable_coeFn _).norm.integrableOn127 (Eventually.of_forall fun _ => norm_nonneg _)128 exact Eventually.of_forall fun a ha => mem_iUnion.mpr ⟨N, mem_iUnion.mpr ⟨le_rfl, ha⟩⟩129 obtain ⟨m, hm, B, hB, hdisj, hmassB⟩ :=130 exists_disjoint_annuli (fun n a => ‖x n a‖) (fun n => (L1.integrable_coeFn _).norm)131 S hS hanti hlim ε hε hlarge132 exact ⟨ε / 2, half_pos hε, m, hm, B, hB, hdisj, hmassB⟩133134/-- Norming a sequence on disjoint measurable sets produces a single bounded135operator into the genuine scalar ell1 space. -/136theorem exists_disjoint_norming_operator (f : ℕ → Lp 𝕜 1 μ)137 (B : ℕ → Set Ω) (hB : ∀ k, MeasurableSet (B k))138 (hdisj : Pairwise (fun k l => Disjoint (B k) (B l))) :139 ∃ T : Lp 𝕜 1 μ →L[𝕜] Ell1 𝕜, ‖T‖ ≤ 1 ∧140 ∀ k, T (f k) k = (‖L1Masks.mask μ (B k) (hB k) (f k)‖ : 𝕜) := by141 classical142 choose ψ hψ hvalue using fun k =>143 exists_dual_vector'' 𝕜 (L1Masks.mask μ (B k) (hB k) (f k))144 let α : ℕ → Lp 𝕜 1 μ →L[𝕜] 𝕜 := fun k => (ψ k).comp (L1Masks.mask μ (B k) (hB k))145 have hsum : ∀ (g : Lp 𝕜 1 μ) (s : Finset ℕ), ∑ k ∈ s, ‖α k g‖ ≤ ‖g‖ := by146 intro g s147 apply le_trans _ (L1Masks.sum_norm_mask_le μ s B hB hdisj g)148 apply Finset.sum_le_sum149 intro k _150 change ‖ψ k (L1Masks.mask μ (B k) (hB k) g)‖ ≤ ‖L1Masks.mask μ (B k) (hB k) g‖151 exact ((ψ k).le_opNorm _).trans (by152 simpa only [one_mul] using153 mul_le_mul_of_nonneg_right (hψ k) (norm_nonneg (L1Masks.mask μ (B k) (hB k) g)))154 let T₀ : Lp 𝕜 1 μ →ₗ[𝕜] Ell1 𝕜 :=155 { toFun := fun g => ⟨fun k => α k g, memℓp_gen' (by simpa using hsum g)⟩156 map_add' := by intro g h; ext k; exact (α k).map_add g h157 map_smul' := by intro c g; ext k; exact (α k).map_smul c g }158 have hT₀ : ∀ g, ‖T₀ g‖ ≤ 1 * ‖g‖ := by159 intro g160 rw [one_mul]161 apply lp.norm_le_of_forall_sum_le (by simp) (norm_nonneg g)162 intro s163 simpa only [T₀, LinearMap.coe_mk, AddHom.coe_mk, ENNReal.toReal_one, Real.rpow_one] using hsum g s164 let T := T₀.mkContinuous 1 hT₀165 refine ⟨T, ContinuousLinearMap.opNorm_le_bound _ zero_le_one hT₀, ?_⟩166 exact hvalue167168/-- Weak convergence in scalar L1 implies uniform absolute continuity of the169integral norms. This holds for arbitrary measures, without a finiteness or170probability assumption. -/171theorem weaklyConverges_uniformSmallSetMass {x : ℕ → Lp 𝕜 1 μ} {a : Lp 𝕜 1 μ}172 (hx : WeaklyConverges 𝕜 (Lp 𝕜 1 μ) x a) : UniformSmallSetMass x := by173 by_contra hbad174 obtain ⟨ε, hε, n, hn, B, hB, hdisj, hmass⟩ :=175 exists_disjoint_sets_of_not_uniformSmallSetMass hbad176 obtain ⟨T, _, hvalue⟩ := exists_disjoint_norming_operator (fun k => x (n k)) B hB hdisj177 have hn_top : Tendsto n atTop atTop := tendsto_atTop_mono hn tendsto_id178 have hTlim := (ell1_hasSchurProperty 𝕜 _ _ (hx.map T)).comp hn_top179 have hdiff : Tendsto (fun k => ‖T (x (n k)) - T a‖) atTop (𝓝 0) := by180 simpa only [sub_self, norm_zero, Function.comp_def] using181 (hTlim.sub (tendsto_const_nhds (x := T a))).norm182 have hcoord : Tendsto (fun k => ‖T a k‖) atTop (𝓝 0) :=183 (L1Sum.summable_norm (T a)).tendsto_atTop_zero184 have hsumlim : Tendsto (fun k => ‖T (x (n k)) - T a‖ + ‖T a k‖) atTop (𝓝 0) := by185 simpa only [zero_add] using hdiff.add hcoord186 obtain ⟨k, hk⟩ := (hsumlim.eventually_lt_const hε).exists187 have hlower : ε < ‖T (x (n k)) k‖ := by188 rw [hvalue k, RCLike.norm_ofReal, abs_of_nonneg (norm_nonneg _), L1Masks.norm_mask]189 exact hmass k190 have hupper : ‖T (x (n k)) k‖ ≤ ‖T (x (n k)) - T a‖ + ‖T a k‖ := by191 calc192 ‖T (x (n k)) k‖ ≤ ‖T (x (n k)) k - T a k‖ + ‖T a k‖ := by193 simpa only [sub_add_cancel] using norm_add_le (T (x (n k)) k - T a k) (T a k)194 _ ≤ ‖T (x (n k)) - T a‖ + ‖T a k‖ := by195 apply add_le_add _ le_rfl196 exact lp.norm_apply_le_norm (by simp : (1 : ℝ≥0∞) ≠ 0) (T (x (n k)) - T a) k197 linarith198199/-- The real-valued small-set criterion implies Mathlib's measure-theoretic200uniform integrability predicate. -/201theorem UniformSmallSetMass.unifIntegrable {x : ℕ → Lp 𝕜 1 μ}202 (hx : UniformSmallSetMass x) : UnifIntegrable (fun n => (x n : Ω → 𝕜)) 1 μ := by203 apply unifIntegrable_iff'.mpr204 intro ε hε205 by_cases htop : ε = ∞206 · subst ε207 exact ⟨1, by simp, fun _ _ _ _ => le_top⟩208 obtain ⟨δ, hδ, hbound⟩ := hx ε.toReal (ENNReal.toReal_pos hε.ne' htop)209 refine ⟨δ, hδ, fun n A hA hμA => ?_⟩210 rw [eLpNorm_one_eq_lintegral_enorm,211 ← ofReal_integral_norm_eq_lintegral_enorm (L1.integrable_coeFn (x n)).integrableOn]212 exact (ENNReal.ofReal_le_ofReal (hbound n A hA hμA)).trans_eq (ENNReal.ofReal_toReal htop)213214/-- Weakly convergent scalar L1 sequences are uniformly integrable in215Mathlib's full sense: uniformly absolutely continuous integral norms and a216uniform L1 bound. The result applies to arbitrary measures and both fields. -/217theorem weaklyConverges_uniformIntegrable {x : ℕ → Lp 𝕜 1 μ} {a : Lp 𝕜 1 μ}218 (hx : WeaklyConverges 𝕜 (Lp 𝕜 1 μ) x a) :219 UniformIntegrable (fun n => (x n : Ω → 𝕜)) 1 μ := by220 obtain ⟨C, hC, hbound⟩ := hx.exists_pos_norm_bound221 refine ⟨fun n => (L1.integrable_coeFn (x n)).aestronglyMeasurable,222 (weaklyConverges_uniformSmallSetMass hx).unifIntegrable, ⟨⟨C, hC.le⟩, fun n => ?_⟩⟩223 rw [← Lp.enorm_def]224 exact ENNReal.coe_le_coe.mpr (hbound n)225226end ScalarL1227228end PL1.L1UniformIntegrability229