PL1/MainTheoremB.lean

All source files · Download exact source

SHA-256: eb8d34075256768803f6ae87154fa2a7fd2c05e07eacf04fff63bdca69dd8c72

1import PL1.ALAlternative2import PL1.EnfloNoL13import PL1.ComplementedLatticeRealAmbient45/-!6# The full reviewed Theorem B78The actual constant-rate projection range contains no interval L1 copy.9If it admitted an equivalent real lattice norm, the complemented-L1 lattice10alternative would make it Schur or yield a real interval L1 copy. Both11possibilities contradict proved properties of this same range.12-/1314noncomputable section15set_option backward.isDefEq.respectTransparency false16universe u17open TopologicalSpace1819namespace PL120open PL1.ComplementedLattice2122/-- Every reviewed clause of B holds for the actual constant-rate projection,23including the stronger underlying-real nonlattice clause for complex scalars. -/24theorem constant_intervalProjection_theoremBSpec (K : Type u) [RCLike K] :25    TheoremBSpec K (Noise.intervalProjection K Noise.constantRates) := by26  let Q := Noise.intervalProjection K Noise.constantRates27  have hQ := Noise.intervalProjection_isProjection K Noise.constantRates28  have hclosed := Noise.intervalProjection_range_isClosed K Noise.constantRates29  let : CompleteSpace Q.range := hclosed.isComplete.completeSpace_coe30  let : SeparableSpace (Noise.projection K Noise.constantRates).range :=31    Noise.projection_range_separableSpace K Noise.constantRates32  let e := Noise.intervalProjectionRangeEquiv K Noise.constantRates33  let : SeparableSpace Q.range := e.surjective.denseRange.separableSpace e.continuous34  let : CompleteSpace (UnderlyingReal K Q.range) := inferInstanceAs (CompleteSpace Q.range)35  let : SeparableSpace (UnderlyingReal K Q.range) := inferInstanceAs (SeparableSpace Q.range)36  refine ⟨hQ, Noise.norm_intervalProjection_le K Noise.constantRates, hclosed,37    Noise.intervalProjection_range_infiniteDimensional K Noise.constantRates,38    Noise.constant_intervalProjection_range_contains_ell2 K, ?_,39    Noise.constant_intervalProjection_range_not_schur K, ?_⟩40  · intro hcopy41    exact Noise.constant_intervalProjection_range_no_real_L1 K42      (scalar_L1_copy_contains_real_L1 hcopy)43  · intro hlat44    apply hlat.elim_separable45    intro F _ _ _ _ _ eF46    let eFn : Q.range ≃L[ℝ] F := (naturalToUnderlyingReal (K := K) Q.range).trans eF47    let CF := complementedCopyTransport (projectionRangeCopyReal Q hQ) eFn48    let CFreal := complementedCopyComp CF (scalarIntervalRealCopy K)49    obtain hs | hc := ALAlternative.schur_or_contains_interval_of_complemented CFreal50    · exact Noise.constant_intervalProjection_range_not_schur K51        ((hasSchurProperty_iff_real (𝕜 := K) (E := Q.range)).mpr52          ((hasSchurProperty_equiv_iff eFn).mpr hs))53    · exact Noise.constant_intervalProjection_range_no_real_L1 K (hc.map eFn.symm)5455theorem theoremB (K : Type u) [RCLike K] : TheoremBStatement K :=56  ⟨Noise.intervalProjection K Noise.constantRates, constant_intervalProjection_theoremBSpec K⟩5758theorem theoremBReal : TheoremBRealStatement := theoremB ℝ5960theorem theoremBComplexStrong : TheoremBComplexStrongStatement := theoremB ℂ6162end PL163