ComplementedSubspace/RealMainConsequences.lean

1import ComplementedSubspace.RealMainTheorem

2import ComplementedSubspace.ActualProjectionBidualDPR

3import ComplementedSubspace.AmbientSchauder

5/-! Real corollary and separable nonprimarity for the actual recursive construction.

6The nonlattice assertion for the range dual uses the separately proved bidual

7DPR obstruction. -/

9noncomputable section

10set_option backward.isDefEq.respectTransparency false

11set_option backward.isDefEq.respectTransparency.types false

12set_option synthInstance.maxSize 256

14namespace ComplementedSubspace

16def ambientBanachModel (a : BlockParameters) : BanachModel.{0} ℝ where

17 Carrier := Ambient a

18 normedGroup := inferInstance

19 normedSpace := inferInstance

20 completeSpace := inferInstance

22theorem realCorollary : RealCorollaryStatement := by

23 intro ρ hρ

24 obtain ⟨η, hη, P, hPP, hP1, hP, hPc1, hPc, hcoords⟩ :=

25 exists_recursive_alternatingProjection_near_one (B := 1 + ρ) (by linarith)

26 let s := recursiveFrameSelection hη

27 letI : CompleteSpace P.range := completeSpace_projection_range P hPP

28 have hn := @corollary_negations_of_DPR_obstructions P.range

29 (inferInstance : NormedAddCommGroup P.range)

30 (inferInstance : NormedSpace ℝ P.range)

31 (completeSpace_projection_range P hPP)

32 (actualProjection_range_chiDPR_eq_top s P hcoords)

33 (actualProjection_range_dual_chiDPR_eq_top s P hcoords)

34 (actualProjection_range_bidual_chiDPR_eq_top s P hcoords)

35 exact ⟨ambientBanachModel s.toBlockParameters,

36 ambient_hasOneUnconditionalSchauderBasis s.toBlockParameters,

37 P, hPP, hP, hn⟩

39theorem realUnconditionalCorollary : UnconditionalCorollaryStatement ℝ := by

40 intro ρ hρ

41 obtain ⟨X, hX, P, hPP, hP, hZ, hZD, hZlat, hZDlat⟩ := realCorollary ρ hρ

42 exact ⟨X, hX, P, hPP, hP, hZ, hZD⟩

44theorem separableNonprimarity_of_realMainTheorem (hmain : RealMainTheoremStatement) :

45 SeparableNonprimarityStatement := by

46 intro ρ hρ

47 obtain ⟨a, hsep, huc, hlat, P, hPP, hP, hPc, hZ, hZc⟩ := hmain ρ hρ

48 refine ⟨ambientBanachModel a, hsep, hlat, ?_,

49 ambient_hasOneUnconditionalSchauderBasis a, P, hPP, hP, hPc, ?_, ?_⟩

50 · exact ⟨ambientBanachModel a, huc, ⟨ContinuousLinearEquiv.refl ℝ (Ambient a)⟩⟩

51 · exact not_isomorphic_to_realBanachLattice_of_dual_DPR_top hZ.2.2.2

52 · exact not_isomorphic_to_realBanachLattice_of_dual_DPR_top hZc.2.2.2

54theorem realSeparableNonprimarity : SeparableNonprimarityStatement :=

55 separableNonprimarity_of_realMainTheorem realMainTheorem

57end ComplementedSubspace