PL1/SchurLatticeAtomicity.lean

All source files · Download exact source

SHA-256: 1663132a506edfaee39f1c29b863c01e52f9fa2767823cf3d66250ed8b35a9f2

1import PL1.BalancedFragmentTree2import PL1.LatticeFragments3import PL1.LatticeRademacherWeak45/-!6# Separable Schur Banach lattices are atomic and have RNP78An atomless positive fragment produces a genuine balanced binary tree. Its9Rademachers have constant lattice modulus and satisfy the actual square bound10on every finite subsequence, contradicting the Schur property. Atomic bands11then supply the unconditional finite-dimensional projections required for RNP.12-/1314noncomputable section15open scoped Topology BigOperators16universe u v1718namespace PL1.SchurLattice1920variable {E : Type u} [NormedAddCommGroup E] [Lattice E]21  [IsOrderedAddMonoid E] [NormedVectorLattice E]2223/-- The actual balanced tree satisfies the square estimate on every finite24family of distinct Rademacher indices, with no subsequence restriction. -/25theorem balancedTree_rademacherSquareBound (φ : E →L[ℝ] ℝ) (hφ : 0 ≤ φ)26    {u : E} {split : E → E} (hu : 0 ≤ u)27    (hs : BalancedFragmentTree.IsBalancedSplit φ u split) :28    HasRademacherSquareBound φ u (BalancedFragmentTree.rademacher u split) := by29  classical30  intro N q hq ε hε31  let m := (Finset.univ.sup q) + 132  have hqm (i : Fin N) : q i < m :=33    Nat.lt_succ_of_le (Finset.le_sup (Finset.mem_univ i))34  let f : Fin N → Fin m := fun i => ⟨q i, hqm i⟩35  have hf : Function.Injective f := fun i j hij => hq (congrArg Fin.val hij)36  have hσ (i j : Fin N) :37      (∑ w : BalancedFragmentTree.Word m,38        φ (BalancedFragmentTree.cell u split m w) * BalancedFragmentTree.sign (f i) w *39          BalancedFragmentTree.sign (f j) w) = if i = j then φ u else 0 := by40    simpa only [hf.eq_iff] using BalancedFragmentTree.weighted_sign_orthogonality hu hs (f i) (f j)41  have h := dual_abs_sum_sq_le_of_orthogonal_fragments φ hφ u42    (BalancedFragmentTree.cell u split m)43    (fun w => (BalancedFragmentTree.cell_mem_Icc hu hs m w).1)44    (BalancedFragmentTree.cell_pairwise_disjoint hu hs m)45    (BalancedFragmentTree.sum_cell u split m)46    (fun i : Fin N => BalancedFragmentTree.rademacher u split (q i))47    (fun i w => BalancedFragmentTree.sign (f i) w)48    (fun i => BalancedFragmentTree.rademacher_refinement u split (hqm i)) hσ ε49  have hεsq (i : Fin N) : ε i ^ 2 = 1 := by50    rcases hε i with hi | hi <;> simp [hi]51  simpa only [hεsq, Finset.sum_const, Finset.card_univ, Fintype.card_fin,52    nsmul_eq_mul, mul_one] using h5354/-- Separability, completeness and the Schur property suffice for actual55vector-lattice atomicity; it is no longer an additional premise. -/56theorem isAtomicLattice_of_schur [CompleteSpace E] [TopologicalSpace.SeparableSpace E]57    (hS : HasSchurProperty ℝ E) : IsAtomicLattice E := by58  obtain ⟨φ, hφpos, hφ⟩ := exists_strictlyPositive (E := E)59  intro u hu60  by_contra hbad61  have hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u := fun a ha hau => hbad ⟨a, ha, hau⟩62  obtain ⟨split, hs⟩ := BalancedFragmentTree.exists_balancedSplit φ u (by63    intro x hx hxu64    exact LatticeFragments.exists_half_fragment hS φ hφ hx65      (fun a ha hax => hna a ha (hax.trans hxu)))66  have heq : u = 0 := eq_zero_of_constant_abs_rademacherSquareBound hS φ hφ u67    (BalancedFragmentTree.rademacher u split)68    (BalancedFragmentTree.abs_rademacher hu.le hs)69    (balancedTree_rademacherSquareBound φ hφpos hu.le hs)70  exact hu.ne' heq7172/-- Full vector-measure RNP for every separable Schur Banach lattice, with73an independent universe for the source measure space. -/74theorem hasRadonNikodymProperty_of_schur [CompleteSpace E] [TopologicalSpace.SeparableSpace E]75    (hS : HasSchurProperty ℝ E) : HasRadonNikodymProperty.{u, v} E :=76  AtomicBandDecomposition.hasRadonNikodymProperty_of_atomic hS (isAtomicLattice_of_schur hS)7778end PL1.SchurLattice79