PL1/LatticeReduction.lean

All source files · Download exact source

SHA-256: 655ee03987a3eb56b5714ba1fa8a348af6b3ab2720cc222e82a95ede03f5c450

1import PL1.LatticeRenorming2import PL1.PartialMainTheorems34/-! # The structural reduction for Theorem A56This module proves a conditional reduction. `SeparableSchurLatticeRNP` is7explicitly supplied as an argument here and is proved in `PL1.MainTheoremA`8using the actual Schur-lattice atomicity and vector-measure RNP theorems.9-/1011noncomputable section12universe u13open TopologicalSpace1415namespace PL11617/-- The real Banach-lattice structural assertion used by the reduction. This is a18proposition to prove, not an axiom or an instance. -/19def SeparableSchurLatticeRNP : Prop :=20  ∀ (F : Type u) [NormedAddCommGroup F] [Lattice F] [IsOrderedAddMonoid F]21    [BanachLattice F] [SeparableSpace F],22    HasSchurProperty ℝ F → HasRadonNikodymProperty.{u, 0} F2324theorem not_hasEquivalentRealLatticeNorm_of_structural_RNP25    (hstruct : SeparableSchurLatticeRNP.{u})26    {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]27    [CompleteSpace E] [SeparableSpace E]28    (hS : HasSchurProperty ℝ E) (hRNP : ¬ HasRadonNikodymProperty.{u, 0} E) :29    ¬ HasEquivalentRealLatticeNorm E := by30  intro h31  apply h.elim_separable32  intro F _ _ _ _ _ e33  exact hRNP ((RNPBridge.hasRadonNikodymProperty_iff_equiv e).mpr34    (hstruct F ((hasSchurProperty_equiv_iff e).mp hS)))3536/-- Conditional endpoint with exactly the reviewed full A target.37`PL1.MainTheoremA` discharges the structural RNP hypothesis. -/38theorem theoremA_of_separableSchurLatticeRNP (𝕜 : Type u) [RCLike 𝕜]39    (hstruct : SeparableSchurLatticeRNP.{u}) : TheoremAStatement 𝕜 := by40  let P := Noise.intervalProjection 𝕜 Noise.schurRates41  have hclosed := Noise.intervalProjection_range_isClosed 𝕜 Noise.schurRates42  let : CompleteSpace P.range := hclosed.isComplete.completeSpace_coe43  let : SeparableSpace (Noise.projection 𝕜 Noise.schurRates).range :=44    Noise.projection_range_separableSpace 𝕜 Noise.schurRates45  let e := Noise.intervalProjectionRangeEquiv 𝕜 Noise.schurRates46  let : SeparableSpace P.range := e.surjective.denseRange.separableSpace e.continuous47  refine ⟨P, Noise.intervalProjection_isProjection 𝕜 Noise.schurRates,48    Noise.norm_intervalProjection_le 𝕜 Noise.schurRates, hclosed,49    Noise.intervalProjection_range_infiniteDimensional 𝕜 Noise.schurRates,50    Noise.schur_intervalProjection_isDunfordPettis 𝕜,51    Noise.schur_intervalProjection_range_hasSchurProperty 𝕜,52    Noise.schur_intervalProjection_range_not_RNP 𝕜, ?_⟩53  let := NormedSpace.restrictScalars ℝ 𝕜 P.range54  change ¬ HasEquivalentRealLatticeNorm P.range55  apply not_hasEquivalentRealLatticeNorm_of_structural_RNP hstruct56  · exact (hasSchurProperty_iff_underlyingReal 𝕜 P.range).mp57      (Noise.schur_intervalProjection_range_hasSchurProperty 𝕜)58  · exact Noise.schur_intervalProjection_range_not_RNP 𝕜5960end PL161