PL1/L1Truncation.lean
All source files · Download exact source
SHA-256: 14db5f2ffbbce13da1e1172d37ce317bc03a9060e541e33825076dbb65a76e79
1import PL1.L1UniformIntegrability2import PL1.CompactRestriction34/-!5# Uniform bounded truncation and the L1 compact-restriction criterion67Actual bounded functions approximate every weakly convergent scalar L18sequence uniformly. Consequently, compactness of an operator's restriction9to L-infinity implies its Dunford-Pettis property on L1.10-/1112noncomputable section13open Filter MeasureTheory Set14open scoped Topology ENNReal NNReal1516namespace PL1.L1Truncation1718variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]19variable (μ : Measure Ω)2021/-- Remove the part of an L1 function at or above a prescribed norm threshold. -/22def truncatedFun (f : Lp 𝕜 1 μ) (C : ℝ≥0) : Ω → 𝕜 :=23 {a | ‖f a‖₊ < C}.indicator f2425theorem measurableSet_below (f : Lp 𝕜 1 μ) (C : ℝ≥0) :26 MeasurableSet {a | ‖f a‖₊ < C} :=27 measurableSet_lt (Lp.stronglyMeasurable f).nnnorm.measurable measurable_const2829theorem norm_truncatedFun_le (f : Lp 𝕜 1 μ) (C : ℝ≥0) (a : Ω) :30 ‖truncatedFun μ f C a‖ ≤ C := by31 classical32 by_cases ha : ‖f a‖₊ < C33 · simp only [truncatedFun, mem_ofPred_eq, ha, indicator_of_mem]34 exact_mod_cast ha.le35 · rw [truncatedFun, indicator_of_notMem (show a ∉ {a | ‖f a‖₊ < C} from ha), norm_zero]36 exact C.property3738theorem memLp_truncatedFun (f : Lp 𝕜 1 μ) (C : ℝ≥0) :39 MemLp (truncatedFun μ f C) ∞ μ :=40 memLp_top_of_bound ((Lp.aestronglyMeasurable f).indicator (measurableSet_below μ f C)) C41 (Eventually.of_forall (norm_truncatedFun_le μ f C))4243/-- The bounded truncation as an actual L-infinity equivalence class. -/44def truncate (f : Lp 𝕜 1 μ) (C : ℝ≥0) : Lp 𝕜 ∞ μ :=45 (memLp_truncatedFun μ f C).toLp (truncatedFun μ f C)4647theorem coeFn_truncate (f : Lp 𝕜 1 μ) (C : ℝ≥0) :48 truncate μ f C =ᵐ[μ] truncatedFun μ f C :=49 (memLp_truncatedFun μ f C).coeFn_toLp5051variable [IsProbabilityMeasure μ]5253theorem norm_truncate_le (f : Lp 𝕜 1 μ) (C : ℝ≥0) : ‖truncate μ f C‖ ≤ C := by54 have hb : ∀ᵐ a ∂μ, ‖truncate μ f C a‖ ≤ C := by55 filter_upwards [coeFn_truncate μ f C] with a ha56 rw [ha]57 exact norm_truncatedFun_le μ f C a58 simpa using Lp.norm_le_of_ae_bound C.property hb5960/-- The truncation error is precisely the removed large-value tail. -/61theorem coeFn_sub_inclusion_truncate (f : Lp 𝕜 1 μ) (C : ℝ≥0) :62 (f - ProbabilityLp.inclusion μ 1 ∞ le_top (truncate μ f C) : Lp 𝕜 1 μ) =ᵐ[μ]63 {a | C ≤ ‖f a‖₊}.indicator f := by64 classical65 filter_upwards [Lp.coeFn_sub f (ProbabilityLp.inclusion μ 1 ∞ le_top (truncate μ f C)),66 ProbabilityLp.coeFn_inclusion μ 1 ∞ le_top (truncate μ f C), coeFn_truncate μ f C]67 with a hsub hinc htrunc68 change (f - ProbabilityLp.inclusion μ 1 ∞ le_top (truncate μ f C)) a =69 f a - ProbabilityLp.inclusion μ 1 ∞ le_top (truncate μ f C) a at hsub70 rw [hsub, hinc, htrunc]71 by_cases ha : ‖f a‖₊ < C72 · simp [truncatedFun, ha, not_le_of_gt ha]73 · simp [truncatedFun, ha, le_of_not_gt ha]7475/-- Uniform integrability supplies uniform approximation by a bounded ball76of the actual L-infinity space. -/77theorem uniformIntegrable_hasUniformBoundedApproximations {x : ℕ → Lp 𝕜 1 μ}78 (hx : UniformIntegrable (fun n => (x n : Ω → 𝕜)) 1 μ) :79 HasUniformBoundedApproximations (ProbabilityLp.inclusion μ 1 ∞ le_top) x := by80 intro ε hε81 obtain ⟨C, hC⟩ := hx.spec (by simp : (1 : ℝ≥0∞) ≠ 0) (by simp : (1 : ℝ≥0∞) ≠ ∞)82 (ENNReal.ofReal_pos.mpr (half_pos hε))83 refine ⟨C, fun n => ⟨truncate μ (x n) C, norm_truncate_le μ (x n) C, ?_⟩⟩84 rw [Lp.norm_def, eLpNorm_congr_ae (coeFn_sub_inclusion_truncate μ (x n) C)]85 calc86 (eLpNorm ({a | C ≤ ‖x n a‖₊}.indicator (x n)) 1 μ).toReal ≤87 (ENNReal.ofReal (ε / 2)).toReal := ENNReal.toReal_mono (by simp) (hC n)88 _ = ε / 2 := ENNReal.toReal_ofReal (half_pos hε).le89 _ < ε := half_lt_self hε9091/-- The uniform approximation hypothesis follows from full-dual weak92convergence, without any additional assumptions on the sequence. -/93theorem weaklyConverges_hasUniformBoundedApproximations {x : ℕ → Lp 𝕜 1 μ}94 {a : Lp 𝕜 1 μ} (hx : WeaklyConverges 𝕜 (Lp 𝕜 1 μ) x a) :95 HasUniformBoundedApproximations (ProbabilityLp.inclusion μ 1 ∞ le_top) x :=96 uniformIntegrable_hasUniformBoundedApproximations μ97 (L1UniformIntegrability.weaklyConverges_uniformIntegrable hx)9899/-- The paper's compact-restriction criterion for scalar L1 on a probability100space, with the weak-sequence uniform-integrability step fully discharged. -/101theorem isDunfordPettis_of_compact_Linfty_restriction102 {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]103 (T : Lp 𝕜 1 μ →L[𝕜] F)104 (hcompact : IsCompactOperator (T.comp (ProbabilityLp.inclusion μ 1 ∞ le_top))) :105 IsDunfordPettis T :=106 isDunfordPettis_of_compact_restriction T _ hcompact107 (fun _ _ hx => weaklyConverges_hasUniformBoundedApproximations μ hx)108109end PL1.L1Truncation110