PL1/ProjectionTransport.lean
All source files · Download exact source
SHA-256: d1b189cec742f13de9a4aa2e3e91432067e30a1aa137299e426417913470697c
1import PL1.WeakSchur2import Mathlib.Analysis.Normed.Operator.NormedSpace34/-!5# Transport of projection properties along Banach-space isomorphisms67This is the abstract transport step needed after constructing the projection on8an auxiliary space and identifying that space with the actual interval L1.9An arbitrary continuous linear equivalence transports the range properties;10a linear isometry equivalence additionally preserves the exact operator norm.11-/1213noncomputable section1415namespace PL11617variable {𝕜 : Type*} [RCLike 𝕜]18variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]19variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]20variable {D : Type*} [NormedAddCommGroup D] [NormedSpace 𝕜 D]2122/-- Conjugating an operator by a continuous linear equivalence. -/23def conjugateOperator (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) : F →L[𝕜] F :=24 e.toContinuousLinearMap.comp (P.comp e.symm.toContinuousLinearMap)2526@[simp]27theorem conjugateOperator_apply (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) (x : F) :28 conjugateOperator e P x = e (P (e.symm x)) := rfl2930@[simp]31theorem conjugateOperator_symm (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) :32 conjugateOperator e.symm (conjugateOperator e P) = P := by33 ext x34 simp3536/-- Conjugating a projection produces a projection. -/37theorem IsProjection.conjugate {P : E →L[𝕜] E} (hP : IsProjection P)38 (e : E ≃L[𝕜] F) : IsProjection (conjugateOperator e P) := by39 ext x40 have h := DFunLike.congr_fun hP (e.symm x)41 change P (P (e.symm x)) = P (e.symm x) at h42 simp only [ContinuousLinearMap.comp_apply, conjugateOperator_apply,43 ContinuousLinearEquiv.symm_apply_apply, h]4445theorem isProjection_conjugate_iff (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) :46 IsProjection (conjugateOperator e P) ↔ IsProjection P := by47 constructor48 · intro h49 simpa using h.conjugate e.symm50 · exact fun h => h.conjugate e5152/-- Conjugation preserves the Dunford–Pettis property. -/53theorem IsDunfordPettis.conjugate {P : E →L[𝕜] E} (hP : IsDunfordPettis P)54 (e : E ≃L[𝕜] F) : IsDunfordPettis (conjugateOperator e P) :=55 (hP.comp_right e.symm.toContinuousLinearMap).comp_left e.toContinuousLinearMap5657theorem isDunfordPettis_conjugate_iff (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) :58 IsDunfordPettis (conjugateOperator e P) ↔ IsDunfordPettis P := by59 constructor60 · intro h61 simpa using h.conjugate e.symm62 · exact fun h => h.conjugate e6364/-- The range of the transported operator is exactly the image of the old range. -/65theorem conjugateOperator_range (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) :66 P.range.map e.toLinearMap = (conjugateOperator e P).range := by67 ext x68 constructor69 · rintro ⟨y, ⟨z, hz⟩, hy⟩70 change P z = y at hz71 change e y = x at hy72 refine ⟨e z, ?_⟩73 change e (P (e.symm (e z))) = x74 simpa only [ContinuousLinearEquiv.symm_apply_apply, hz] using hy75 · rintro ⟨z, hz⟩76 refine ⟨P (e.symm z), ⟨e.symm z, rfl⟩, ?_⟩77 exact hz7879/-- The original and transported ranges are continuously linearly equivalent. -/80def conjugateRangeEquiv (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) :81 P.range ≃L[𝕜] (conjugateOperator e P).range :=82 e.ofSubmodules _ _ (conjugateOperator_range e P)8384theorem hasSchurProperty_conjugate_range_iff (e : E ≃L[𝕜] F)85 (P : E →L[𝕜] E) :86 HasSchurProperty 𝕜 (conjugateOperator e P).range ↔87 HasSchurProperty 𝕜 P.range :=88 (hasSchurProperty_equiv_iff (conjugateRangeEquiv e P)).symm8990theorem isClosed_conjugate_range_iff (e : E ≃L[𝕜] F) (P : E →L[𝕜] E) :91 IsClosed ((conjugateOperator e P).range : Set F) ↔92 IsClosed (P.range : Set E) := by93 rw [← conjugateOperator_range, Submodule.map_coe]94 exact e.isClosed_image9596/-- Finite dimensionality of the actual range is unchanged by conjugation. -/97theorem finiteDimensional_conjugate_range_iff (e : E ≃L[𝕜] F)98 (P : E →L[𝕜] E) :99 FiniteDimensional 𝕜 (conjugateOperator e P).range ↔100 FiniteDimensional 𝕜 P.range := by101 constructor102 · intro h103 let := h104 exact (conjugateRangeEquiv e P).symm.toLinearEquiv.finiteDimensional105 · intro h106 let := h107 exact (conjugateRangeEquiv e P).toLinearEquiv.finiteDimensional108109/-- Isomorphic-copy containment is invariant under an isomorphism of ambient spaces. -/110theorem ContainsIsomorphicCopy.map (h : ContainsIsomorphicCopy 𝕜 D E)111 (e : E ≃L[𝕜] F) : ContainsIsomorphicCopy 𝕜 D F := by112 obtain ⟨V, hclosed, ⟨f⟩⟩ := h113 refine ⟨V.map e.toLinearMap, ?_, ⟨f.trans (e.submoduleMap V)⟩⟩114 rw [Submodule.map_coe]115 exact e.isClosed_image.mpr hclosed116117theorem containsIsomorphicCopy_equiv_iff (e : E ≃L[𝕜] F) :118 ContainsIsomorphicCopy 𝕜 D E ↔ ContainsIsomorphicCopy 𝕜 D F :=119 ⟨fun h => h.map e, fun h => h.map e.symm⟩120121theorem containsIsomorphicCopy_conjugate_range_iff (e : E ≃L[𝕜] F)122 (P : E →L[𝕜] E) :123 ContainsIsomorphicCopy 𝕜 D (conjugateOperator e P).range ↔124 ContainsIsomorphicCopy 𝕜 D P.range :=125 (containsIsomorphicCopy_equiv_iff (D := D) (conjugateRangeEquiv e P)).symm126127/-- Isometric conjugation preserves the exact operator norm, including on the zero space. -/128theorem norm_conjugateOperator_isometry (e : E ≃ₗᵢ[𝕜] F) (P : E →L[𝕜] E) :129 ‖conjugateOperator e.toContinuousLinearEquiv P‖ = ‖P‖ := by130 change ‖(e : E →L[𝕜] F).comp (P.comp (e.symm : F →L[𝕜] E))‖ = ‖P‖131 simp only [ContinuousLinearMap.opNorm_linearIsometryEquiv_comp,132 ContinuousLinearMap.opNorm_comp_linearIsometryEquiv]133134end PL1135