PL1/ExplicitMartingaleWeak.lean

All source files · Download exact source

SHA-256: 7e8bfb7283b4a8dfbc43fa647b7bc6751650cfe2e404d81257e17749ef2c1fe5

1import PL1.ExplicitMartingale2import PL1.SchurExample3import PL1.WeakSequentialCompleteness4import PL1.RealSchur56/-! # Every explicit increasing-rate martingale trajectory fails to be weakly Cauchy78The conclusion quantifies over the entire continuous dual of the actual9intrinsic Banach space. In particular no countable set of weak tests replaces it.10-/1112noncomputable section13open Filter MeasureTheory14open scoped Topology ENNReal NNReal15namespace PL1.ExplicitMartingale16open Noise Walsh1718variable (K : Type*) [RCLike K]1920/-- The actual increasing-rate intrinsic space is weakly sequentially complete. -/21theorem schur_intrinsic_weaklySequentiallyComplete :22    IsWeaklySequentiallyComplete K (dyadicSystem K schurRates).IntrinsicSpace :=23  (schurRates_intrinsic_hasSchurProperty K).isWeaklySequentiallyComplete2425/-- Every trajectory of the explicit martingale fails the full-dual weak Cauchy test. -/26theorem schur_beta_not_weaklyCauchy (s : Walsh.Group) :27    ¬ WeaklyCauchy K (dyadicSystem K schurRates).IntrinsicSpace28      (fun m => beta K schurRates m s) := by29  intro h30  exact schur_beta_not_cauchy K s31    ((schurRates_intrinsic_hasSchurProperty K).cauchySeq_of_weaklyCauchy h)3233/-- Each trajectory has an actual continuous linear functional witnessing scalar non-Cauchyness. -/34theorem schur_beta_exists_dual_not_cauchy (s : Walsh.Group) :35    ∃ φ : (dyadicSystem K schurRates).IntrinsicSpace →L[K] K,36      ¬ CauchySeq (fun m => φ (beta K schurRates m s)) :=37  (schurRates_intrinsic_hasSchurProperty K).exists_dual_not_cauchy (schur_beta_not_cauchy K s)3839/-- A fixed positive scalar oscillation persists arbitrarily far along every trajectory. -/40theorem schur_beta_exists_dual_oscillation (s : Walsh.Group) :41    ∃ (φ : (dyadicSystem K schurRates).IntrinsicSpace →L[K] K) (ε : ℝ), 0 < ε ∧42      ∀ N : ℕ, ∃ m ≥ N, ∃ n ≥ N,43        ε ≤ ‖φ (beta K schurRates m s) - φ (beta K schurRates n s)‖ :=44  (schurRates_intrinsic_hasSchurProperty K).exists_dual_oscillation (schur_beta_not_cauchy K s)4546/-- The distinguished explicit sequence also fails to be weakly Cauchy. -/47theorem schur_sequence_not_weaklyCauchy :48    ¬ WeaklyCauchy K (dyadicSystem K schurRates).IntrinsicSpace (sequence K schurRates) :=49  schur_beta_not_weaklyCauchy K 15051/-- The same conclusion holds for the real continuous dual of either scalar-field construction. -/52theorem schur_beta_not_weaklyCauchy_real (s : Walsh.Group) :53    ¬ WeaklyCauchy ℝ (dyadicSystem K schurRates).IntrinsicSpace54      (fun m => beta K schurRates m s) := by55  have hS : HasSchurProperty ℝ (dyadicSystem K schurRates).IntrinsicSpace :=56    hasSchurProperty_iff_real.mp (schurRates_intrinsic_hasSchurProperty K)57  exact fun h => schur_beta_not_cauchy K s (hS.cauchySeq_of_weaklyCauchy h)5859#print axioms schur_intrinsic_weaklySequentiallyComplete60#print axioms schur_beta_not_weaklyCauchy61#print axioms schur_beta_exists_dual_oscillation62#print axioms schur_beta_not_weaklyCauchy_real63end PL1.ExplicitMartingale64