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

PL1/IntervalModel.lean

All source files · Download exact source

SHA-256: f6b04f146074d153fa084e548fab10a659cc4db07ee149fd871d14c329d46174

1import PL1.L1Sum2import PL1.WalshModel3import Mathlib.MeasureTheory.Integral.Prod4import Mathlib.MeasureTheory.Integral.Bochner.SumMeasure56/-!7# The countable disjoint-union L1 model89The construction below gives the actual isometry between an ell1 sum of L110spaces and L1 on counting measure times the original measure. The further11identification with interval Lebesgue L1 is a separate step.12-/1314noncomputable section15open MeasureTheory Set Filter16open scoped ENNReal NNReal Topology1718namespace PL1.IntervalModel1920variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]21variable (μ : Measure Ω) [SFinite μ]2223/-- The genuine measure on the countable disjoint union. -/24def disjointMeasure : Measure (ℕ × Ω) := Measure.count.prod μ2526abbrev SumSpace := L1Sum (Lp 𝕜 1 μ)27abbrev DisjointL1 := Lp 𝕜 1 (disjointMeasure μ)2829/-- Flatten the canonical representatives, one function on each component. -/30def flattenFunction (f : SumSpace (𝕜 := 𝕜) μ) (z : ℕ × Ω) : 𝕜 := f z.1 z.23132theorem measurable_flattenFunction (f : SumSpace (𝕜 := 𝕜) μ) :33    Measurable (flattenFunction μ f) :=34  measurable_from_prod_countable_right (fun n => (Lp.stronglyMeasurable (f n)).measurable)3536theorem integrable_flattenFunction (f : SumSpace (𝕜 := 𝕜) μ) :37    Integrable (flattenFunction μ f) (disjointMeasure μ) := by38  apply (integrable_prod_iff (measurable_flattenFunction μ f).aestronglyMeasurable).239  constructor40  · exact ae_of_all _ (fun n => L1.integrable_coeFn (f n))41  · simp only [flattenFunction, ← L1.norm_eq_integral_norm]42    apply integrable_count_iff.243    simpa only [norm_norm] using L1Sum.summable_norm f4445/-- The actual L1 class of the flattened function. -/46def flatten (f : SumSpace (𝕜 := 𝕜) μ) : DisjointL1 (𝕜 := 𝕜) μ :=47  (integrable_flattenFunction μ f).toL1 (flattenFunction μ f)4849theorem flatten_coeFn (f : SumSpace (𝕜 := 𝕜) μ) :50    (flatten μ f : ℕ × Ω → 𝕜) =ᵐ[disjointMeasure μ] flattenFunction μ f :=51  (integrable_flattenFunction μ f).coeFn_toL15253theorem norm_flatten (f : SumSpace (𝕜 := 𝕜) μ) : ‖flatten μ f‖ = ‖f‖ := by54  rw [L1.norm_eq_integral_norm]55  calc56    (∫ z, ‖flatten μ f z‖ ∂disjointMeasure μ) =57        ∫ z, ‖flattenFunction μ f z‖ ∂disjointMeasure μ :=58      integral_congr_ae ((flatten_coeFn μ f).fun_comp norm)59    _ = ∫ n, ∫ x, ‖f n x‖ ∂μ ∂Measure.count :=60      integral_prod _ (integrable_flattenFunction μ f).norm61    _ = ∑' n, ‖f n‖ := by62      simp only [← L1.norm_eq_integral_norm]63      rw [integral_countable (integrable_count_iff.2 (by64        simpa only [norm_norm] using L1Sum.summable_norm f))]65      simp66    _ = ‖f‖ := (L1Sum.norm_eq_tsum f).symm6768theorem flatten_add (f g : SumSpace (𝕜 := 𝕜) μ) :69    flatten μ (f + g) = flatten μ f + flatten μ g := by70  apply Lp.ext71  apply (flatten_coeFn μ (f + g)).trans72  apply EventuallyEq.trans _ (Lp.coeFn_add _ _).symm73  apply EventuallyEq.trans _ ((flatten_coeFn μ f).add (flatten_coeFn μ g)).symm74  apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun75    (measurable_flattenFunction μ (f + g))76    ((measurable_flattenFunction μ f).add (measurable_flattenFunction μ g)))).277  exact ae_of_all _ (fun n => Lp.coeFn_add (f n) (g n))7879theorem flatten_smul (c : 𝕜) (f : SumSpace (𝕜 := 𝕜) μ) :80    flatten μ (c • f) = c • flatten μ f := by81  apply Lp.ext82  apply (flatten_coeFn μ (c • f)).trans83  apply EventuallyEq.trans _ (Lp.coeFn_smul _ _).symm84  apply EventuallyEq.trans _ ((flatten_coeFn μ f).const_smul c).symm85  apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun86    (measurable_flattenFunction μ (c • f))87    ((measurable_flattenFunction μ f).const_smul c))).288  exact ae_of_all _ (fun n => Lp.coeFn_smul c (f n))8990/-- Isometric flattening into actual L1 on the countable disjoint union. -/91def flattenIsometry : SumSpace (𝕜 := 𝕜) μ →ₗᵢ[𝕜] DisjointL1 (𝕜 := 𝕜) μ where92  toFun := flatten μ93  map_add' := flatten_add μ94  map_smul' := by intro c f; exact flatten_smul μ c f95  norm_map' := norm_flatten μ9697/-- Each slice of an integrable function is integrable, since counting measure98has no nonempty null sets. -/99theorem integrable_slice (f : DisjointL1 (𝕜 := 𝕜) μ) (n : ℕ) :100    Integrable (fun x => f (n, x)) μ :=101  Measure.ae_count_iff.1 (L1.integrable_coeFn f).prod_right_ae n102103/-- Recover the nth actual L1 class. -/104def slice (f : DisjointL1 (𝕜 := 𝕜) μ) (n : ℕ) : Lp 𝕜 1 μ :=105  (integrable_slice μ f n).toL1 (fun x => f (n, x))106107theorem slice_coeFn (f : DisjointL1 (𝕜 := 𝕜) μ) (n : ℕ) :108    (slice μ f n : Ω → 𝕜) =ᵐ[μ] (fun x => f (n, x)) :=109  (integrable_slice μ f n).coeFn_toL1110111theorem norm_slice (f : DisjointL1 (𝕜 := 𝕜) μ) (n : ℕ) :112    ‖slice μ f n‖ = ∫ x, ‖f (n, x)‖ ∂μ := by113  rw [L1.norm_eq_integral_norm]114  exact integral_congr_ae ((slice_coeFn μ f n).fun_comp norm)115116theorem summable_norm_slice (f : DisjointL1 (𝕜 := 𝕜) μ) :117    Summable (fun n => ‖slice μ f n‖) := by118  have h := integrable_count_iff.1 (L1.integrable_coeFn f).integral_norm_prod_left119  simp only [norm_slice]120  convert h using 1121  ext n122  exact (Real.norm_of_nonneg (integral_nonneg (fun x => norm_nonneg (f (n, x))))).symm123124/-- Slicing gives an actual ell1 sequence of L1 classes. -/125def unflatten (f : DisjointL1 (𝕜 := 𝕜) μ) : SumSpace (𝕜 := 𝕜) μ :=126  ⟨slice μ f, by127    apply (memℓp_gen_iff (by simp : 0 < (1 : ℝ≥0∞).toReal)).2128    simpa using summable_norm_slice μ f⟩129130theorem flatten_unflatten (f : DisjointL1 (𝕜 := 𝕜) μ) : flatten μ (unflatten μ f) = f := by131  apply Lp.ext132  apply (flatten_coeFn μ (unflatten μ f)).trans133  apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun134    (measurable_flattenFunction μ (unflatten μ f)) (Lp.stronglyMeasurable f).measurable)).2135  exact ae_of_all _ (fun n => slice_coeFn μ f n)136137theorem unflatten_flatten (f : SumSpace (𝕜 := 𝕜) μ) : unflatten μ (flatten μ f) = f := by138  apply (flattenIsometry μ).injective139  exact flatten_unflatten μ (flatten μ f)140141/-- The actual surjective linear isometry between the ell1 sum and L1 on the142countable disjoint union. No isomorphism witness is assumed. -/143def sumDisjointEquiv : SumSpace (𝕜 := 𝕜) μ ≃ₗᵢ[𝕜] DisjointL1 (𝕜 := 𝕜) μ where144  toFun := flatten μ145  invFun := unflatten μ146  left_inv := unflatten_flatten μ147  right_inv := flatten_unflatten μ148  map_add' := flatten_add μ149  map_smul' := by intro c f; exact flatten_smul μ c f150  norm_map' := norm_flatten μ151152/-- Specialization to the actual Haar model used by both projection constructions. -/153def walshSumDisjointEquiv : L1Sum (Lp 𝕜 1 Walsh.haar) ≃ₗᵢ[𝕜]154    Lp 𝕜 1 ((Measure.count : Measure ℕ).prod Walsh.haar) :=155  sumDisjointEquiv Walsh.haar156157end PL1.IntervalModel158159160