TopologyUnconditionalBridge.lean

1 import PaperIRelease.TopologyUnconditional
2 import PaperIRelease.TopologyCountablePackets
3 
4 /-! # Identification of countable packet coordinates with the general sum space -/
5 
6 noncomputable section
7 open Set
8 
9 namespace PaperIRelease.TopologyCountablePackets.Projectors
10 
11 open PaperIRelease.TopologyUnconditional
12 
13 variable {𝕜 X : Type*} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
14 variable (P : Projectors 𝕜 X)
15 
16 /-- The closed ranges of the countable bounded idempotents. -/
17 def closedPackets : ClosedPackets 𝕜 X where
18   packet n := (P.proj n).range
19   closed n := by
20     apply ContinuousLinearMap.IsIdempotentElem.isClosed_range
21     apply ContinuousLinearMap.ext
22     exact P.idempotent n
23 
24 /-- Both carriers are the same summable coordinate families. -/
25 def generalSpaceLinearEquiv : P.PacketSpace ≃ₗ[𝕜] P.closedPackets.Space where
26   toFun x := ⟨x.val, x.property⟩
27   invFun x := ⟨x.val, x.property⟩
28   left_inv _ := rfl
29   right_inv _ := rfl
30   map_add' _ _ := rfl
31   map_smul' _ _ := rfl
32 
33 /-- The two literal signed-sum supremum norms agree. -/
34 def generalSpaceIsometry : P.PacketSpace ≃ₗᵢ[𝕜] P.closedPackets.Space where
35   toLinearEquiv := P.generalSpaceLinearEquiv
36   norm_map' x := by
37     change sSup (P.closedPackets.signedValues (P.generalSpaceLinearEquiv x)) =
38       sSup (P.signedValues x)
39     congr 1
40     ext r
41     constructor
42     · rintro ⟨⟨F, ⟨a, ha⟩⟩, hr⟩
43       exact ⟨F, a, ha, hr.symm⟩
44     · rintro ⟨F, a, ha, hr⟩
45       exact ⟨⟨F, ⟨a, ha⟩⟩, hr.symm⟩
46 
47 /-- The countable theorem targets exactly the general unconditional sum
48 space of the closed packet ranges. -/
49 def countableUnconditionalPacketEquiv : X ≃L[𝕜] P.closedPackets.Space :=
50   P.packetEquiv.trans P.generalSpaceIsometry.toContinuousLinearEquiv
51 
52 /-- Its analysis norm is at most the declared multiplier constant. -/
53 theorem countable_analysis_norm_le :
54     ‖P.countableUnconditionalPacketEquiv.toContinuousLinearMap‖ ≤ P.K := by
55   apply ContinuousLinearMap.opNorm_le_bound _ P.nonneg_K
56   intro x
57   change ‖P.generalSpaceIsometry (P.packetEquiv x)‖ ≤ _
58   rw [P.generalSpaceIsometry.norm_map]
59   exact ContinuousLinearMap.le_of_opNorm_le _ P.analysis_opNorm_le x
60 
61 /-- Its synthesis norm is at most one. -/
62 theorem countable_synthesis_norm_le :
63     ‖P.countableUnconditionalPacketEquiv.symm.toContinuousLinearMap‖ ≤ 1 := by
64   apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one
65   intro x
66   change ‖P.synthesis (P.generalSpaceIsometry.symm x)‖ ≤ _
67   calc
68     ‖P.synthesis (P.generalSpaceIsometry.symm x)‖ ≤ ‖P.generalSpaceIsometry.symm x‖ :=
69       P.synthesis_norm_le _
70     _ = 1 * ‖x‖ := by rw [P.generalSpaceIsometry.symm.norm_map, one_mul]
71 
72 end PaperIRelease.TopologyCountablePackets.Projectors

Back to source controls