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

PL1/DecompositionRNP.lean

All source files · Download exact source

SHA-256: bea0ed03e360d22f80620c96b8ae4477b34b7151e418234ce52374d94505642d

1import PL1.FiniteDimensionalRNP2import PL1.VectorDensityBounds3import Mathlib.MeasureTheory.Integral.DominatedConvergence45/-! # Radon–Nikodym densities from boundedly complete finite-dimensional projections67The hypotheses describe an actual sequence of finite-dimensional projections.8Existence of such a decomposition is not asserted here.9-/1011noncomputable section12universe u v13open MeasureTheory Set Filter14open scoped ENNReal Topology1516namespace PL1.DecompositionRNP1718variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]1920/-- Every bounded coherent sequence in the projection ranges converges in norm.21The case `m = n` of coherence already says that its `n`th term is in the range. -/22def BoundedlyComplete (P : ℕ → E →L[ℝ] E) : Prop :=23  ∀ x : ℕ → E, (∀ m n, m ≤ n → P m (x n) = x m) →24    (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) → ∃ a, Tendsto x atTop (𝓝 a)2526/-- A boundedly complete sequence of uniformly bounded finite-dimensional27projections converging strongly to the identity. -/28structure BoundedlyCompleteDecomposition (E : Type u)29    [NormedAddCommGroup E] [NormedSpace ℝ E] where30  projection : ℕ → E →L[ℝ] E31  finiteDimensional : ∀ n, FiniteDimensional ℝ (projection n).range32  nested : ∀ m n, m ≤ n → (projection m).comp (projection n) = projection m33  uniformBound : ∃ C : ℝ, ∀ n, ‖projection n‖ ≤ C34  tendsto_identity : ∀ x, Tendsto (fun n => projection n x) atTop (𝓝 x)35  bounded_complete : BoundedlyComplete projection3637section Densities38variable {Ω : Type v} [MeasurableSpace Ω] {μ : Measure Ω}3940/-- Uniqueness in the setwise formulation used by the reviewed definition. -/41theorem ae_eq_of_setwise_integral_eq {g h : Ω → E}42    (hg : Integrable g μ) (hh : Integrable h μ)43    (heq : ∀ A : Set Ω, MeasurableSet A → (∫ x in A, g x ∂μ) = ∫ x in A, h x ∂μ) :44    g =ᵐ[μ] h := by45  apply hg.ae_eq_of_withDensityᵥ_eq hh46  apply VectorMeasure.ext47  intro A hA48  simpa only [withDensityᵥ_apply hg hA, withDensityᵥ_apply hh hA] using heq A hA4950omit [CompleteSpace E] in51set_option backward.isDefEq.respectTransparency false in52/-- A bounded linear image taking values in an RNP space admits a setwise density. -/53theorem exists_density_of_RNP_image {F : Type*}54    [NormedAddCommGroup F] [NormedSpace ℝ F]55    (hF : HasRadonNikodymProperty.{_, v} F) (T : E →L[ℝ] F)56    (hμ : μ univ < ∞) (ν : VectorMeasure Ω E) (hν : ν.variation univ < ∞)57    (hAC : ∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) :58    ∃ g : Ω → F, Integrable g μ ∧59      ∀ A : Set Ω, MeasurableSet A → T (ν A) = ∫ x in A, g x ∂μ := by60  refine hF Ω ‹MeasurableSpace Ω› μ hμ (RNPBridge.mapVectorMeasure T ν) ?_ ?_61  · exact RNPBridge.mapVectorMeasure_finite_variation T ν hν62  · intro A hA hz63    rw [RNPBridge.mapVectorMeasure_apply, hAC A hA hz, map_zero]6465/-- A finite-rank image of a finite-variation vector measure has a Bochner density. -/66theorem exists_density_of_finite_rank (P : E →L[ℝ] E)67    (hP : FiniteDimensional ℝ P.range) (hμ : μ univ < ∞)68    (ν : VectorMeasure Ω E) (hν : ν.variation univ < ∞)69    (hAC : ∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) :70    ∃ g : Ω → E, Integrable g μ ∧71      ∀ A : Set Ω, MeasurableSet A → P (ν A) = ∫ x in A, g x ∂μ := by72  let := hP73  have hRNP : HasRadonNikodymProperty.{u, v} P.range :=74    RNPBridge.hasRadonNikodymProperty_of_finiteDimensional P.range75  obtain ⟨g, hg, hrepr⟩ := exists_density_of_RNP_image hRNP P.rangeRestrict hμ ν hν hAC76  refine ⟨fun x => P.range.subtypeL (g x), P.range.subtypeL.integrable_comp hg, ?_⟩77  intro A hA78  rw [P.range.subtypeL.integral_comp_comm hg.integrableOn, ← hrepr A hA]79  rfl80/-- Nested operators force the corresponding densities to agree almost everywhere. -/81theorem densities_coherent (P : ℕ → E →L[ℝ] E)82    (hP : ∀ m n, m ≤ n → (P m).comp (P n) = P m)83    (ν : VectorMeasure Ω E) (g : ℕ → Ω → E)84    (hg : ∀ n, Integrable (g n) μ)85    (hrepr : ∀ n (A : Set Ω), MeasurableSet A → P n (ν A) = ∫ x in A, g n x ∂μ) :86    ∀ᵐ x ∂μ, ∀ m n, m ≤ n → P m (g n x) = g m x := by87  have hmn (m n : ℕ) (hmn : m ≤ n) : (fun x => P m (g n x)) =ᵐ[μ] g m := by88    apply ae_eq_of_setwise_integral_eq ((P m).integrable_comp (hg n)) (hg m)89    intro A hA90    rw [(P m).integral_comp_comm (hg n).integrableOn, ← hrepr n A hA, ← hrepr m A hA]91    exact congrArg (fun T : E →L[ℝ] E => T (ν A)) (hP m n hmn)92  rw [ae_all_iff]93  intro m94  rw [ae_all_iff]95  intro n96  by_cases h : m ≤ n97  · filter_upwards [hmn m n h] with x hx using fun _ => hx98  · exact Eventually.of_forall fun _ h' => (h h').elim99100omit [CompleteSpace E] in101/-- A common integrable bound turns bounded completeness into an integrable limit. -/102theorem exists_integrable_limit (P : ℕ → E →L[ℝ] E) (hP : BoundedlyComplete P)103    (g : ℕ → Ω → E) (hg : ∀ n, Integrable (g n) μ)104    (hcoh : ∀ᵐ x ∂μ, ∀ m n, m ≤ n → P m (g n x) = g m x)105    (b : Ω → ℝ) (hb : Integrable b μ)106    (hbound : ∀ n, ∀ᵐ x ∂μ, ‖g n x‖ ≤ b x) :107    ∃ f : Ω → E, Integrable f μ ∧108      (∀ᵐ x ∂μ, Tendsto (fun n => g n x) atTop (𝓝 (f x))) := by109  let f (x : Ω) := limUnder atTop (fun n => g n x)110  have hlim : ∀ᵐ x ∂μ, Tendsto (fun n => g n x) atTop (𝓝 (f x)) := by111    filter_upwards [hcoh, ae_all_iff.mpr hbound] with x hx hbx112    exact tendsto_nhds_limUnder (hP (fun n => g n x) hx ⟨b x, hbx⟩)113  have hmeas : AEStronglyMeasurable f μ :=114    aestronglyMeasurable_of_tendsto_ae atTop (fun n => (hg n).aestronglyMeasurable) hlim115  have hfb : ∀ᵐ x ∂μ, ‖f x‖ ≤ b x := by116    filter_upwards [hlim, ae_all_iff.mpr hbound] with x hx hbx117    exact le_of_tendsto hx.norm (Eventually.of_forall hbx)118  exact ⟨f, hb.mono' hmeas hfb, hlim⟩119120omit [CompleteSpace E] in121/-- Recover a vector measure from dominated densities of strongly convergent122projections. This is the analytic limit step of bounded-completeness implies RNP. -/123theorem exists_density_of_dominated_coherent_projections124    (P : ℕ → E →L[ℝ] E) (hP : BoundedlyComplete P)125    (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x))126    (ν : VectorMeasure Ω E) (g : ℕ → Ω → E) (hg : ∀ n, Integrable (g n) μ)127    (hrepr : ∀ n (A : Set Ω), MeasurableSet A → P n (ν A) = ∫ x in A, g n x ∂μ)128    (hcoh : ∀ᵐ x ∂μ, ∀ m n, m ≤ n → P m (g n x) = g m x)129    (b : Ω → ℝ) (hb : Integrable b μ)130    (hbound : ∀ n, ∀ᵐ x ∂μ, ‖g n x‖ ≤ b x) :131    ∃ f : Ω → E, Integrable f μ ∧132      ∀ A : Set Ω, MeasurableSet A → ν A = ∫ x in A, f x ∂μ := by133  obtain ⟨f, hf, hlim⟩ := exists_integrable_limit P hP g hg hcoh b hb hbound134  refine ⟨f, hf, fun A hA => ?_⟩135  have hi := tendsto_integral_of_dominated_convergence (μ := μ.restrict A) b136    (fun n => (hg n).integrableOn.aestronglyMeasurable) hb.integrableOn137    (fun n => ae_restrict_of_ae (hbound n)) (ae_restrict_of_ae hlim)138  have hp : Tendsto (fun n => ∫ x in A, g n x ∂μ) atTop (𝓝 (ν A)) := by139    simpa only [← hrepr _ A hA] using hstrong (ν A)140  exact tendsto_nhds_unique hp hi141142end Densities143/-- A boundedly complete finite-dimensional projection decomposition implies the144full reviewed vector-measure Radon–Nikodym property, for every source universe. -/145theorem hasRadonNikodymProperty_of_boundedlyCompleteDecomposition146    (D : BoundedlyCompleteDecomposition E) : HasRadonNikodymProperty.{u, v} E := by147  intro Ω mΩ148  let := mΩ149  intro μ hμ ν hν hAC150  let : IsFiniteMeasure μ := ⟨hμ⟩151  let : IsFiniteMeasure ν.variation := ⟨hν⟩152  have hdensity (n : ℕ) : ∃ g : Ω → E, Integrable g μ ∧153      ∀ A : Set Ω, MeasurableSet A → D.projection n (ν A) = ∫ x in A, g x ∂μ :=154    exists_density_of_finite_rank (D.projection n) (D.finiteDimensional n) hμ ν hν hAC155  choose g hg hrepr using hdensity156  obtain ⟨C, hC⟩ := D.uniformBound157  have hC0 : 0 ≤ C := (norm_nonneg (D.projection 0)).trans (hC 0)158  let b (x : Ω) : ℝ := C * (ν.variation.rnDeriv μ x).toReal159  have hderiv : Integrable (fun x => (ν.variation.rnDeriv μ x).toReal) μ := by160    simpa only [IntegrableOn, Measure.restrict_univ] using161      (Measure.integrableOn_toReal_rnDeriv (μ := ν.variation) (ν := μ) (s := univ) hν.ne)162  have hb : Integrable b μ := hderiv.const_mul C163  have hbound (n : ℕ) : ∀ᵐ x ∂μ, ‖g n x‖ ≤ b x := by164    apply VectorDensityBounds.ae_norm_map_density_le_rnDeriv μ ν hAC165      (D.projection n) (hg n) _ C hC0 (hC n)166    apply VectorMeasure.ext167    intro A hA168    rw [withDensityᵥ_apply (hg n) hA, RNPBridge.mapVectorMeasure_apply]169    exact (hrepr n A hA).symm170  exact exists_density_of_dominated_coherent_projections D.projection D.bounded_complete171    D.tendsto_identity ν g hg hrepr (densities_coherent D.projection D.nested ν g hg hrepr)172    b hb hbound173174/-- Failure of RNP rules out every decomposition satisfying these concrete properties. -/175theorem no_boundedlyCompleteDecomposition_of_not_RNP176    (hE : ¬ HasRadonNikodymProperty.{u, v} E) :177    IsEmpty (BoundedlyCompleteDecomposition E) :=178  ⟨fun D => hE (hasRadonNikodymProperty_of_boundedlyCompleteDecomposition D)⟩179180end PL1.DecompositionRNP181182183184185186187188189190191192193