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

PL1/ALDyadicEmbedding.lean

All source files · Download exact source

SHA-256: 313c446c2a448652cfdf9cdb10a130b1ee072b41696698708cc262c971269e33

1import PL1.ALFragments2import PL1.BalancedFragmentTree3import PL1.DyadicL1Coordinates4import PL1.Definitions5import Mathlib.Analysis.Normed.Operator.Completeness6import Mathlib.Logic.Equiv.Fin.Basic78/-! The interval L1 copy generated by an atomless balanced fragment tree. -/9noncomputable section10set_option backward.isDefEq.respectTransparency false11open scoped BigOperators Topology12open Filter13namespace PL1.ALDyadicEmbedding14open PL1.BalancedFragmentTree PL1.FiniteSumming PL1.DyadicTrace PL1.ALOrder1516/-- Binary word ordering matching the interval children 2i and 2i+1. -/17def wordEquiv : (n : ℕ) → Fin (2 ^ n) ≃ Word n18  | 0 => {19      toFun := fun _ i => Fin.elim0 i20      invFun := fun _ => 021      left_inv := fun i => by apply Fin.ext; have hi := i.isLt; norm_num at hi; omega22      right_inv := fun _ => Subsingleton.elim _ _ }23  | n + 1 => (finCongr (pow_succ 2 n)).trans24      ((finProdFinEquiv.symm.trans (Equiv.prodCongr (wordEquiv n) finTwoEquiv)).trans25        (snocEquiv n))2627def childIndex (n : ℕ) (i : Fin (2 ^ n)) (b : Bool) : Fin (2 ^ (n + 1)) :=28  (finCongr (pow_succ 2 n)).symm (finProdFinEquiv (i, finTwoEquiv.symm b))2930@[simp] theorem wordEquiv_childIndex (n : ℕ) (i : Fin (2 ^ n)) (b : Bool) :31    wordEquiv (n + 1) (childIndex n i b) = Fin.snoc (wordEquiv n i) b := by32  simp only [wordEquiv, childIndex, Equiv.trans_apply, Equiv.apply_symm_apply,33    Equiv.symm_apply_apply, Equiv.prodCongr_apply]34  simp [snocEquiv]3536@[simp] theorem childIndex_false_val (n : ℕ) (i : Fin (2 ^ n)) :37    (childIndex n i false).val = 2 * i.val := by38  simp only [childIndex, finCongr_symm_apply_coe]39  simp [finProdFinEquiv, finTwoEquiv]4041@[simp] theorem childIndex_true_val (n : ℕ) (i : Fin (2 ^ n)) :42    (childIndex n i true).val = 2 * i.val + 1 := by43  simp only [childIndex, finCongr_symm_apply_coe]44  simp [finProdFinEquiv, finTwoEquiv, Nat.add_comm]4546variable {E : Type*} [NormedAddCommGroup E] [Lattice E]47  [IsOrderedAddMonoid E] [NormedVectorLattice E]4849theorem exists_balancedSplit_of_atomless [CompleteSpace E] (hAL : ALRenorming.IsALNorm E)50    (u : E) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u) :51    ∃ split : E → E, IsBalancedSplit (normFunctional hAL) u split := by52  apply exists_balancedSplit53  intro x hx hxu54  exact ALFragments.exists_half_fragment hAL (normFunctional hAL)55    (normFunctional_strictlyPositive hAL) hx56    (fun a ha hax => hna a ha (hax.trans hxu))5758def node (u : E) (split : E → E) (n : ℕ) (i : Fin (2 ^ n)) : E :=59  BalancedFragmentTree.cell u split n (wordEquiv n i)6061omit [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] in62theorem node_children_add (u : E) (split : E → E) (n : ℕ) (i : Fin (2 ^ n)) :63    node u split (n + 1) (childIndex n i false) +64      node u split (n + 1) (childIndex n i true) = node u split n i := by65  simp only [node, wordEquiv_childIndex, cell_children_add]6667theorem node_nonneg {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}68    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split)69    (n : ℕ) (i : Fin (2 ^ n)) : 0 ≤ node u split n i :=70  (cell_mem_Icc hu hs n _).17172theorem norm_node {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}73    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split)74    (n : ℕ) (i : Fin (2 ^ n)) : ‖node u split n i‖ = ‖u‖ / (2 : ℝ)^n := by75  rw [← normFunctional_nonneg hAL (node_nonneg hu hs n i)]76  exact (cell_phi hu hs n _).trans (by rw [normFunctional_nonneg hAL hu])7778theorem node_disjoint {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}79    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (n : ℕ) :80    Pairwise (fun i j : Fin (2 ^ n) => IsVLDisjoint (node u split n i) (node u split n j)) :=81  fun _ _ hij => cell_pairwise_disjoint hu hs n (fun h => hij ((wordEquiv n).injective h))8283def treeSynthesis (u : E) (split : E → E) (n : ℕ) : EllOne (2 ^ n) →L[ℝ] E :=84  ∑ i : Fin (2 ^ n), (PiLp.proj 1 (fun _ : Fin (2 ^ n) => ℝ) i).smulRight85    ((2 : ℝ)^n • node u split n i)8687theorem treeSynthesis_apply (u : E) (split : E → E) (n : ℕ) (x : EllOne (2 ^ n)) :88    treeSynthesis u split n x = ∑ i, ((2 : ℝ)^n * x i) • node u split n i := by89  simp [treeSynthesis, smul_smul, mul_comm]9091theorem norm_treeSynthesis {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}92    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split)93    (n : ℕ) (x : EllOne (2 ^ n)) : ‖treeSynthesis u split n x‖ = ‖u‖ * ‖x‖ := by94  rw [treeSynthesis_apply, ← norm_abs_eq_norm]95  rw [← normFunctional_nonneg hAL (abs_nonneg _),96    abs_sum_smul_disjoint _ _ (node_disjoint hu hs n), map_sum]97  simp only [map_smul, smul_eq_mul, abs_of_nonneg (node_nonneg hu hs n _)]98  simp_rw [normFunctional_nonneg hAL (node_nonneg hu hs n _), norm_node hu hs]99  rw [norm_ellOne, Finset.mul_sum]100  apply Finset.sum_congr rfl101  intro i _102  rw [abs_mul, abs_of_nonneg (pow_nonneg (by norm_num : (0 : ℝ) ≤ 2) n)]103  field_simp104105 theorem norm_treeSynthesis_le {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}106    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (n : ℕ) :107    ‖treeSynthesis u split n‖ ≤ ‖u‖ := by108  apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg u)109  intro x110  exact (norm_treeSynthesis hu hs n x).le111112113114115116117open PL1.DyadicL1Coordinates118119theorem synthesis_single (n : ℕ) (i : Fin (2 ^ n)) :120    synthesis n (PiLp.single 1 i 1) = normalizedVector n i := by121  rw [synthesis_apply]122  simp [PiLp.single_apply]123124theorem treeSynthesis_single (u : E) (split : E → E) (n : ℕ) (i : Fin (2 ^ n)) :125    treeSynthesis u split n (PiLp.single 1 i 1) = (2 : ℝ)^n • node u split n i := by126  rw [treeSynthesis_apply]127  simp [PiLp.single_apply]128129def treeApprox (u : E) (split : E → E) (n : ℕ) : IntervalL1 ℝ →L[ℝ] E :=130  (treeSynthesis u split n).comp (analysis n)131132theorem treeApprox_normalizedVector (u : E) (split : E → E) (n : ℕ) (i : Fin (2 ^ n)) :133    treeApprox u split n (normalizedVector n i) = (2 : ℝ)^n • node u split n i := by134  rw [← synthesis_single n i]135  change treeSynthesis u split n (analysis n (synthesis n _)) = _136  rw [analysis_synthesis, treeSynthesis_single]137138theorem treeApprox_vector (u : E) (split : E → E) (n : ℕ) (i : Fin (2 ^ n)) :139    treeApprox u split n (dyadicVector n i) = node u split n i := by140  have hp : (2 : ℝ)^n ≠ 0 := pow_ne_zero _ (by norm_num)141  have he : dyadicVector (𝕜 := ℝ) n i = ((2 : ℝ)^n)⁻¹ • normalizedVector n i := by142    simp [normalizedVector, smul_smul, hp]143  rw [he, map_smul, treeApprox_normalizedVector, smul_smul, inv_mul_cancel₀ hp, one_smul]144145theorem norm_treeApprox {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}146    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split)147    (n : ℕ) (f : IntervalL1 ℝ) : ‖treeApprox u split n f‖ = ‖u‖ * ‖dyadicAverage n f‖ := by148  change ‖treeSynthesis u split n (analysis n f)‖ = _149  rw [norm_treeSynthesis hu hs, ← norm_synthesis n (analysis n f), synthesis_analysis]150151theorem norm_treeApprox_le {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}152    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (n : ℕ) :153    ‖treeApprox u split n‖ ≤ ‖u‖ := by154  calc155    _ ≤ ‖treeSynthesis u split n‖ * ‖analysis n‖ := ContinuousLinearMap.opNorm_comp_le _ _156    _ ≤ ‖u‖ * ‖analysis n‖ := mul_le_mul_of_nonneg_right (norm_treeSynthesis_le hu hs n) (norm_nonneg _)157    _ ≤ ‖u‖ * 1 := mul_le_mul_of_nonneg_left (norm_analysis_le_one n) (norm_nonneg _)158    _ = _ := mul_one _159160theorem treeApprox_stable_vector (u : E) (split : E → E) {n m : ℕ} (hnm : n ≤ m)161    (i : Fin (2 ^ n)) : treeApprox u split m (dyadicVector n i) = node u split n i := by162  induction hnm using Nat.decreasingInduction with163  | self => exact treeApprox_vector u split m i164  | of_succ n hn ih =>165    have h0 := ih (childIndex n i false)166    have h1 := ih (childIndex n i true)167    calc168      _ = treeApprox u split m169          (dyadicVector (n + 1) (childIndex n i false) +170            dyadicVector (n + 1) (childIndex n i true)) := by171        rw [childIndex_false_val, childIndex_true_val, ← dyadicVector_refine]172      _ = node u split (n + 1) (childIndex n i false) +173          node u split (n + 1) (childIndex n i true) := by rw [map_add, h0, h1]174      _ = _ := node_children_add u split n i175176theorem treeApprox_average_self (u : E) (split : E → E) (n : ℕ) (f : IntervalL1 ℝ) :177    treeApprox u split n (dyadicAverage n f) = treeApprox u split n f := by178  rw [← synthesis_analysis]179  change treeSynthesis u split n (analysis n (synthesis n (analysis n f))) = _180  rw [analysis_synthesis]181  rfl182183theorem treeApprox_stable_average (u : E) (split : E → E) {n m : ℕ} (hnm : n ≤ m)184    (f : IntervalL1 ℝ) : treeApprox u split m (dyadicAverage n f) = treeApprox u split n f := by185  rw [← treeApprox_average_self u split n f]186  rw [dyadicAverage, PartitionAverages.average_apply, map_sum, map_sum]187  simp_rw [map_smul]188  apply Finset.sum_congr rfl189  intro i hi190  have hi' : i < 2 ^ n := Finset.mem_range.mp hi191  rw [treeApprox_stable_vector u split hnm ⟨i, hi'⟩,192    treeApprox_vector u split n ⟨i, hi'⟩]193194195196197198theorem treeApprox_cauchy {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}199    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (f : IntervalL1 ℝ) :200    CauchySeq (fun n => treeApprox u split n f) := by201  apply Metric.cauchySeq_iff'.mpr202  intro ε hε203  have ht : Tendsto (fun n => ‖u‖ * ‖f - dyadicAverage n f‖) atTop (𝓝 0) := by204    simpa only [sub_self, norm_zero, mul_zero] using205      (((tendsto_const_nhds (x := f)).sub (dyadicAverage_tendsto f)).norm).const_mul ‖u‖206  obtain ⟨N, hN⟩ := (ht.eventually_lt_const hε).exists207  refine ⟨N, fun n hn => ?_⟩208  calc209    _ = ‖treeApprox u split n (f - dyadicAverage N f)‖ := by210      rw [dist_eq_norm, map_sub, treeApprox_stable_average u split hn f]211    _ ≤ ‖treeApprox u split n‖ * ‖f - dyadicAverage N f‖ := ContinuousLinearMap.le_opNorm _ _212    _ ≤ ‖u‖ * ‖f - dyadicAverage N f‖ :=213      mul_le_mul_of_nonneg_right (norm_treeApprox_le hu hs n) (norm_nonneg _)214    _ < ε := hN215216variable [CompleteSpace E]217218def treeLimit {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}219    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (f : IntervalL1 ℝ) : E :=220  (cauchySeq_tendsto_of_complete (treeApprox_cauchy hu hs f)).choose221222theorem treeLimit_tendsto {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}223    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (f : IntervalL1 ℝ) :224    Tendsto (fun n => treeApprox u split n f) atTop (𝓝 (treeLimit hu hs f)) :=225  (cauchySeq_tendsto_of_complete (treeApprox_cauchy hu hs f)).choose_spec226227def treeEmbedding {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}228    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) : IntervalL1 ℝ →L[ℝ] E :=229  ContinuousLinearMap.ofTendstoOfBoundedRange (treeLimit hu hs) (treeApprox u split)230    (tendsto_pi_nhds.mpr (treeLimit_tendsto hu hs))231    (isBounded_iff_forall_norm_le.mpr ⟨‖u‖, by232      rintro _ ⟨n, rfl⟩233      exact norm_treeApprox_le hu hs n⟩)234235theorem treeEmbedding_tendsto {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}236    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (f : IntervalL1 ℝ) :237    Tendsto (fun n => treeApprox u split n f) atTop (𝓝 (treeEmbedding hu hs f)) :=238  treeLimit_tendsto hu hs f239240theorem norm_treeEmbedding {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}241    (hu : 0 ≤ u) (hs : IsBalancedSplit (normFunctional hAL) u split) (f : IntervalL1 ℝ) :242    ‖treeEmbedding hu hs f‖ = ‖u‖ * ‖f‖ := by243  apply tendsto_nhds_unique (treeEmbedding_tendsto hu hs f).norm244  have ht := ((dyadicAverage_tendsto f).norm).const_mul ‖u‖245  simpa only [norm_treeApprox hu hs] using ht246247/-- The fragment tree yields a genuine isometry of the actual interval L1 norm. -/248def treeIsometry {hAL : ALRenorming.IsALNorm E} {u : E} {split : E → E}249    (hu : 0 < u) (hs : IsBalancedSplit (normFunctional hAL) u split) : IntervalL1 ℝ →ₗᵢ[ℝ] E where250  toLinearMap := ((‖u‖⁻¹ : ℝ) • treeEmbedding hu.le hs).toLinearMap251  norm_map' f := by252    have hn : ‖u‖ ≠ 0 := norm_ne_zero_iff.mpr (ne_of_gt hu)253    change ‖(‖u‖⁻¹ : ℝ) • treeEmbedding hu.le hs f‖ = ‖f‖254    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (inv_nonneg.mpr (norm_nonneg u)),255      norm_treeEmbedding, ← mul_assoc, inv_mul_cancel₀ hn, one_mul]256257theorem containsIsomorphicCopy_of_atomless_vector (hAL : ALRenorming.IsALNorm E)258    (u : E) (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u) :259    ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E := by260  obtain ⟨split, hs⟩ := exists_balancedSplit_of_atomless hAL u hna261  let J := treeIsometry hu hs262  have hc : IsClosed (J.toContinuousLinearMap.range : Set E) := J.isometry.isClosedEmbedding.isClosed_range263  exact ⟨J.toContinuousLinearMap.range, hc,264    ⟨J.toContinuousLinearMap.equivRange J.injective hc⟩⟩265266theorem containsIsomorphicCopy_of_not_atomic (hAL : ALRenorming.IsALNorm E)267    (hna : ¬ IsAtomicLattice E) : ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E := by268  rw [IsAtomicLattice] at hna269  push Not at hna270  obtain ⟨u, hu, hna⟩ := hna271  exact containsIsomorphicCopy_of_atomless_vector hAL u hu (fun a ha hau => hna a ha hau)272273#print axioms containsIsomorphicCopy_of_atomless_vector274#print axioms containsIsomorphicCopy_of_not_atomic275end PL1.ALDyadicEmbedding276277