Read-only source copy. Line numbers are navigation aids.
import ComplementedSubspace.ActualProjectionDPRimport ComplementedSubspace.ActualProjectionDualDPRimport ComplementedSubspace.AmbientUniformConveximport ComplementedSubspace.AmbientFiniteApproximationimport ComplementedSubspace.ProjectionCorollaries/-! Assembly of the real main theorem from the actual recursive construction. -/noncomputable sectionopen scoped ENNRealset_option backward.isDefEq.respectTransparency falsenamespace ComplementedSubspacetheorem realMainTheorem : RealMainTheoremStatement := by intro ρ hρ obtain ⟨η, hη, P, hPP, hP1, hP, hPc1, hPc, hcoords⟩ := exists_recursive_alternatingProjection_near_one (B := 1 + ρ) (by linarith) let s := recursiveFrameSelection hη refine ⟨s.toBlockParameters, inferInstance, inferInstance, ambient_hasRealBanachLatticeOrder s.toBlockParameters, P, hPP, hP, hPc, ?_, ?_⟩ · exact hasSeparatedRange_of_DPR_obstructions P hPP (ambient_chiGL_le_one s.toBlockParameters) (ambientDual_chiGL_le_one s.toBlockParameters) (actualProjection_range_chiDPR_eq_top s P hcoords) (actualProjection_range_dual_chiDPR_eq_top s P hcoords) · exact hasSeparatedRange_of_DPR_obstructions (ContinuousLinearMap.id ℝ (Ambient s.toBlockParameters) - P) (complement_idempotent P hPP) (ambient_chiGL_le_one s.toBlockParameters) (ambientDual_chiGL_le_one s.toBlockParameters) (actualProjection_complement_range_chiDPR_eq_top s P hcoords) (actualProjection_complement_range_dual_chiDPR_eq_top s P hcoords)end ComplementedSubspace