On complemented subspaces of L1[0,1]L_1[0,1]

PL1/RNPBridge.lean

All source files · Download exact source

SHA-256: f8a4a9aa83d788c30173a4c7fa2020374e79efacf11c2ff48379ab6939743105

1import PL1.Definitions2import Mathlib.Analysis.Normed.Operator.NNNorm3import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap4import Mathlib.MeasureTheory.Function.LpSpace.Indicator5import Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum67/-!8# Transport and operator consequences of the reviewed RNP definition910This file uses `PL1.HasRadonNikodymProperty` unchanged, with its full11vector-measure quantifiers and explicit source universe.12-/1314noncomputable section15universe u v w16open MeasureTheory Set17open scoped ENNReal NNReal Function1819namespace PL1.RNPBridge2021variable {E : Type u} {F : Type v}22  [NormedAddCommGroup E] [NormedSpace ℝ E]23  [NormedAddCommGroup F] [NormedSpace ℝ F]2425/-- Apply a bounded linear map to a countably additive vector measure. -/26def mapVectorMeasure {Ω : Type w} [MeasurableSpace Ω]27    (T : E →L[ℝ] F) (ν : VectorMeasure Ω E) : VectorMeasure Ω F :=28  ν.mapRange T.toLinearMap.toAddMonoidHom T.continuous2930@[simp]31theorem mapVectorMeasure_apply {Ω : Type w} [MeasurableSpace Ω]32    (T : E →L[ℝ] F) (ν : VectorMeasure Ω E) (A : Set Ω) :33    mapVectorMeasure T ν A = T (ν A) := rfl3435/-- Bounded maps multiply total variation by at most their operator norm. -/36theorem variation_mapVectorMeasure_le {Ω : Type w} [MeasurableSpace Ω]37    (T : E →L[ℝ] F) (ν : VectorMeasure Ω E) :38    (mapVectorMeasure T ν).variation ≤ ‖T‖ₑ • ν.variation := by39  apply VectorMeasure.variation_le_of_forall_enorm_le40  intro A hA41  simp only [mapVectorMeasure_apply, Measure.smul_apply, smul_eq_mul]42  exact (T.le_opENorm (ν A)).trans43    (mul_le_mul_of_nonneg_left (VectorMeasure.enorm_measure_le_variation ν A) zero_le)4445theorem mapVectorMeasure_finite_variation {Ω : Type w} [MeasurableSpace Ω]46    (T : E →L[ℝ] F) (ν : VectorMeasure Ω E) (hν : ν.variation univ < ∞) :47    (mapVectorMeasure T ν).variation univ < ∞ := by48  apply lt_of_le_of_lt (variation_mapVectorMeasure_le T ν univ)49  simpa only [Measure.smul_apply, smul_eq_mul] using50    ENNReal.mul_lt_top (by simp : ‖T‖ₑ < ∞) hν5152/-- The reviewed RNP is preserved by real Banach-space isomorphism.53The universe of measurable source spaces is independent of both target universes. -/54theorem hasRadonNikodymProperty_of_equiv (e : E ≃L[ℝ] F)55    (hE : HasRadonNikodymProperty.{u, w} E) : HasRadonNikodymProperty.{v, w} F := by56  intro Ω mΩ57  let := mΩ58  intro μ hμ ν hν hAC59  let η : VectorMeasure Ω E := mapVectorMeasure e.symm.toContinuousLinearMap ν60  have hη : η.variation univ < ∞ := mapVectorMeasure_finite_variation _ ν hν61  have hηAC : ∀ A : Set Ω, MeasurableSet A → μ A = 0 → η A = 0 := by62    intro A hA hz63    change e.symm (ν A) = 064    rw [hAC A hA hz, map_zero]65  obtain ⟨g, hg, hrepr⟩ := hE Ω mΩ μ hμ η hη hηAC66  refine ⟨fun x => e (g x), e.toContinuousLinearMap.integrable_comp hg, ?_⟩67  intro A hA68  rw [e.integral_comp_comm]69  rw [← hrepr A hA]70  exact (e.apply_symm_apply (ν A)).symm7172theorem hasRadonNikodymProperty_iff_equiv (e : E ≃L[ℝ] F) :73    HasRadonNikodymProperty.{u, w} E ↔ HasRadonNikodymProperty.{v, w} F :=74  ⟨hasRadonNikodymProperty_of_equiv e, hasRadonNikodymProperty_of_equiv e.symm⟩7576theorem not_hasRadonNikodymProperty_of_equiv (e : E ≃L[ℝ] F)77    (hE : ¬ HasRadonNikodymProperty.{u, w} E) : ¬ HasRadonNikodymProperty.{v, w} F :=78  fun hF => hE (hasRadonNikodymProperty_of_equiv e.symm hF)7980section IndicatorMeasure8182variable {Ω : Type w} [MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ]8384/-- The genuine `L1` class of a measurable indicator, extended by zero on85nonmeasurable sets to conform to `VectorMeasure`. -/86def indicatorL1 (A : Set Ω) : Lp ℝ 1 μ := by87  classical88  exact if hA : MeasurableSet A then indicatorConstLp 1 hA (measure_ne_top μ A) (1 : ℝ) else 08990theorem indicatorL1_of_measurable {A : Set Ω} (hA : MeasurableSet A) :91    indicatorL1 μ A = indicatorConstLp 1 hA (measure_ne_top μ A) (1 : ℝ) := by92  simp only [indicatorL1, dite_eq_left hA]9394theorem indicatorL1_coeFn {A : Set Ω} (hA : MeasurableSet A) :95    (indicatorL1 μ A : Ω → ℝ) =ᵐ[μ] A.indicator (fun _ => (1 : ℝ)) := by96  rw [indicatorL1_of_measurable μ hA]97  exact indicatorConstLp_coeFn9899theorem enorm_indicatorL1_le (A : Set Ω) : ‖indicatorL1 μ A‖ₑ ≤ μ A := by100  by_cases hA : MeasurableSet A101  · rw [indicatorL1_of_measurable μ hA]102    simpa using (enorm_indicatorConstLp_le (p := 1) (hs := hA)103      (hμs := measure_ne_top μ A) (c := (1 : ℝ)))104  · simp [indicatorL1, hA]105106theorem norm_indicatorL1 {A : Set Ω} (hA : MeasurableSet A) :107    ‖indicatorL1 μ A‖ = μ.real A := by108  rw [indicatorL1_of_measurable μ hA]109  simpa using (norm_indicatorConstLp (p := 1) (hs := hA)110    (hμs := measure_ne_top μ A) (c := (1 : ℝ)) (by norm_num) (by simp))111112theorem indicatorL1_eq_zero_of_null {A : Set Ω} (hA : μ A = 0) : indicatorL1 μ A = 0 := by113  apply enorm_eq_zero.1114  exact le_antisymm (hA ▸ enorm_indicatorL1_le μ A) zero_le115116/-- Countable additivity of the canonical indicator-valued vector measure. -/117theorem hasSum_indicatorL1 {A : ℕ → Set Ω} (hA : ∀ n, MeasurableSet (A n))118    (hdisj : Pairwise (Disjoint on A)) :119    HasSum (fun n => indicatorL1 μ (A n)) (indicatorL1 μ (⋃ n, A n)) := by120  have habs : (∑' n, ‖indicatorL1 μ (A n)‖ₑ) ≠ ∞ := by121    apply ne_of_lt122    calc123      _ ≤ ∑' n, μ (A n) := ENNReal.tsum_le_tsum (fun n => enorm_indicatorL1_le μ (A n))124      _ = μ (⋃ n, A n) := (measure_iUnion hdisj hA).symm125      _ < ∞ := measure_lt_top μ _126  have hsum : Summable (fun n => indicatorL1 μ (A n)) := Summable.of_enorm habs127  have heq : (∑' n, indicatorL1 μ (A n)) = indicatorL1 μ (⋃ n, A n) := by128    apply Lp.ext129    filter_upwards [Lp.coeFn_tsum habs,130      ae_all_iff.2 (fun n => indicatorL1_coeFn μ (hA n)),131      indicatorL1_coeFn μ (MeasurableSet.iUnion hA)] with x hx hxi hxU132    rw [hx, hxU]133    simp only [hxi]134    by_cases hmem : ∃ n, x ∈ A n135    · obtain ⟨n, hn⟩ := hmem136      rw [Set.indicator_of_mem (Set.mem_iUnion.2 ⟨n, hn⟩)]137      rw [tsum_eq_single n]138      · exact Set.indicator_of_mem hn _139      · intro k hk140        apply Set.indicator_of_notMem141        intro hxk142        exact Set.disjoint_left.1 (hdisj hk) hxk hn143    · have hnone : ∀ n, x ∉ A n := by simpa using hmem144      have hU : x ∉ ⋃ n, A n := by simpa using hmem145      simp [hnone, hU]146  rw [← heq]147  exact hsum.hasSum148149/-- The canonical countably additive `L1`-valued measure `A ↦ 1_A`. -/150def indicatorVectorMeasure : VectorMeasure Ω (Lp ℝ 1 μ) where151  measureOf' := indicatorL1 μ152  empty' := by simp [indicatorL1, indicatorConstLp_empty]153  not_measurable' := by intro A hA; simp [indicatorL1, hA]154  m_iUnion' := by155    intro A hA hdisj156    exact hasSum_indicatorL1 μ hA hdisj157158@[simp]159theorem indicatorVectorMeasure_apply (A : Set Ω) :160    indicatorVectorMeasure μ A = indicatorL1 μ A := rfl161162theorem variation_indicatorVectorMeasure_le : (indicatorVectorMeasure μ).variation ≤ μ :=163  VectorMeasure.variation_le_of_forall_enorm_le (fun A _ => enorm_indicatorL1_le μ A)164165/-- The vector measure canonically induced by an operator out of actual `L1`. -/166def operatorVectorMeasure (T : Lp ℝ 1 μ →L[ℝ] E) : VectorMeasure Ω E :=167  mapVectorMeasure T (indicatorVectorMeasure μ)168169@[simp]170theorem operatorVectorMeasure_apply (T : Lp ℝ 1 μ →L[ℝ] E) (A : Set Ω) :171    operatorVectorMeasure μ T A = T (indicatorL1 μ A) := rfl172173theorem variation_operatorVectorMeasure_le (T : Lp ℝ 1 μ →L[ℝ] E) :174    (operatorVectorMeasure μ T).variation ≤ ‖T‖ₑ • μ := by175  apply VectorMeasure.variation_le_of_forall_enorm_le176  intro A hA177  simp only [operatorVectorMeasure_apply, Measure.smul_apply, smul_eq_mul]178  exact (T.le_opENorm (indicatorL1 μ A)).trans179    (mul_le_mul_of_nonneg_left (enorm_indicatorL1_le μ A) zero_le)180181theorem operatorVectorMeasure_finite_variation (T : Lp ℝ 1 μ →L[ℝ] E) :182    (operatorVectorMeasure μ T).variation univ < ∞ := by183  apply lt_of_le_of_lt (variation_operatorVectorMeasure_le μ T univ)184  simpa only [Measure.smul_apply, smul_eq_mul] using185    ENNReal.mul_lt_top (by simp : ‖T‖ₑ < ∞) (measure_lt_top μ univ)186187theorem operatorVectorMeasure_absolutelyContinuous (T : Lp ℝ 1 μ →L[ℝ] E)188    {A : Set Ω} (hA : μ A = 0) : operatorVectorMeasure μ T A = 0 := by189  rw [operatorVectorMeasure_apply, indicatorL1_eq_zero_of_null μ hA, map_zero]190191/-- The full reviewed RNP gives a Bochner density for the operator's values on192every measurable indicator. No representability premise is substituted for RNP. -/193theorem exists_setwise_density_of_RNP (hE : HasRadonNikodymProperty.{u, w} E)194    (T : Lp ℝ 1 μ →L[ℝ] E) :195    ∃ g : Ω → E, Integrable g μ ∧ ∀ A : Set Ω, MeasurableSet A →196      T (indicatorL1 μ A) = ∫ x in A, g x ∂μ := by197  obtain ⟨g, hg, hrepr⟩ := hE Ω inferInstance μ (measure_lt_top μ univ)198    (operatorVectorMeasure μ T) (operatorVectorMeasure_finite_variation μ T)199    (fun A _ hA => operatorVectorMeasure_absolutelyContinuous μ T hA)200  exact ⟨g, hg, hrepr⟩201202/-- A single nonrepresentable operator witnesses failure of the reviewed RNP. -/203theorem not_RNP_of_no_setwise_density (T : Lp ℝ 1 μ →L[ℝ] E)204    (hT : ¬ ∃ g : Ω → E, Integrable g μ ∧ ∀ A : Set Ω, MeasurableSet A →205      T (indicatorL1 μ A) = ∫ x in A, g x ∂μ) :206    ¬ HasRadonNikodymProperty.{u, w} E := fun hE => hT (exists_setwise_density_of_RNP μ hE T)207208end IndicatorMeasure209210end PL1.RNPBridge211212