PL1/ScalarDecompositionRNP.lean

All source files · Download exact source

SHA-256: a19293a92330b09856e0dbe3791a9c4742569a6077bb6a9ef209acd40d4b361a

1import PL1.DecompositionRNP2import Mathlib.Analysis.RCLike.Lemmas34/-! # Scalar restriction for finite-dimensional projection decompositions -/56noncomputable section7universe u v8open Filter9open scoped Topology1011namespace PL1.ScalarDecompositionRNP1213variable {K : Type*} [RCLike K]14variable {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E]1516/-- Bounded completeness expressed directly for scalar-linear projections and the inherited norm. -/17def BoundedlyComplete (P : ℕ → E →L[K] E) : Prop :=18  ∀ x : ℕ → E, (∀ m n, m ≤ n → P m (x n) = x m) →19    (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) → ∃ a, Tendsto x atTop (𝓝 a)2021/-- Scalar-linear boundedly complete finite-dimensional projections give the full RNP22of the underlying real space, with exactly the inherited norm. -/23theorem hasRNP_of_scalar_projections24    (P : ℕ → E →L[K] E) (hfinite : ∀ n, FiniteDimensional K (P n).range)25    (hnested : ∀ m n, m ≤ n → (P m).comp (P n) = P m)26    (hbound : ∃ C : ℝ, ∀ n, ‖P n‖ ≤ C)27    (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x))28    (hBC : ∀ x : ℕ → E, (∀ m n, m ≤ n → P m (x n) = x m) →29      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) → ∃ a, Tendsto x atTop (𝓝 a)) :30    @HasRadonNikodymProperty.{u, v} (UnderlyingReal K E)31      (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ K E) := by32  let := NormedSpace.restrictScalars ℝ K E33  let := IsScalarTower.restrictScalars ℝ K E34  change HasRadonNikodymProperty.{u, v} E35  let Q : ℕ → E →L[ℝ] E := fun n => (P n).restrictScalars ℝ36  have hfiniteR (n : ℕ) : FiniteDimensional ℝ (Q n).range := by37    let := hfinite n38    let : FiniteDimensional ℝ (P n).range := FiniteDimensional.trans ℝ K (P n).range39    exact inferInstanceAs (FiniteDimensional ℝ (P n).range)40  apply DecompositionRNP.hasRadonNikodymProperty_of_boundedlyCompleteDecomposition41  refine {42    projection := Q43    finiteDimensional := hfiniteR44    nested := ?_45    uniformBound := ?_46    tendsto_identity := hstrong47    bounded_complete := hBC }48  · intro m n hmn49    ext1 x50    exact DFunLike.congr_fun (hnested m n hmn) x51  · obtain ⟨C, hC⟩ := hbound52    exact ⟨C, fun n => (ContinuousLinearMap.norm_restrictScalars (P n)).trans_le (hC n)⟩5354/-- A failed bounded-completeness condition supplies a bounded coherent branch which is not Cauchy. -/55theorem exists_nonCauchy_branch (P : ℕ → E →L[K] E) (hP : ¬ BoundedlyComplete P) :56    ∃ x : ℕ → E, (∀ m n, m ≤ n → P m (x n) = x m) ∧57      (∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) ∧ ¬ CauchySeq x := by58  classical59  by_contra! h60  apply hP61  intro x hx hbounded62  exact cauchySeq_tendsto_of_complete (h x hx hbounded)6364end PL1.ScalarDecompositionRNP65