PL1/NonSchurExample.lean

All source files · Download exact source

SHA-256: 39a73c7ab415cd041c9abec2bdf6babb4e7f03e421b7cef528b2b303422da767

1import PL1.ConcreteResolvents2import PL1.RademacherEmbedding3import PL1.EigenvectorEmbedding4import PL1.Ell2Schur5import PL1.DunfordPettis67/-!8# The concrete non-Schur projection on the countable sum of Haar L1910Constant coordinate rates make the entire closed first Walsh chaos a common11resolvent eigenspace. The explicit Rademacher embedding therefore lifts to the12intrinsic graph and the actual range of the constructed projection.13-/1415noncomputable section16set_option autoImplicit false17open MeasureTheory18open scoped ENNReal NNReal Topology1920namespace PL1.Noise2122open Walsh EigenvectorEmbedding ResolventEstimates2324variable (𝕜 : Type*) [RCLike 𝕜]2526theorem constantRates_firstChaos_eigen (n : ℕ) (a : Ell2 𝕜) :27    (dyadicSystem 𝕜 constantRates).operator n (rademacherL1 𝕜 a) =28      (((1 + (dyadicRatio ^ 2) ^ n)⁻¹ : ℝ) : 𝕜) • rademacherL1 𝕜 a := by29  apply rademacherL1_eigen30  intro j31  change resolventL1 𝕜 constantRates (dyadicTime n) (scalarCharacterLp 𝕜 1 {j}) = _32  simp [rateSum, constantRates, dyadicTime]3334theorem constantRates_intrinsic_contains_ell2 :35    ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) (dyadicSystem 𝕜 constantRates).IntrinsicSpace :=36  containsIsomorphicCopy_of_first_chaos (dyadicSystem 𝕜 constantRates).operator37    (rademacherL1 𝕜) (constantRates_firstChaos_eigen 𝕜) 16 (rademacherL1_lower 𝕜)3839theorem constantRates_projection_range_contains_ell2 :40    ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) (projection 𝕜 constantRates).range := by41  change ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) (dyadicSystem 𝕜 constantRates).projection.range42  rw [DyadicSystem.projection_range]43  exact constantRates_intrinsic_contains_ell2 𝕜4445theorem constantRates_projection_range_not_schur :46    ¬ HasSchurProperty 𝕜 (projection 𝕜 constantRates).range :=47  not_hasSchurProperty_of_contains_ell2 𝕜 (constantRates_projection_range_contains_ell2 𝕜)4849theorem constantRates_projection_range_infiniteDimensional :50    ¬ FiniteDimensional 𝕜 (projection 𝕜 constantRates).range := by51  intro h52  exact constantRates_projection_range_not_schur 𝕜 hasSchurProperty_of_finiteDimensional5354/-- The constructed constant-rate projection has the quantitative operator55bound and its actual closed range contains ell2 and fails the Schur property. -/56theorem constantRates_projection_spec :57    IsProjection (projection 𝕜 constantRates) ∧58      ‖projection 𝕜 constantRates‖ ≤ projectionBound ∧59      IsClosed ((projection 𝕜 constantRates).range : Set (L1Sum (Lp 𝕜 1 haar))) ∧60      ¬ FiniteDimensional 𝕜 (projection 𝕜 constantRates).range ∧61      ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) (projection 𝕜 constantRates).range ∧62      ¬ HasSchurProperty 𝕜 (projection 𝕜 constantRates).range :=63  ⟨projection_isProjection 𝕜 constantRates, norm_projection_le 𝕜 constantRates,64    projection_range_isClosed 𝕜 constantRates, constantRates_projection_range_infiniteDimensional 𝕜,65    constantRates_projection_range_contains_ell2 𝕜, constantRates_projection_range_not_schur 𝕜⟩6667theorem linearIndependent_rademacherL1 :68    LinearIndependent 𝕜 (fun j : ℕ => scalarCharacterLp 𝕜 1 {j}) := by69  have hinj : Function.Injective (l2ToL1 (𝕜 := 𝕜)) := by70    intro f g h71    apply Lp.ext72    exact (ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) f).symm.trans73      ((by rw [h] : l2ToL1 f =ᵐ[haar] l2ToL1 g).trans74        (ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) g))75  have hi := (orthonormal_rademacherL2 𝕜).linearIndependent.map' l2ToL1.toLinearMap76    (LinearMap.ker_eq_bot.mpr hinj)77  simpa only [Function.comp_def, ContinuousLinearMap.coe_coe,78    l2ToL1_scalarCharacter] using hi7980theorem linearIndependent_resolvent_rademacher (rates : ℕ → ℝ≥0) :81    LinearIndependent 𝕜 (fun j : ℕ =>82      resolventL1 𝕜 rates (dyadicTime 0) (scalarCharacterLp 𝕜 1 {j})) := by83  have hc (j : ℕ) : (((1 + (rates j : ℝ))⁻¹ : ℝ) : 𝕜) ≠ 0 := by84    exact_mod_cast inv_ne_zero (ne_of_gt (by positivity : 0 < 1 + (rates j : ℝ)))85  have hi := (linearIndependent_rademacherL1 𝕜).units_smul86    (fun j => Units.mk0 (((1 + (rates j : ℝ))⁻¹ : ℝ) : 𝕜) (hc j))87  change LinearIndependent 𝕜 (fun j =>88    (((1 + (rates j : ℝ))⁻¹ : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 {j}) at hi89  simpa only [resolventL1_scalarCharacter, dyadicTime, pow_zero,90    rateSum, Finset.sum_singleton, one_mul] using hi9192set_option backward.isDefEq.respectTransparency false in93/-- Every choice of nonnegative rates gives an infinite-dimensional intrinsic94space: its zeroth reconstruction column retains independent Rademacher vectors. -/95theorem intrinsic_infiniteDimensional (rates : ℕ → ℝ≥0) :96    ¬ FiniteDimensional 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace := by97  intro hfinite98  let v : ℕ → (dyadicSystem 𝕜 rates).IntrinsicSpace := fun j =>99    (dyadicSystem 𝕜 rates).column 0 (scalarCharacterLp 𝕜 1 {j})100  have hi : LinearIndependent 𝕜 v := by101    apply LinearIndependent.of_comp102      (IntrinsicGraph.evalZero (dyadicSystem 𝕜 rates).analysis).toLinearMap103    change LinearIndependent 𝕜 (fun j =>104      IntrinsicGraph.evalZero (dyadicSystem 𝕜 rates).analysis105        ((dyadicSystem 𝕜 rates).column 0 (scalarCharacterLp 𝕜 1 {j})))106    simp only [DyadicSystem.evalZero_column]107    exact linearIndependent_resolvent_rademacher 𝕜 rates108  exact Module.Finite.not_linearIndependent_of_infinite v hi109110theorem projection_range_infiniteDimensional (rates : ℕ → ℝ≥0) :111    ¬ FiniteDimensional 𝕜 (projection 𝕜 rates).range := by112  change ¬ FiniteDimensional 𝕜 (dyadicSystem 𝕜 rates).projection.range113  rw [DyadicSystem.projection_range]114  exact intrinsic_infiniteDimensional 𝕜 rates115116end PL1.Noise117