PL1/EnfloStarbirdProjection.lean
All source files · Download exact source
SHA-256: 753dc567e9a082c112d47d447359f41ae1a72377310fd89ad048eb6aa92b90e6
1import PL1.WeakSchur2import Mathlib.Topology.Algebra.Module.Complement3import Mathlib.Analysis.Normed.Ring.Units45/-! # The projection and factorization step in the Enflo–Starbird route67This file proves the bounded inverse/projection construction from a quantitative8approximate left inverse. It does not assert the missing Enflo–Starbird9disjoint-tree extraction theorem for arbitrary L1 embeddings.10-/1112noncomputable section13set_option backward.isDefEq.respectTransparency false14namespace PL1.EnfloStarbird1516variable {𝕜 : Type*} [RCLike 𝕜]17variable {D : Type*} [NormedAddCommGroup D] [NormedSpace 𝕜 D]18variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]1920/-- A complemented copy described by its actual bounded embedding and retraction. -/21structure ComplementedCopy (𝕜 D E : Type*) [RCLike 𝕜]22 [NormedAddCommGroup D] [NormedSpace 𝕜 D]23 [NormedAddCommGroup E] [NormedSpace 𝕜 E] where24 embedding : D →L[𝕜] E25 retraction : E →L[𝕜] D26 left_inv : Function.LeftInverse retraction embedding2728namespace ComplementedCopy2930variable (C : ComplementedCopy 𝕜 D E)3132def projection : E →L[𝕜] E := C.embedding.comp C.retraction3334@[simp] theorem projection_apply (x : E) : C.projection x = C.embedding (C.retraction x) := rfl3536theorem isProjection : IsProjection C.projection := by37 ext x38 exact congrArg C.embedding (C.left_inv (C.retraction x))3940theorem range_projection : C.projection.range = C.embedding.range := by41 ext x42 constructor43 · rintro ⟨y, rfl⟩44 exact ⟨C.retraction y, rfl⟩45 · rintro ⟨y, rfl⟩46 exact ⟨C.embedding y, congrArg C.embedding (C.left_inv y)⟩4748theorem closedComplemented_range : C.embedding.range.ClosedComplemented :=49 C.embedding.closedComplemented_range_of_leftInverse C.retraction C.left_inv5051def rangeEquiv : D ≃L[𝕜] C.embedding.range :=52 ContinuousLinearEquiv.equivOfInverse C.embedding.rangeRestrict53 (C.retraction.comp C.embedding.range.subtypeL)54 C.left_inv (by55 rintro ⟨x, y, hy⟩56 apply Subtype.ext57 change C.embedding (C.retraction x) = x58 rw [← hy]59 exact congrArg C.embedding (C.left_inv y))6061include C in62theorem containsIsomorphicCopy : ContainsIsomorphicCopy 𝕜 D E :=63 ⟨C.embedding.range, C.closedComplemented_range.isClosed, ⟨C.rangeEquiv⟩⟩6465theorem norm_projection_le : ‖C.projection‖ ≤ ‖C.embedding‖ * ‖C.retraction‖ :=66 ContinuousLinearMap.opNorm_comp_le _ _6768end ComplementedCopy6970/-- The concrete maps are equivalent to the usual complemented-subspace definition. -/71theorem nonempty_complementedCopy_iff : Nonempty (ComplementedCopy 𝕜 D E) ↔72 ∃ V : Submodule 𝕜 E, V.ClosedComplemented ∧ Nonempty (D ≃L[𝕜] V) := by73 constructor74 · rintro ⟨C⟩75 exact ⟨C.embedding.range, C.closedComplemented_range, ⟨C.rangeEquiv⟩⟩76 · rintro ⟨V, ⟨P, hP⟩, ⟨e⟩⟩77 exact ⟨⟨V.subtypeL.comp e.toContinuousLinearMap,78 e.symm.toContinuousLinearMap.comp P,79 fun x => (congrArg e.symm (hP (e x))).trans (e.symm_apply_apply x)⟩⟩8081variable [CompleteSpace D]8283/-- Neumann-series correction of an approximate left inverse. -/84def correctedRetraction (J : D →L[𝕜] E) (R : E →L[𝕜] D)85 (h : ‖1 - R.comp J‖ < 1) : E →L[𝕜] D :=86 ((↑(Units.oneSub (1 - R.comp J) h)⁻¹ : D →L[𝕜] D)).comp R8788theorem correctedRetraction_left_inv (J : D →L[𝕜] E) (R : E →L[𝕜] D)89 (h : ‖1 - R.comp J‖ < 1) : Function.LeftInverse (correctedRetraction J R h) J := by90 let U := Units.oneSub (1 - R.comp J) h91 have hU : (↑U : D →L[𝕜] D) = R.comp J := by simp [U]92 have hi : (↑U⁻¹ : D →L[𝕜] D).comp (R.comp J) = ContinuousLinearMap.id 𝕜 D := by93 rw [← hU]94 exact U.inv_val95 intro x96 exact DFunLike.congr_fun hi x9798/-- An approximate inverse at distance below one produces a genuine complemented copy. -/99def complementedCopyOfApproximateInverse (J : D →L[𝕜] E) (R : E →L[𝕜] D)100 (h : ‖1 - R.comp J‖ < 1) : ComplementedCopy 𝕜 D E :=101 ⟨J, correctedRetraction J R h, correctedRetraction_left_inv J R h⟩102103theorem norm_correctedRetraction_le (J : D →L[𝕜] E) (R : E →L[𝕜] D)104 (h : ‖1 - R.comp J‖ < 1) :105 ‖correctedRetraction J R h‖ ≤ (1 - ‖1 - R.comp J‖)⁻¹ * ‖R‖ := by106 have hu : ‖(↑(Units.oneSub (1 - R.comp J) h)⁻¹ : D →L[𝕜] D)‖ ≤107 (1 - ‖1 - R.comp J‖)⁻¹ := by108 change ‖∑' n : ℕ, (1 - R.comp J) ^ n‖ ≤ _109 have hb := tsum_geometric_le_of_norm_lt_one (1 - R.comp J) h110 have h1 : ‖(1 : D →L[𝕜] D)‖ ≤ 1 := ContinuousLinearMap.norm_id_le111 linarith112 exact (ContinuousLinearMap.opNorm_comp_le _ _).trans113 (mul_le_mul_of_nonneg_right hu (norm_nonneg R))114115theorem norm_approximateInverse_projection_le (J : D →L[𝕜] E) (R : E →L[𝕜] D)116 (h : ‖1 - R.comp J‖ < 1) :117 ‖(complementedCopyOfApproximateInverse J R h).projection‖ ≤118 ‖J‖ * ((1 - ‖1 - R.comp J‖)⁻¹ * ‖R‖) :=119 (ComplementedCopy.norm_projection_le _).trans120 (mul_le_mul_of_nonneg_left (norm_correctedRetraction_le J R h) (norm_nonneg J))121122theorem closedComplemented_range_of_approximateInverse (J : D →L[𝕜] E)123 (R : E →L[𝕜] D) (h : ‖1 - R.comp J‖ < 1) : J.range.ClosedComplemented :=124 (complementedCopyOfApproximateInverse J R h).closedComplemented_range125126/-- Exact bounded factorization of the identity through the indicated operator. -/127def IdentityFactorsThrough (Q : E →L[𝕜] E) : Prop :=128 ∃ A : E →L[𝕜] D, ∃ B : D →L[𝕜] E,129 A.comp (Q.comp B) = ContinuousLinearMap.id 𝕜 D130131private theorem projection_fixes_range (Q : E →L[𝕜] E) (hQ : IsProjection Q)132 (y : Q.range) : Q (y : E) = y := by133 obtain ⟨z, hz⟩ := y.property134 rw [← hz]135 exact DFunLike.congr_fun hQ z136137omit [CompleteSpace D] in138/-- For a projection, identity factorization means exactly a complemented copy in its range. -/139theorem identityFactorsThrough_iff_complementedCopy_range (Q : E →L[𝕜] E)140 (hQ : IsProjection Q) : IdentityFactorsThrough (D := D) Q ↔141 Nonempty (ComplementedCopy 𝕜 D Q.range) := by142 constructor143 · rintro ⟨A, B, h⟩144 exact ⟨⟨Q.rangeRestrict.comp B, A.comp Q.range.subtypeL,145 fun x => DFunLike.congr_fun h x⟩⟩146 · rintro ⟨C⟩147 refine ⟨C.retraction.comp Q.rangeRestrict, Q.range.subtypeL.comp C.embedding, ?_⟩148 ext x149 change C.retraction ⟨Q (Q (C.embedding x)), _⟩ = x150 have hy : (⟨Q (Q (C.embedding x)), by exact ⟨Q (C.embedding x), rfl⟩⟩ : Q.range) =151 C.embedding x := by152 apply Subtype.ext153 exact (congrArg Q (projection_fixes_range Q hQ (C.embedding x))).trans154 (projection_fixes_range Q hQ (C.embedding x))155 rw [hy]156 exact C.left_inv x157158omit [CompleteSpace D] in159/-- The no-factorization conclusion rules out every complemented copy in the range. -/160theorem no_complementedCopy_range_of_no_factorization (Q : E →L[𝕜] E)161 (hQ : IsProjection Q) (h : ¬ IdentityFactorsThrough (D := D) Q) :162 ¬ Nonempty (ComplementedCopy 𝕜 D Q.range) :=163 fun hc => h ((identityFactorsThrough_iff_complementedCopy_range Q hQ).mpr hc)164165/-- A norm distance below one already implies exact factorization, by correcting the inverse. -/166theorem identityFactorsThrough_of_approximation (Q : E →L[𝕜] E)167 (A : E →L[𝕜] D) (B : D →L[𝕜] E)168 (h : ‖1 - A.comp (Q.comp B)‖ < 1) : IdentityFactorsThrough (D := D) Q := by169 refine ⟨correctedRetraction (Q.comp B) A h, B, ?_⟩170 ext x171 exact correctedRetraction_left_inv (Q.comp B) A h x172173/-- In a Banach domain, failure of exact factorization entails the sharp unit-distance barrier. -/174theorem one_le_norm_sub_of_no_factorization (Q : E →L[𝕜] E)175 (h : ¬ IdentityFactorsThrough (D := D) Q)176 (A : E →L[𝕜] D) (B : D →L[𝕜] E) :177 1 ≤ ‖1 - A.comp (Q.comp B)‖ := by178 by_contra hn179 exact h (identityFactorsThrough_of_approximation Q A B (lt_of_not_ge hn))180181#print axioms complementedCopyOfApproximateInverse182#print axioms norm_approximateInverse_projection_le183#print axioms nonempty_complementedCopy_iff184#print axioms identityFactorsThrough_iff_complementedCopy_range185#print axioms one_le_norm_sub_of_no_factorization186187end PL1.EnfloStarbird188