Read-only source copy. Line numbers are navigation aids.
import ComplementedSubspace.ComplexProjectionRealEquivimport ComplementedSubspace.ComplexCorollaryAssembly/-! The complex unconditional-basis theorem, using the actual finite complexprojection and a whole-space real equivalence to the verified real frame sum.The continuous dual is handled by the real/complex dual isometry. -/noncomputable sectionset_option backward.isDefEq.respectTransparency falseset_option backward.isDefEq.respectTransparency.types falseset_option synthInstance.maxSize 256namespace ComplementedSubspace/-- For every positive tolerance there is a projection on a complex Banachspace with an actual 1-unconditional basis, of norm below one plus thattolerance, whose range and continuous dual have no unconditional basis. -/theorem complexCorollary : ComplexCorollaryStatement := by exact complexCorollary_of_recursive_range_equivalences (fun s => ⟨s.predecessorComplexRangeRealEquiv⟩)end ComplementedSubspace