PL1/UnconditionalRNP.lean

All source files · Download exact source

SHA-256: 8f34f976dd28fc64e6da1f94d589f119c019f6cc18bcab40269c8b1974a09521

1import PL1.DecompositionRNP2import PL1.UnconditionalDecomposition34/-! # Schur spaces with unconditional finite-dimensional projections have RNP56This proves the analytic implication once the actual finite-dimensional7projections are supplied. It makes no assertion that an arbitrary Banach8lattice has a basis or a sequence of such projections.9-/1011noncomputable section12universe u v13open Filter14open scoped Topology BigOperators1516namespace PL1.UnconditionalRNP1718open DecompositionRNP UnconditionalDecomposition1920variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]2122/-- The projection differences telescope on every vector. -/23theorem sum_difference_apply (P : ℕ → E →L[ℝ] E) (N : ℕ) (y : E) :24    (∑ j ∈ Finset.range (N + 1), difference P j y) = P N y := by25  have h : ∀ j, difference P j y = branchDifference (fun n => P n y) j := by26    intro j27    cases j <;> rfl28  simpa only [h] using sum_branchDifference (fun n => P n y) N2930/-- The all-positive choice of signs bounds the partial-sum projections. -/31theorem norm_projection_le_of_sign_bound32    (P : ℕ → E →L[ℝ] E) (C : ℝ) (hC : 0 ≤ C)33    (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),34      (∀ j, ε j = 1 ∨ ε j = -1) →35        ‖∑ j ∈ Finset.range (N + 1), ε j • difference P j y‖ ≤ C * ‖y‖)36    (N : ℕ) : ‖P N‖ ≤ C := by37  apply ContinuousLinearMap.opNorm_le_bound _ hC38  intro y39  have h := htransform N (fun _ => 1) y (fun _ => Or.inl rfl)40  simpa only [one_smul, sum_difference_apply] using h4142/-- The full vector-measure RNP follows from the Schur property and an actual43unconditional finite-dimensional projection decomposition. -/44theorem hasRadonNikodymProperty_of_schur_unconditional_projections [CompleteSpace E]45    (hS : HasSchurProperty ℝ E) (P : ℕ → E →L[ℝ] E)46    (hfinite : ∀ n, FiniteDimensional ℝ (P n).range)47    (hnested : ∀ m n, m ≤ n → (P m).comp (P n) = P m)48    (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x))49    (C : ℝ) (hC : 0 ≤ C)50    (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),51      (∀ j, ε j = 1 ∨ ε j = -1) →52        ‖∑ j ∈ Finset.range (N + 1), ε j • difference P j y‖ ≤ C * ‖y‖) :53    HasRadonNikodymProperty.{u, v} E := by54  apply hasRadonNikodymProperty_of_boundedlyCompleteDecomposition55  exact {56    projection := P57    finiteDimensional := hfinite58    nested := hnested59    uniformBound := ⟨C, norm_projection_le_of_sign_bound P C hC htransform⟩60    tendsto_identity := hstrong61    bounded_complete := bounded_branch_converges hS P C hC htransform }6263/-- A Schur space failing RNP cannot have uniformly bounded sign transforms64for any strongly convergent nested finite-dimensional projection decomposition. -/65theorem no_uniform_sign_bound_of_not_RNP [CompleteSpace E]66    (hS : HasSchurProperty ℝ E) (hRNP : ¬ HasRadonNikodymProperty.{u, v} E)67    (P : ℕ → E →L[ℝ] E)68    (hfinite : ∀ n, FiniteDimensional ℝ (P n).range)69    (hnested : ∀ m n, m ≤ n → (P m).comp (P n) = P m)70    (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x)) :71    ¬ ∃ C : ℝ, 0 ≤ C ∧ ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),72      (∀ j, ε j = 1 ∨ ε j = -1) →73        ‖∑ j ∈ Finset.range (N + 1), ε j • difference P j y‖ ≤ C * ‖y‖ := by74  rintro ⟨C, hC, htransform⟩75  exact hRNP (hasRadonNikodymProperty_of_schur_unconditional_projections76    hS P hfinite hnested hstrong C hC htransform)7778end PL1.UnconditionalRNP79