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

PL1/EigenvectorEmbedding.lean

All source files · Download exact source

SHA-256: 2811367342c34103480a8f024e49da65b4e4bc360ff752ab79e0b0b175c55c64

1import PL1.IntrinsicGraph2import PL1.ResolventEstimates3import Mathlib.Analysis.Normed.Operator.Banach45/-!6# Lifting a common eigenspace into the intrinsic graph78The analytic lifting step of the non-Schur construction. A bounded-below map9into the base space lifts to a closed isomorphic copy in the intrinsic graph10when its weighted coordinates have a uniform summable bound. Specializing to11the common resolvent eigenvalue `a = 1` gives the first-chaos mechanism.12The concrete Rademacher map from `ell2` is not assumed to have been constructed.13-/1415noncomputable section16set_option maxHeartbeats 80000017open scoped BigOperators NNReal1819namespace PL1.EigenvectorEmbedding2021open IntrinsicGraph ResolventEstimates2223variable {𝕜 H Y : Type*} [RCLike 𝕜]24  [NormedAddCommGroup H] [NormedSpace 𝕜 H]25  [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]2627section GeneralLift2829variable (D : ℕ → Y →L[𝕜] Y) (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)30  (T : H →L[𝕜] Y) (hs : ∀ x, Summable (fun n => ‖D n (T x)‖))3132/-- The algebraic lift of a map whose coordinate norms are summable. -/33def liftLinear : H →ₗ[𝕜] Space D where34  toFun x := ofSummable D h0 (T x) (hs x)35  map_add' x y := by36    apply evalZero_injective D37    simp only [map_add, evalZero_ofSummable]38  map_smul' c x := by39    apply evalZero_injective D40    simp only [map_smul, evalZero_ofSummable, RingHom.id_apply]4142/-- A uniform coordinate-sum estimate makes the lift continuous. -/43def lift (C : ℝ) (hC : ∀ x, (∑' n, ‖D n (T x)‖) ≤ C * ‖x‖) :44    H →L[𝕜] Space D :=45  (liftLinear D h0 T hs).mkContinuous C (fun x => by46    change ‖ofSummable D h0 (T x) (hs x)‖ ≤ C * ‖x‖47    rw [norm_ofSummable]48    exact hC x)4950variable (C : ℝ) (hC : ∀ x, (∑' n, ‖D n (T x)‖) ≤ C * ‖x‖)5152@[simp]53theorem evalZero_lift (x : H) : evalZero D (lift D h0 T hs C hC x) = T x :=54  evalZero_ofSummable D h0 (T x) (hs x)5556@[simp]57theorem coord_lift (n : ℕ) (x : H) : coord D n (lift D h0 T hs C hC x) = D n (T x) := rfl5859theorem norm_lift_eq (x : H) :60    ‖lift D h0 T hs C hC x‖ = ∑' n, ‖D n (T x)‖ :=61  norm_ofSummable D h0 (T x) (hs x)6263theorem norm_base_le_lift (x : H) : ‖T x‖ ≤ ‖lift D h0 T hs C hC x‖ := by64  simpa only [evalZero_lift] using norm_evalZero_le D (lift D h0 T hs C hC x)6566theorem lift_antilipschitz (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :67    AntilipschitzWith K (lift D h0 T hs C hC) := by68  apply ContinuousLinearMap.antilipschitz_of_bound69  intro x70  exact (hT x).trans (mul_le_mul_of_nonneg_left (norm_base_le_lift D h0 T hs C hC x) K.coe_nonneg)7172theorem lift_isClosed_range [CompleteSpace H] (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :73    IsClosed ((lift D h0 T hs C hC).range : Set (Space D)) :=74  (lift_antilipschitz D h0 T hs C hC K hT).isClosed_range75    (lift D h0 T hs C hC).uniformContinuous7677/-- The lifted embedding is a genuine continuous linear equivalence onto its closed range. -/78def liftEquivRange [CompleteSpace H] [CompleteSpace Y]79    (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :80    H ≃L[𝕜] (lift D h0 T hs C hC).range :=81  (lift D h0 T hs C hC).equivRange82    (lift_antilipschitz D h0 T hs C hC K hT).injective83    (lift_isClosed_range D h0 T hs C hC K hT)8485include h0 hs C hC in86theorem containsIsomorphicCopy_of_coordinate_bound [CompleteSpace H] [CompleteSpace Y]87    (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :88    PL1.ContainsIsomorphicCopy 𝕜 H (Space D) :=89  ⟨(lift D h0 T hs C hC).range,90    lift_isClosed_range D h0 T hs C hC K hT,91    ⟨liftEquivRange D h0 T hs C hC K hT⟩⟩9293end GeneralLift9495section ScalarCoordinates9697variable (D : ℕ → Y →L[𝕜] Y) (T : H →L[𝕜] Y) (α : ℕ → 𝕜)98  (hα : Summable (fun n => ‖α n‖))99  (heigen : ∀ n x, D n (T x) = α n • T x)100101include heigen102103include hα in104theorem scalar_coordinates_summable (x : H) : Summable (fun n => ‖D n (T x)‖) := by105  simpa only [heigen, norm_smul] using hα.mul_right ‖T x‖106107theorem scalar_coordinates_tsum (x : H) :108    (∑' n, ‖D n (T x)‖) = (∑' n, ‖α n‖) * ‖T x‖ := by109  simp only [heigen, norm_smul, tsum_mul_right]110111theorem scalar_coordinates_bound (x : H) :112    (∑' n, ‖D n (T x)‖) ≤ ((∑' n, ‖α n‖) * ‖T‖) * ‖x‖ := by113  rw [scalar_coordinates_tsum D T α heigen]114  calc115    _ ≤ (∑' n, ‖α n‖) * (‖T‖ * ‖x‖) :=116      mul_le_mul_of_nonneg_left (T.le_opNorm x) (tsum_nonneg (fun n => norm_nonneg _))117    _ = _ := by ring118119include hα in120theorem containsIsomorphicCopy_of_scalar_coordinates [CompleteSpace H] [CompleteSpace Y]121    (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)122    (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :123    PL1.ContainsIsomorphicCopy 𝕜 H (Space D) :=124  containsIsomorphicCopy_of_coordinate_bound D h0 T125    (scalar_coordinates_summable D T α hα heigen)126    ((∑' n, ‖α n‖) * ‖T‖)127    (scalar_coordinates_bound D T α heigen) K hT128129end ScalarCoordinates130131/-- The scalar resolvent multiplier on a common eigenspace with eigenvalue `a`. -/132def dyadicEigenvalue (a : ℝ) (n : ℕ) : ℝ := (1 + (dyadicRatio ^ 2) ^ n * a)⁻¹133134/-- The resulting eigenvalues of the weighted intrinsic coordinate operators. -/135def intrinsicEigenCoefficient (a : ℝ) : ℕ → ℝ136  | 0 => 1137  | n + 1 => a * dyadicRatio ^ (n + 1) / (1 + (dyadicRatio ^ 2) ^ (n + 1) * a)138139theorem dyadic_eigen_denominator_pos (a : ℝ) (ha : 0 ≤ a) (n : ℕ) :140    0 < 1 + (dyadicRatio ^ 2) ^ n * a := by141  have hp : 0 ≤ (dyadicRatio ^ 2) ^ n := pow_nonneg (sq_nonneg _) _142  positivity143144theorem intrinsicEigenCoefficient_nonneg (a : ℝ) (ha : 0 ≤ a) (n : ℕ) :145    0 ≤ intrinsicEigenCoefficient a n := by146  cases n with147  | zero => exact zero_le_one148  | succ n =>149    exact div_nonneg (mul_nonneg ha (pow_nonneg dyadicRatio_nonneg _))150      (dyadic_eigen_denominator_pos a ha _).le151152theorem intrinsicEigenCoefficient_le (a : ℝ) (ha : 0 ≤ a) (n : ℕ) :153    intrinsicEigenCoefficient a (n + 1) ≤ a * dyadicRatio ^ (n + 1) := by154  change a * dyadicRatio ^ (n + 1) / (1 + (dyadicRatio ^ 2) ^ (n + 1) * a) ≤ _155  apply (div_le_iff₀ (dyadic_eigen_denominator_pos a ha _)).2156  apply le_mul_of_one_le_right (mul_nonneg ha (pow_nonneg dyadicRatio_nonneg _))157  exact le_add_of_nonneg_right (mul_nonneg (pow_nonneg (sq_nonneg _) _) ha)158159theorem intrinsicEigenCoefficient_tail_summable (a : ℝ) (ha : 0 ≤ a) :160    Summable (fun n => intrinsicEigenCoefficient a (n + 1)) :=161  (geometric_tail_summable.mul_left a).of_nonneg_of_le162    (fun n => intrinsicEigenCoefficient_nonneg a ha (n + 1))163    (intrinsicEigenCoefficient_le a ha)164165theorem intrinsicEigenCoefficient_summable (a : ℝ) (ha : 0 ≤ a) :166    Summable (intrinsicEigenCoefficient a) :=167  (summable_nat_add_iff 1).1 (intrinsicEigenCoefficient_tail_summable a ha)168169theorem intrinsicEigenCoefficient_norm_summable (a : ℝ) (ha : 0 ≤ a) :170    Summable (fun n => ‖(intrinsicEigenCoefficient a n : 𝕜)‖) := by171  simpa only [RCLike.norm_ofReal, abs_of_nonneg (intrinsicEigenCoefficient_nonneg a ha _)] using172    intrinsicEigenCoefficient_summable a ha173174/-- An explicit upper bound for the change from base norm to intrinsic norm. -/175def eigenNormBound (a : ℝ) : ℝ := 1 + a * dyadicRatio / (1 - dyadicRatio)176177theorem eigenNormBound_nonneg (a : ℝ) (ha : 0 ≤ a) : 0 ≤ eigenNormBound a := by178  unfold eigenNormBound179  exact add_nonneg zero_le_one180    (div_nonneg (mul_nonneg ha dyadicRatio_nonneg) one_sub_dyadicRatio_pos.le)181182theorem intrinsicEigenCoefficient_tsum_le (a : ℝ) (ha : 0 ≤ a) :183    (∑' n, intrinsicEigenCoefficient a n) ≤ eigenNormBound a := by184  rw [(intrinsicEigenCoefficient_summable a ha).tsum_eq_zero_add]185  change 1 + (∑' n, intrinsicEigenCoefficient a (n + 1)) ≤ _186  calc187    _ ≤ 1 + (∑' n, a * dyadicRatio ^ (n + 1)) :=188      add_le_add le_rfl (Summable.tsum_le_tsum (intrinsicEigenCoefficient_le a ha)189        (intrinsicEigenCoefficient_tail_summable a ha) (geometric_tail_summable.mul_left a))190    _ = eigenNormBound a := by rw [tsum_mul_left, geometric_tail_tsum]; unfold eigenNormBound; ring191192theorem intrinsicEigenCoefficient_norm_tsum_le (a : ℝ) (ha : 0 ≤ a) :193    (∑' n, ‖(intrinsicEigenCoefficient a n : 𝕜)‖) ≤ eigenNormBound a := by194  simpa only [RCLike.norm_ofReal, abs_of_nonneg (intrinsicEigenCoefficient_nonneg a ha _)] using195    intrinsicEigenCoefficient_tsum_le a ha196197/-- Cancellation between the dyadic weight and the defect of a resolvent multiplier. -/198theorem intrinsicEigenCoefficient_eq_weighted_defect (a : ℝ) (ha : 0 ≤ a) (n : ℕ) :199    intrinsicEigenCoefficient a (n + 1) =200      (dyadicRatio ^ (n + 1))⁻¹ * (1 - dyadicEigenvalue a (n + 1)) := by201  unfold intrinsicEigenCoefficient dyadicEigenvalue202  rw [dyadicRatio_sq_pow]203  have hd : 1 + (dyadicRatio ^ (n + 1)) ^ 2 * a ≠ 0 := by204    rw [← dyadicRatio_sq_pow]205    exact ne_of_gt (dyadic_eigen_denominator_pos a ha _)206  field_simp [dyadicRatio_pow_ne_zero, ne_of_gt dyadicRatio_pos, hd]207  ring208209section CommonEigenspace210211variable (S : ℕ → Y →L[𝕜] Y) (T : H →L[𝕜] Y) (a : ℝ) (ha : 0 ≤ a)212  (heigen : ∀ n x, S n (T x) = (dyadicEigenvalue a n : 𝕜) • T x)213214include ha heigen215216theorem analysisCoordinate_eigen (n : ℕ) (x : H) :217    analysisCoordinate S n (T x) = (intrinsicEigenCoefficient a n : 𝕜) • T x := by218  cases n with219  | zero => simp [analysisCoordinate, intrinsicEigenCoefficient]220  | succ n =>221    simp only [analysisCoordinate, smul_apply, sub_apply, ContinuousLinearMap.id_apply, heigen]222    rw [intrinsicEigenCoefficient_eq_weighted_defect a ha n,223      RCLike.ofReal_mul, RCLike.ofReal_sub, RCLike.ofReal_one, mul_smul, sub_smul, one_smul]224225theorem dyadic_coordinates_summable (x : H) :226    Summable (fun n => ‖analysisCoordinate S n (T x)‖) :=227  scalar_coordinates_summable (analysisCoordinate S) T228    (fun n => (intrinsicEigenCoefficient a n : 𝕜))229    (intrinsicEigenCoefficient_norm_summable a ha) (analysisCoordinate_eigen S T a ha heigen) x230231theorem dyadic_coordinates_tsum_le (x : H) :232    (∑' n, ‖analysisCoordinate S n (T x)‖) ≤ eigenNormBound a * ‖T x‖ := by233  rw [scalar_coordinates_tsum (analysisCoordinate S) T234    (fun n => (intrinsicEigenCoefficient a n : 𝕜)) (analysisCoordinate_eigen S T a ha heigen)]235  exact mul_le_mul_of_nonneg_right (intrinsicEigenCoefficient_norm_tsum_le a ha) (norm_nonneg _)236237theorem dyadic_coordinates_bound (x : H) :238    (∑' n, ‖analysisCoordinate S n (T x)‖) ≤ (eigenNormBound a * ‖T‖) * ‖x‖ :=239  (dyadic_coordinates_tsum_le S T a ha heigen x).trans (by240    rw [mul_assoc]241    exact mul_le_mul_of_nonneg_left (T.le_opNorm x) (eigenNormBound_nonneg a ha))242243/-- The bounded lift of a common eigenspace into the actual intrinsic graph. -/244def commonEigenvectorLift : H →L[𝕜] Space (analysisCoordinate S) :=245  lift (analysisCoordinate S) rfl T (dyadic_coordinates_summable S T a ha heigen)246    (eigenNormBound a * ‖T‖) (dyadic_coordinates_bound S T a ha heigen)247248@[simp]249theorem evalZero_commonEigenvectorLift (x : H) :250    evalZero (analysisCoordinate S) (commonEigenvectorLift S T a ha heigen x) = T x :=251  evalZero_lift _ _ _ _ _ _ x252253theorem commonEigenvectorLift_norm_bounds (x : H) :254    ‖T x‖ ≤ ‖commonEigenvectorLift S T a ha heigen x‖ ∧255      ‖commonEigenvectorLift S T a ha heigen x‖ ≤ eigenNormBound a * ‖T x‖ := by256  constructor257  · exact norm_base_le_lift _ _ _ _ _ _ x258  · rw [norm_eq_tsum_operators, evalZero_commonEigenvectorLift]259    exact dyadic_coordinates_tsum_le S T a ha heigen x260261/-- A common eigenspace that is a Banach-space copy in the base space remains262a closed Banach-space copy with the intrinsic norm. -/263theorem containsIsomorphicCopy_of_common_eigenspace [CompleteSpace H] [CompleteSpace Y]264    (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :265    PL1.ContainsIsomorphicCopy 𝕜 H (Space (analysisCoordinate S)) :=266  containsIsomorphicCopy_of_coordinate_bound (analysisCoordinate S) rfl T267    (dyadic_coordinates_summable S T a ha heigen)268    (eigenNormBound a * ‖T‖) (dyadic_coordinates_bound S T a ha heigen) K hT269270end CommonEigenspace271272/-- The intrinsic norm bound for the first-chaos eigenvalue is exactly `2 + √2`. -/273theorem eigenNormBound_one : eigenNormBound 1 = 2 + Real.sqrt 2 := by274  unfold eigenNormBound275  field_simp [ne_of_gt one_sub_dyadicRatio_pos]276  rw [dyadicRatio_eq_sqrt_div_two]277  have hs := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)278  nlinarith279280/-- The first-chaos lifting statement needed in Theorem B. -/281theorem containsIsomorphicCopy_of_first_chaos [CompleteSpace H] [CompleteSpace Y]282    (S : ℕ → Y →L[𝕜] Y) (T : H →L[𝕜] Y)283    (heigen : ∀ n x, S n (T x) = (((1 + (dyadicRatio ^ 2) ^ n)⁻¹ : ℝ) : 𝕜) • T x)284    (K : ℝ≥0) (hT : ∀ x, ‖x‖ ≤ K * ‖T x‖) :285    PL1.ContainsIsomorphicCopy 𝕜 H (Space (analysisCoordinate S)) :=286  containsIsomorphicCopy_of_common_eigenspace S T 1 (by norm_num)287    (by simpa [dyadicEigenvalue] using heigen) K hT288289/-- The same conclusion using the customary positive lower norm bound. -/290theorem containsIsomorphicCopy_of_common_eigenspace_boundedBelow291    [CompleteSpace H] [CompleteSpace Y]292    (S : ℕ → Y →L[𝕜] Y) (T : H →L[𝕜] Y) (a : ℝ) (ha : 0 ≤ a)293    (heigen : ∀ n x, S n (T x) = (dyadicEigenvalue a n : 𝕜) • T x)294    (b : ℝ) (hb : 0 < b) (hT : ∀ x, b * ‖x‖ ≤ ‖T x‖) :295    PL1.ContainsIsomorphicCopy 𝕜 H (Space (analysisCoordinate S)) := by296  apply containsIsomorphicCopy_of_common_eigenspace S T a ha heigen297    ⟨b⁻¹, inv_nonneg.2 hb.le⟩298  intro x299  change ‖x‖ ≤ b⁻¹ * ‖T x‖300  calc301    ‖x‖ = b⁻¹ * (b * ‖x‖) := by rw [← mul_assoc, inv_mul_cancel₀ (ne_of_gt hb), one_mul]302    _ ≤ b⁻¹ * ‖T x‖ := mul_le_mul_of_nonneg_left (hT x) (inv_nonneg.2 hb.le)303304end PL1.EigenvectorEmbedding305