PL1/Ell1RNP.lean
All source files · Download exact source
SHA-256: dd159e74070cead450c63183ac3bbfe60557d830496b455a06d20f0bfd00aae4
1import PL1.ScalarDecompositionRNP2import PL1.L1Sum3import PL1.SingularResolvents4import PL1.RNPTransport56/-! # Full RNP of genuine scalar ℓ₁ and the resulting isomorphism obstruction -/78noncomputable section9universe u v10open Filter11open scoped Topology ENNReal BigOperators1213namespace PL1.Ell1RNP1415variable (K : Type*) [RCLike K]1617def coordinate (j : ℕ) : Ell1 K →L[K] Ell1 K :=18 (lp.singleContinuousLinearMap K (fun _ : ℕ => K) 1 j).comp19 (lp.evalCLM K (fun _ : ℕ => K) 1 j)2021def projection (N : ℕ) : Ell1 K →L[K] Ell1 K :=22 ∑ j ∈ Finset.range (N + 1), coordinate K j2324theorem projection_apply (N : ℕ) (x : Ell1 K) :25 projection K N x = ∑ j ∈ Finset.range (N + 1), lp.single 1 j (x j) := by26 simp only [projection, sum_apply, coordinate,27 ContinuousLinearMap.comp_apply, lp.singleContinuousLinearMap_apply]28 rfl2930theorem projection_apply_coordinate (N : ℕ) (x : Ell1 K) (j : ℕ) :31 projection K N x j = if j ≤ N then x j else 0 := by32 rw [projection_apply]33 simp only [lp.coeFn_sum, Finset.sum_apply, lp.coeFn_single, Finset.sum_pi_single,34 Finset.mem_range, Nat.lt_succ_iff]3536theorem projection_comp (m n : ℕ) (hmn : m ≤ n) :37 (projection K m).comp (projection K n) = projection K m := by38 ext x j39 simp only [ContinuousLinearMap.comp_apply, projection_apply_coordinate]40 by_cases hj : j ≤ m41 · simp [hj, hj.trans hmn]42 · simp [hj]4344def finiteSpan (N : ℕ) : Submodule K (Ell1 K) :=45 Submodule.span K ((fun j => lp.single 1 j (1 : K)) '' (Finset.range (N + 1) : Set ℕ))4647instance finiteDimensional_span (N : ℕ) : FiniteDimensional K (finiteSpan K N) :=48 FiniteDimensional.span_of_finite K49 ((Finset.finite_toSet (Finset.range (N + 1))).image _)5051theorem projection_mem_span (N : ℕ) (x : Ell1 K) : projection K N x ∈ finiteSpan K N := by52 rw [projection_apply]53 apply Submodule.sum_mem54 intro j hj55 have h : lp.single 1 j (1 : K) ∈ finiteSpan K N :=56 Submodule.subset_span ⟨j, hj, rfl⟩57 have hs := (finiteSpan K N).smul_mem (x j) h58 simpa only [← lp.single_smul, smul_eq_mul, mul_one] using hs5960instance finiteDimensional_range (N : ℕ) : FiniteDimensional K (projection K N).range := by61 have hle : (projection K N).range ≤ finiteSpan K N := by62 rintro x ⟨y, rfl⟩63 exact projection_mem_span K N y64 exact FiniteDimensional.of_injective (Submodule.inclusion hle)65 (Submodule.inclusion_injective _)6667theorem norm_projection_apply_le (N : ℕ) (x : Ell1 K) : ‖projection K N x‖ ≤ ‖x‖ := by68 rw [projection_apply]69 have h := lp.norm_sum_single (p := 1) (by norm_num) (fun j => x j)70 (Finset.range (N + 1))71 simp only [ENNReal.toReal_one, Real.rpow_one] at h72 rw [h, L1Sum.norm_eq_tsum]73 exact (L1Sum.summable_norm x).sum_le_tsum _ (fun _ _ => norm_nonneg _)7475theorem norm_projection_le (N : ℕ) : ‖projection K N‖ ≤ 1 :=76 ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by77 intro x78 simpa using norm_projection_apply_le K N x)7980theorem tendsto_projection (x : Ell1 K) :81 Tendsto (fun N => projection K N x) atTop (𝓝 x) := by82 simpa only [projection_apply, Function.comp_def] using83 ((lp.hasSum_single (p := 1) (by norm_num) x).tendsto_sum_nat.comp84 (tendsto_add_atTop_nat 1))8586theorem boundedlyComplete : ScalarDecompositionRNP.BoundedlyComplete (projection K) := by87 intro x hx hbounded88 obtain ⟨M, hM⟩ := hbounded89 let a : ℕ → K := fun j => x j j90 have hcoord (N j : ℕ) (hj : j ≤ N) : x N j = a j := by91 have h := congrArg (fun z : Ell1 K => z j) (hx j N hj)92 simpa only [projection_apply_coordinate, le_refl, ite_true] using h93 have hs : Summable (fun j => ‖a j‖) := by94 apply summable_of_sum_range_le (fun _ => norm_nonneg _) (c := M)95 intro N96 calc97 ∑ j ∈ Finset.range N, ‖a j‖ = ∑ j ∈ Finset.range N, ‖x N j‖ := by98 apply Finset.sum_congr rfl99 intro j hj100 rw [hcoord N j (Nat.le_of_lt (Finset.mem_range.mp hj))]101 _ ≤ ‖x N‖ := by102 rw [L1Sum.norm_eq_tsum]103 exact (L1Sum.summable_norm (x N)).sum_le_tsum _ (fun _ _ => norm_nonneg _)104 _ ≤ M := hM N105 let z : Ell1 K := ⟨a, memℓp_gen (by simpa using hs)⟩106 have heq (N : ℕ) : x N = projection K N z := by107 ext j108 rw [projection_apply_coordinate]109 by_cases hj : j ≤ N110 · simp only [hj, ite_true]111 exact hcoord N j hj112 · have h := congrArg (fun w : Ell1 K => w j) (hx N N le_rfl)113 simpa only [projection_apply_coordinate, hj, ite_false] using h.symm114 exact ⟨z, (tendsto_projection K z).congr' (Filter.Eventually.of_forall (fun N => (heq N).symm))⟩115116theorem hasRadonNikodymProperty :117 @PL1.HasRadonNikodymProperty.{_, v} (UnderlyingReal K (Ell1 K))118 (inferInstanceAs (NormedAddCommGroup (Ell1 K))) (NormedSpace.restrictScalars ℝ K (Ell1 K)) :=119 ScalarDecompositionRNP.hasRNP_of_scalar_projections (projection K)120 (finiteDimensional_range K) (projection_comp K) ⟨1, norm_projection_le K⟩121 (tendsto_projection K) (boundedlyComplete K)122123theorem not_isomorphic_of_not_RNP {E : Type u} [NormedAddCommGroup E] [NormedSpace K E]124 (hE : ¬ @PL1.HasRadonNikodymProperty.{u, 0} (UnderlyingReal K E)125 (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ K E)) :126 IsEmpty (E ≃L[K] Ell1 K) := by127 refine ⟨fun e => ?_⟩128 exact hE ((RNPTransport.hasRadonNikodymProperty_restrictScalars_iff e).mpr129 (hasRadonNikodymProperty K))130131theorem schur_intrinsic_not_isomorphic_ell1 :132 IsEmpty ((Noise.dyadicSystem K Noise.schurRates).IntrinsicSpace ≃L[K] Ell1 K) := by133 refine ⟨fun e => ?_⟩134 exact Noise.schur_intrinsic_not_RNP K135 ((RNPTransport.hasRadonNikodymProperty_restrictScalars_iff e).mpr136 (hasRadonNikodymProperty K))137138theorem constant_intrinsic_not_isomorphic_ell1 :139 IsEmpty ((Noise.dyadicSystem K Noise.constantRates).IntrinsicSpace ≃L[K] Ell1 K) := by140 refine ⟨fun e => ?_⟩141 exact Noise.constant_intrinsic_not_RNP K142 ((RNPTransport.hasRadonNikodymProperty_restrictScalars_iff e).mpr143 (hasRadonNikodymProperty K))144145theorem schur_projection_range_not_isomorphic_ell1 :146 IsEmpty ((Noise.projection K Noise.schurRates).range ≃L[K] Ell1 K) :=147 not_isomorphic_of_not_RNP K (Noise.schur_projection_range_not_RNP K)148149theorem constant_projection_range_not_isomorphic_ell1 :150 IsEmpty ((Noise.projection K Noise.constantRates).range ≃L[K] Ell1 K) :=151 not_isomorphic_of_not_RNP K (Noise.constant_projection_range_not_RNP K)152153end PL1.Ell1RNP154