PL1/ProjectionRetract.lean
All source files · Download exact source
SHA-256: cfddd853d18199b0f17d8a162f25e6d4a56f853c4c75c95bbc3663dac53fe344
1import PL1.ProjectionTransport2import PL1.RNPBridge34/-! # Transporting a projection through a contractive retraction56An isometric embedding with a contractive left inverse suffices to put the7constructed projection on interval L1 while preserving its norm bound and range.8No isomorphism of the entire ambient spaces is required.9-/1011noncomputable section12namespace PL11314variable (𝕜 : Type*) [RCLike 𝕜]15variable (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E]16variable (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F]1718structure ContractiveRetract where19 embedding : E →ₗᵢ[𝕜] F20 retraction : F →L[𝕜] E21 left_inv : ∀ x, retraction (embedding x) = x22 norm_retraction_le : ‖retraction‖ ≤ 12324namespace ContractiveRetract25variable {𝕜 E F} (R : ContractiveRetract 𝕜 E F)2627def transport (P : E →L[𝕜] E) : F →L[𝕜] F :=28 R.embedding.toContinuousLinearMap.comp (P.comp R.retraction)2930@[simp] theorem transport_apply (P : E →L[𝕜] E) (x : F) :31 R.transport P x = R.embedding (P (R.retraction x)) := rfl3233theorem norm_transport_le (P : E →L[𝕜] E) : ‖R.transport P‖ ≤ ‖P‖ := by34 apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg P)35 intro x36 change ‖R.embedding (P (R.retraction x))‖ ≤ ‖P‖ * ‖x‖37 rw [R.embedding.norm_map]38 exact (P.le_opNorm _).trans (mul_le_mul_of_nonneg_left39 ((R.retraction.le_opNorm x).trans (by40 simpa only [one_mul] using mul_le_mul_of_nonneg_right R.norm_retraction_le (norm_nonneg x)))41 (norm_nonneg P))4243theorem isProjection {P : E →L[𝕜] E} (hP : IsProjection P) :44 IsProjection (R.transport P) := by45 ext x46 have h := DFunLike.congr_fun hP (R.retraction x)47 change P (P (R.retraction x)) = P (R.retraction x) at h48 change R.embedding (P (R.retraction (R.embedding (P (R.retraction x))))) = _49 rw [R.left_inv, h]50 rfl5152theorem isDunfordPettis {P : E →L[𝕜] E} (hP : IsDunfordPettis P) :53 IsDunfordPettis (R.transport P) :=54 (hP.comp_right R.retraction).comp_left R.embedding.toContinuousLinearMap5556def rangeForward (P : E →L[𝕜] E) : P.range →L[𝕜] (R.transport P).range :=57 (R.embedding.toContinuousLinearMap.comp P.range.subtypeL).codRestrict _ (by58 rintro ⟨x, y, hy⟩59 refine ⟨R.embedding y, ?_⟩60 change R.embedding (P (R.retraction (R.embedding y))) = R.embedding x61 rw [R.left_inv]62 exact congrArg R.embedding hy)6364def rangeBackward (P : E →L[𝕜] E) : (R.transport P).range →L[𝕜] P.range :=65 (R.retraction.comp (R.transport P).range.subtypeL).codRestrict _ (by66 rintro ⟨x, y, hy⟩67 refine ⟨R.retraction y, ?_⟩68 change P (R.retraction y) = R.retraction x69 rw [← hy]70 exact (R.left_inv _).symm)7172def rangeEquiv (P : E →L[𝕜] E) : P.range ≃L[𝕜] (R.transport P).range :=73 ContinuousLinearEquiv.equivOfInverse (R.rangeForward P) (R.rangeBackward P)74 (by75 intro x76 apply Subtype.ext77 exact R.left_inv x)78 (by79 rintro ⟨x, y, hy⟩80 apply Subtype.ext81 change R.embedding (R.retraction x) = x82 rw [← hy]83 change R.embedding (R.retraction (R.embedding (P (R.retraction y)))) = _84 rw [R.left_inv]85 rfl)8687theorem rangeEquiv_norm (P : E →L[𝕜] E) (x : P.range) :88 ‖R.rangeEquiv P x‖ = ‖x‖ := R.embedding.norm_map x8990theorem hasSchurProperty_range_iff (P : E →L[𝕜] E) :91 HasSchurProperty 𝕜 (R.transport P).range ↔ HasSchurProperty 𝕜 P.range :=92 (hasSchurProperty_equiv_iff (R.rangeEquiv P)).symm9394theorem containsIsomorphicCopy_range_iff95 {D : Type*} [NormedAddCommGroup D] [NormedSpace 𝕜 D] (P : E →L[𝕜] E) :96 ContainsIsomorphicCopy 𝕜 D (R.transport P).range ↔ ContainsIsomorphicCopy 𝕜 D P.range :=97 (containsIsomorphicCopy_equiv_iff (D := D) (R.rangeEquiv P)).symm9899theorem finiteDimensional_range_iff (P : E →L[𝕜] E) :100 FiniteDimensional 𝕜 (R.transport P).range ↔ FiniteDimensional 𝕜 P.range := by101 constructor102 · intro h103 let := h104 exact (R.rangeEquiv P).symm.toLinearEquiv.finiteDimensional105 · intro h106 let := h107 exact (R.rangeEquiv P).toLinearEquiv.finiteDimensional108109end ContractiveRetract110end PL1111