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

PL1/DyadicProjection.lean

All source files · Download exact source

SHA-256: bfec0e898577aad5ad80bc622431437167efd5bd59e22a24d12a6af07974668f

1import PL1.IntrinsicGraph2import PL1.L1Sum3import PL1.ResolventEstimates4import PL1.WeakSchur56/-!7# The projection constructed from a dyadic resolvent system89The operator hypotheses are the precise conclusions required from the10resolvent construction. Under these hypotheses we construct the intrinsic11Banach space as a closed graph in the actual countable ell1 sum, its12reconstruction map, and the projection. This conditional construction does13not assert that either of the paper's measure-theoretic resolvent families14has yet been constructed.15-/1617noncomputable section18open Filter19open scoped Topology BigOperators2021namespace PL12223open ResolventEstimates2425/-- The analytic properties of the dyadic resolvents used in the construction. -/26structure DyadicSystem (𝕜 Y : Type*) [RCLike 𝕜]27    [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] where28  operator : ℕ → Y →L[𝕜] Y29  contractive : ∀ n, ‖operator n‖ ≤ 130  commute : ∀ i j, (operator i).comp (operator j) = (operator j).comp (operator i)31  resolvent : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - operator i).comp (operator j) =32    (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •33      (operator i).comp (ContinuousLinearMap.id 𝕜 Y - operator j)34  strong : ∀ y, Tendsto (fun n => operator n y) atTop (𝓝 y)3536namespace DyadicSystem3738variable {𝕜 Y : Type*} [RCLike 𝕜]39  [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]4041variable (S : DyadicSystem 𝕜 Y)4243/-- The weighted defect operators that define the intrinsic norm. -/44abbrev analysis := analysisCoordinate S.operator4546/-- The unweighted underlying reconstruction columns. -/47abbrev baseColumn := synthesisCoordinate S.operator4849/-- The actual intrinsic graph normed space. -/50abbrev IntrinsicSpace := IntrinsicGraph.Space S.analysis5152/-- Its isometric embedding into the actual countable ell1 sum. -/53abbrev inclusion : S.IntrinsicSpace →ₗᵢ[𝕜] L1Sum Y :=54  IntrinsicGraph.inclusion S.analysis5556/-- A reconstruction column, with its codomain equipped with the intrinsic norm. -/57def column (j : ℕ) : Y →L[𝕜] S.IntrinsicSpace :=58  IntrinsicGraph.column S.analysis rfl (S.baseColumn j)59    (weighted_column_apply_norm_summable S.operator S.contractive S.resolvent j)60    projectionBound61    (weighted_column_apply_norm_tsum_le S.operator S.contractive S.resolvent j)6263theorem projectionBound_nonneg : 0 ≤ projectionBound := by64  unfold projectionBound65  positivity6667theorem norm_column_le (j : ℕ) : ‖S.column j‖ ≤ projectionBound :=68  IntrinsicGraph.norm_column_le _ _ _ _ _ _ projectionBound_nonneg6970@[simp]71theorem evalZero_column (j : ℕ) (y : Y) :72    IntrinsicGraph.evalZero S.analysis (S.column j y) = S.baseColumn j y :=73  IntrinsicGraph.evalZero_column _ _ _ _ _ _ _7475@[simp]76theorem coord_column (i j : ℕ) (y : Y) :77    IntrinsicGraph.coord S.analysis i (S.column j y) = S.analysis i (S.baseColumn j y) := rfl7879variable [CompleteSpace Y]8081/-- The bounded map K from the ambient ell1 sum to the intrinsic Banach space. -/82def reconstruction : L1Sum Y →L[𝕜] S.IntrinsicSpace :=83  L1Sum.synthesis S.column projectionBound S.norm_column_le8485theorem norm_reconstruction_le : ‖S.reconstruction‖ ≤ projectionBound :=86  L1Sum.norm_synthesis_le _ _ _ projectionBound_nonneg8788@[simp]89theorem reconstruction_apply (x : L1Sum Y) :90    S.reconstruction x = ∑' j, S.column j (x j) := rfl9192@[simp]93theorem reconstruction_single (j : ℕ) (y : Y) :94    S.reconstruction (lp.single 1 j y) = S.column j y :=95  L1Sum.synthesis_single _ _ _ _ _9697/-- The underlying Y-valued reconstruction series is the formula in the paper. -/98theorem evalZero_reconstruction (x : L1Sum Y) :99    IntrinsicGraph.evalZero S.analysis (S.reconstruction x) =100      ∑' j, S.baseColumn j (x j) := by101  rw [reconstruction_apply,102    (IntrinsicGraph.evalZero S.analysis).map_tsum103      (L1Sum.summable_columns S.column projectionBound S.norm_column_le x)]104  simp only [evalZero_column]105106/-- The candidate matrix projection is J composed with K. -/107def projection : L1Sum Y →L[𝕜] L1Sum Y :=108  S.inclusion.toContinuousLinearMap.comp S.reconstruction109110theorem norm_projection_le : ‖S.projection‖ ≤ projectionBound := by111  apply ContinuousLinearMap.opNorm_le_bound _ projectionBound_nonneg112  intro x113  change ‖S.inclusion (S.reconstruction x)‖ ≤ projectionBound * ‖x‖114  rw [S.inclusion.norm_map]115  exact S.reconstruction.le_opNorm x |>.trans116    (mul_le_mul_of_nonneg_right S.norm_reconstruction_le (norm_nonneg _))117118/-- Every matrix block is exactly the weighted resolvent formula. -/119theorem projection_single_coord (i j : ℕ) (y : Y) :120    S.projection (lp.single 1 j y) i = S.analysis i (S.baseColumn j y) := by121  change IntrinsicGraph.coord S.analysis i122    (S.reconstruction (lp.single 1 j y)) = _123  rw [reconstruction_single, coord_column]124125/-- The zeroth matrix block is S0, the resolvent at time one. -/126theorem projection_zero_zero (y : Y) :127    S.projection (lp.single 1 0 y) 0 = S.operator 0 y := by128  rw [projection_single_coord]129  rfl130131/-- Absolute convergence permits reconstruction, and the finite sums telescope132to the strongly convergent dyadic resolvents. Thus KJ is the identity. -/133theorem reconstruction_inclusion (x : S.IntrinsicSpace) :134    S.reconstruction (S.inclusion x) = x := by135  apply IntrinsicGraph.evalZero_injective S.analysis136  rw [evalZero_reconstruction]137  have hs := L1Sum.summable_columns S.baseColumn 1138    (synthesisCoordinate_norm_le_one S.operator S.contractive) (S.inclusion x)139  have ht := hs.hasSum.tendsto_sum_nat.comp (tendsto_add_atTop_nat 1)140  have heq (N : ℕ) :141      (∑ j ∈ Finset.range (N + 1), S.baseColumn j (S.inclusion x j)) =142        S.operator N (IntrinsicGraph.evalZero S.analysis x) := by143    calc144      _ = ∑ j ∈ Finset.range (N + 1),145          S.baseColumn j (S.analysis j (IntrinsicGraph.evalZero S.analysis x)) := by146            apply Finset.sum_congr rfl147            intro j _148            rw [show S.inclusion x j =149              S.analysis j (IntrinsicGraph.evalZero S.analysis x) from x.property j]150      _ = _ := weighted_composition_partial_sum_apply151        S.operator S.commute S.resolvent N _152  have ht' : Tendsto153      (fun N => S.operator N (IntrinsicGraph.evalZero S.analysis x)) atTop154      (𝓝 (∑' j, S.baseColumn j (S.inclusion x j))) := by155    change Tendsto (fun N => ∑ j ∈ Finset.range (N + 1),156      S.baseColumn j (S.inclusion x j)) atTop _ at ht157    simpa only [heq] using ht158  exact tendsto_nhds_unique ht' (S.strong _)159160theorem reconstruction_comp_inclusion :161    S.reconstruction.comp S.inclusion.toContinuousLinearMap =162      ContinuousLinearMap.id 𝕜 S.IntrinsicSpace := by163  apply ContinuousLinearMap.ext164  intro x165  exact S.reconstruction_inclusion x166167theorem reconstruction_surjective : Function.Surjective S.reconstruction :=168  fun x => ⟨S.inclusion x, S.reconstruction_inclusion x⟩169170/-- The constructed operator is an actual bounded projection. -/171theorem isProjection : IsProjection S.projection := by172  apply ContinuousLinearMap.ext173  intro x174  change S.inclusion (S.reconstruction (S.inclusion (S.reconstruction x))) =175    S.inclusion (S.reconstruction x)176  rw [reconstruction_inclusion]177178/-- Its range is precisely the intrinsic graph, with the inherited ell1 norm. -/179theorem projection_range : S.projection.range = IntrinsicGraph.graph S.analysis := by180  ext x181  constructor182  · rintro ⟨y, rfl⟩183    exact (S.reconstruction y).property184  · intro hx185    refine ⟨x, ?_⟩186    change S.inclusion (S.reconstruction (S.inclusion ⟨x, hx⟩)) = x187    rw [reconstruction_inclusion]188    rfl189190theorem isClosed_projection_range : IsClosed (S.projection.range : Set (L1Sum Y)) :=191  S.isProjection.isClosed_range192193/-- The quantitative operator conclusion of Proposition 4.2, conditional only194on the stated analytic properties of the dyadic resolvents. -/195theorem projection_spec :196    IsProjection S.projection ∧ ‖S.projection‖ ≤ projectionBound ∧197      S.projection.range = IntrinsicGraph.graph S.analysis ∧198      IsClosed (S.projection.range : Set (L1Sum Y)) ∧199      (∀ y, S.projection (lp.single 1 0 y) 0 = S.operator 0 y) :=200  ⟨S.isProjection, S.norm_projection_le, S.projection_range,201    S.isClosed_projection_range, S.projection_zero_zero⟩202203end DyadicSystem204end PL1205