PL1/IntrinsicNonBoundedComplete.lean

All source files · Download exact source

SHA-256: 6e23cf347c04261985fdf578c2c57529bd4aed506d0385e6083eb7b8a8738fe1

1import PL1.IntrinsicWalshBlocks2import PL1.SingularResolvents3import PL1.DecompositionRNP4import PL1.ScalarDecompositionRNP5import PL1.UnconditionalRNP6import PL1.SchurExample78/-! # Failure of bounded completeness for the actual intrinsic Walsh decompositions -/910noncomputable section11open MeasureTheory Filter12open scoped ENNReal NNReal Topology BigOperators1314namespace PL1.Noise1516open DecompositionRNP1718theorem intrinsic_not_boundedlyComplete_real (rates : ℕ → ℝ≥0)19    (hRNP : ¬ HasRadonNikodymProperty.{_, 0} (dyadicSystem ℝ rates).IntrinsicSpace) :20    ¬ BoundedlyComplete (intrinsicExpectation ℝ rates) := by21  intro hBC22  apply hRNP23  apply hasRadonNikodymProperty_of_boundedlyCompleteDecomposition24  exact {25    projection := intrinsicExpectation ℝ rates26    finiteDimensional := intrinsicExpectation_range_finiteDimensional ℝ rates27    nested := intrinsicExpectation_comp_of_le ℝ rates28    uniformBound := ⟨1, norm_intrinsicExpectation_le ℝ rates⟩29    tendsto_identity := tendsto_intrinsicExpectation ℝ rates30    bounded_complete := hBC }3132theorem schur_intrinsic_not_boundedlyComplete_real :33    ¬ BoundedlyComplete (intrinsicExpectation ℝ schurRates) :=34  intrinsic_not_boundedlyComplete_real schurRates schur_intrinsic_not_RNP_real3536theorem constant_intrinsic_not_boundedlyComplete_real :37    ¬ BoundedlyComplete (intrinsicExpectation ℝ constantRates) :=38  intrinsic_not_boundedlyComplete_real constantRates constant_intrinsic_not_RNP_real3940/-- Failure of bounded completeness gives an actual bounded coherent branch that is not Cauchy.41This is an existence consequence; it does not identify a particular martingale. -/42theorem exists_nonCauchy_branch_of_not_boundedlyComplete43    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]44    (P : ℕ → E →L[ℝ] E) (hP : ¬ BoundedlyComplete P) :45    ∃ x : ℕ → E, (∀ m n, m ≤ n → P m (x n) = x m) ∧46      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) ∧ ¬ CauchySeq x := by47  classical48  by_contra! h49  apply hP50  intro x hx hbounded51  exact cauchySeq_tendsto_of_complete (h x hx hbounded)5253theorem schur_intrinsic_exists_nonCauchy_branch_real :54    ∃ x : ℕ → (dyadicSystem ℝ schurRates).IntrinsicSpace,55      (∀ m n, m ≤ n → intrinsicExpectation ℝ schurRates m (x n) = x m) ∧56      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) ∧ ¬ CauchySeq x :=57  exists_nonCauchy_branch_of_not_boundedlyComplete _ schur_intrinsic_not_boundedlyComplete_real5859theorem constant_intrinsic_exists_nonCauchy_branch_real :60    ∃ x : ℕ → (dyadicSystem ℝ constantRates).IntrinsicSpace,61      (∀ m n, m ≤ n → intrinsicExpectation ℝ constantRates m (x n) = x m) ∧62      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) ∧ ¬ CauchySeq x :=63  exists_nonCauchy_branch_of_not_boundedlyComplete _ constant_intrinsic_not_boundedlyComplete_real6465theorem intrinsic_not_boundedlyComplete_scalar (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)66    (hRNP : ¬ @HasRadonNikodymProperty.{_, 0}67      (UnderlyingReal K (dyadicSystem K rates).IntrinsicSpace)68      (inferInstanceAs (NormedAddCommGroup (dyadicSystem K rates).IntrinsicSpace))69      (NormedSpace.restrictScalars ℝ K (dyadicSystem K rates).IntrinsicSpace)) :70    ¬ ScalarDecompositionRNP.BoundedlyComplete (intrinsicExpectation K rates) := by71  intro hBC72  exact hRNP (ScalarDecompositionRNP.hasRNP_of_scalar_projections73    (intrinsicExpectation K rates) (intrinsicExpectation_range_finiteDimensional K rates)74    (intrinsicExpectation_comp_of_le K rates) ⟨1, norm_intrinsicExpectation_le K rates⟩75    (tendsto_intrinsicExpectation K rates) hBC)7677theorem schur_intrinsic_not_boundedlyComplete (K : Type*) [RCLike K] :78    ¬ ScalarDecompositionRNP.BoundedlyComplete (intrinsicExpectation K schurRates) :=79  intrinsic_not_boundedlyComplete_scalar K schurRates (schur_intrinsic_not_RNP K)8081theorem constant_intrinsic_not_boundedlyComplete (K : Type*) [RCLike K] :82    ¬ ScalarDecompositionRNP.BoundedlyComplete (intrinsicExpectation K constantRates) :=83  intrinsic_not_boundedlyComplete_scalar K constantRates (constant_intrinsic_not_RNP K)8485theorem schur_intrinsic_exists_nonCauchy_branch (K : Type*) [RCLike K] :86    ∃ x : ℕ → (dyadicSystem K schurRates).IntrinsicSpace,87      (∀ m n, m ≤ n → intrinsicExpectation K schurRates m (x n) = x m) ∧88      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) ∧ ¬ CauchySeq x :=89  ScalarDecompositionRNP.exists_nonCauchy_branch _ (schur_intrinsic_not_boundedlyComplete K)9091theorem constant_intrinsic_exists_nonCauchy_branch (K : Type*) [RCLike K] :92    ∃ x : ℕ → (dyadicSystem K constantRates).IntrinsicSpace,93      (∀ m n, m ≤ n → intrinsicExpectation K constantRates m (x n) = x m) ∧94      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) ∧ ¬ CauchySeq x :=95  ScalarDecompositionRNP.exists_nonCauchy_branch _ (constant_intrinsic_not_boundedlyComplete K)9697/-- The actual real Schur example has no uniformly bounded sign transformations for its FDD. -/98theorem schur_intrinsic_no_uniform_sign_bound :99    ¬ ∃ C : ℝ, 0 ≤ C ∧ ∀ (N : ℕ) (ε : ℕ → ℝ)100      (y : (dyadicSystem ℝ schurRates).IntrinsicSpace),101      (∀ j, ε j = 1 ∨ ε j = -1) →102        ‖∑ j ∈ Finset.range (N + 1), ε j •103          UnconditionalDecomposition.difference (intrinsicExpectation ℝ schurRates) j y‖ ≤ C * ‖y‖ :=104  UnconditionalRNP.no_uniform_sign_bound_of_not_RNP105    (schurRates_intrinsic_hasSchurProperty ℝ) schur_intrinsic_not_RNP_real106    (intrinsicExpectation ℝ schurRates) (intrinsicExpectation_range_finiteDimensional ℝ schurRates)107    (intrinsicExpectation_comp_of_le ℝ schurRates) (tendsto_intrinsicExpectation ℝ schurRates)108109end PL1.Noise110