ShrinkChain: Forster's four-level shrinking chain (finiteness-and-chi)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md D3, §4.2, proof plan §6.4).

ShrinkChain X packages Forster's 𝔚 ⋐ 𝔙 ⋐ 𝔘 ⋐ 𝔘* same-index-set shrinking chain (D3): U* chart disks (Leray-good), U the level whose closure sits inside U*, V the Montel-compact middle level, W the coboundary level whose closure sits inside V. All four induced FinCover ⊤s share the same index set, so every refinement map between them is τ = id (ref_star_U/ref_star_V/ref_star_W/ref_U_V/ref_V_W/ref_U_W) — no τ-plumbing ever enters the norm layer.

Existence (ShrinkChain.nonempty) iterates the cech exists_chartDisk_closure_basis pattern four times per point (chart disk ⋐ level 1 ⋐ level 2 ⋐ level 3), then extracts a finite subcover of the innermost level W, reindexed by Finset.equivFin exactly as Cech.Covers's exists_good_refinement_closure does.

Also provides the Banach cochain layer at one level P ∈ {U, V, W}: NC0/NC1 (finite Pis of BddHoloOn), deltaCLM (the 0-to-1 coboundary, Cech's d0 transposed to the norm layer), NZ1 (bounded cocycles, packaged as ContinuousLinearMap.ker of an internal d1NC — closed and complete "for free", no hand-rolled pointwise-condition closedness proof needed), resNC0/resNC1 (restriction CLMs between same-index levels), the cocycle-relation workhorse NZ1.rel_res (mirrors Cech.Refinement's Z1.rel_res), resNC1_mapsTo_NZ1 (mirrors resC1_mem_Z1), and resZ (restriction of bounded cocycles, via ContinuousLinearMap.codRestrict).

Finally, Forster's 14.6(b) Banach geometry (§4.2, §5 step 1): tradeDefect (the defect CLM (ζ, ξ, η) ↦ ζ|𝔚 − ξ|𝔚 − δ𝔚 η on Z¹(𝔘) × Z¹(𝔙) × C⁰(𝔚)), tradeSpace (Forster's subspace L ⊆ Z¹(𝔘) × Z¹(𝔙) × C⁰(𝔚), its ContinuousLinearMap.ker — complete for free), the membership unfolders mem_tradeSpace_iff/mem_tradeSpace_iff_eq, and the two Schwartz-cospan projections tradePi (π = pr₂, the leg TradeBounded.lean proves surjective) and tradeCompact (v = res_UV ∘ pr₁, the Montel-compact leg), plus registered instance shortcuts on ↥(NZ1 T P)/↥(tradeSpace T) that make the surrounding instance searches reliable (see the note above NZ1's instances and the resolution note at the end of this file — the former TODO(blocker) is RESOLVED). Still deferred (NOT instance-blocked, just not built here): the two IsCompactOperator assembly lemmas of design §4.4 (isCompactOperator_resZ_UV, isCompactOperator_tradeCompact) — see the end-of-file note. Nothing here uses the forbidden tactic.

structure RS.Finiteness.ShrinkChain (X : Type u_2) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_2

Forster's 𝔚 ⋐ 𝔙 ⋐ 𝔘 ⋐ 𝔘* with 𝔘* chart disks; same index set (D3).

• n : ℕ

  The number of chart centres in the chain.

• c : Fin self.n → X

  The chart centres.

• Ustar : Fin self.n → TopologicalSpace.Opens X

  The outermost opens, each inside its centre's chart source.

• U : Fin self.n → TopologicalSpace.Opens X

  The first shrinking: closure (U i) ⊆ Ustar i.

• V : Fin self.n → TopologicalSpace.Opens X

  The second shrinking: closure (V i) ⊆ U i.

• W : Fin self.n → TopologicalSpace.Opens X

  The innermost opens, which still cover X.

• isChartDisk_Ustar (i : Fin self.n) : Cech.IsChartDisk (self.Ustar i)
• Ustar_subset_source (i : Fin self.n) : ↑(self.Ustar i) ⊆ (chartAt ℂ (self.c i)).source
• closure_U_subset (i : Fin self.n) : closure ↑(self.U i) ⊆ ↑(self.Ustar i)
• closure_V_subset (i : Fin self.n) : closure ↑(self.V i) ⊆ ↑(self.U i)
• closure_W_subset (i : Fin self.n) : closure ↑(self.W i) ⊆ ↑(self.V i)
• covers_W (x : X) : ∃ (i : Fin self.n), x ∈ self.W i

theorem RS.Finiteness.ShrinkChain.W_subset_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : ↑(T.W i) ⊆ ↑(T.V i)

theorem RS.Finiteness.ShrinkChain.V_subset_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : ↑(T.V i) ⊆ ↑(T.U i)

theorem RS.Finiteness.ShrinkChain.U_subset_Ustar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : ↑(T.U i) ⊆ ↑(T.Ustar i)

Opens-level ≤ forms of the chain inclusions — the shapes restrictCLM/resNC1/resZ consume (definitionally the same statements as the Set-level _subset_ lemmas above).

theorem RS.Finiteness.ShrinkChain.W_le_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : T.W i ≤ T.V i

theorem RS.Finiteness.ShrinkChain.V_le_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : T.V i ≤ T.U i

theorem RS.Finiteness.ShrinkChain.U_le_Ustar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : T.U i ≤ T.Ustar i

theorem RS.Finiteness.ShrinkChain.W_le_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (i : Fin T.n) : T.W i ≤ T.U i

theorem RS.Finiteness.ShrinkChain.covers_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (x : X) : ∃ (i : Fin T.n), x ∈ T.V i

theorem RS.Finiteness.ShrinkChain.covers_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (x : X) : ∃ (i : Fin T.n), x ∈ T.U i

theorem RS.Finiteness.ShrinkChain.covers_Ustar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (x : X) : ∃ (i : Fin T.n), x ∈ T.Ustar i

@[reducible]

noncomputable def RS.Finiteness.ShrinkChain.coverW {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.FinCover ⊤

The four FinCover ⊤s induced by a ShrinkChain. Reducible: their fields must unfold at implicit transparency, or applications like C1 D T.coverW are not type-correct there and every rewrite in such a goal fails.

Equations

• T.coverW = { n := T.n, U := T.W, le_base := ⋯, covers := ⋯ }

@[reducible]

noncomputable def RS.Finiteness.ShrinkChain.coverV {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.FinCover ⊤

The cover of X by the V-level opens.

Equations

• T.coverV = { n := T.n, U := T.V, le_base := ⋯, covers := ⋯ }

@[reducible]

noncomputable def RS.Finiteness.ShrinkChain.coverU {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.FinCover ⊤

The cover of X by the U-level opens.

Equations

• T.coverU = { n := T.n, U := T.U, le_base := ⋯, covers := ⋯ }

@[reducible]

noncomputable def RS.Finiteness.ShrinkChain.coverStar {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.FinCover ⊤

The cover of X by the outermost Ustar-level opens.

Equations

• T.coverStar = { n := T.n, U := T.Ustar, le_base := ⋯, covers := ⋯ }

theorem RS.Finiteness.ShrinkChain.good_star {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : T.coverStar.IsGood

theorem RS.Finiteness.ShrinkChain.ref_star_U {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.IsRefIdx T.coverStar T.coverU id

theorem RS.Finiteness.ShrinkChain.ref_star_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.IsRefIdx T.coverStar T.coverV id

theorem RS.Finiteness.ShrinkChain.ref_star_W {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.IsRefIdx T.coverStar T.coverW id

theorem RS.Finiteness.ShrinkChain.ref_U_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.IsRefIdx T.coverU T.coverV id

theorem RS.Finiteness.ShrinkChain.ref_V_W {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.IsRefIdx T.coverV T.coverW id

theorem RS.Finiteness.ShrinkChain.ref_U_W {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) : Cech.IsRefIdx T.coverU T.coverW id

theorem RS.Finiteness.ShrinkChain.nonempty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] : Nonempty (ShrinkChain X)

Existence of a ShrinkChain (§6.4): iterate the cech chart-disk-with-compact-closure basis four times per point, then extract a finite subcover of the innermost level.

Banach cochain layer at a level P ∈ {U, V, W}

@[reducible, inline]

abbrev RS.Finiteness.NC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : Type u_1

0-cochains at level P (a finite Pi of BddHoloOns).

Equations

• RS.Finiteness.NC0 T P = ((i : Fin T.n) → ↥(RS.Finiteness.BddHoloOn (P i)))

@[reducible, inline]

abbrev RS.Finiteness.NC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : Type u_1

1-cochains at level P (full product over ordered pairs, no i < j convention — matches cech's D5 convention).

Equations

• RS.Finiteness.NC1 T P = ((p : Fin T.n × Fin T.n) → ↥(RS.Finiteness.BddHoloOn (P p.1 ⊓ P p.2)))

noncomputable def RS.Finiteness.deltaCLM {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : NC0 T P →L[ℂ] NC1 T P

(δ⁰f)_{ij} = f_j − f_i (after restriction to P i ⊓ P j); the Banach-layer analogue of Cech.d0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Finiteness.deltaCLM_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (f : NC0 T P) (p : Fin T.n × Fin T.n) : (deltaCLM T P) f p = (restrictCLM ⋯) (f p.2) - (restrictCLM ⋯) (f p.1)

noncomputable def RS.Finiteness.d1NC {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : NC1 T P →L[ℂ] (t : Fin T.n × Fin T.n × Fin T.n) → ↥(BddHoloOn (P t.1 ⊓ P t.2.1 ⊓ P t.2.2))

The 1-to-2-cochain coboundary at level P, purely internal (used only to package NZ1 as a continuous-kernel submodule — no NC2 is ever exported).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Finiteness.d1NC_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (f : NC1 T P) (t : Fin T.n × Fin T.n × Fin T.n) : (d1NC T P) f t = (restrictCLM ⋯) (f (t.2.1, t.2.2)) - (restrictCLM ⋯) (f (t.1, t.2.2)) + (restrictCLM ⋯) (f (t.1, t.2.1))

Bounded cocycles: the kernel of d1NC, a closed submodule (ContinuousLinearMap.ker) — Banach for free (ContinuousLinearMap.completeSpace_ker), no hand-rolled pointwise-condition closedness proof needed.

noncomputable def RS.Finiteness.NZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : Submodule ℂ (NC1 T P)

The norm-bounded cocycles at level P: the kernel of the bounded coboundary d1NC.

Equations

• RS.Finiteness.NZ1 T P = (↑(RS.Finiteness.d1NC T P)).ker

instance RS.Finiteness.instCompleteSpaceSubtypeNC1MemSubmoduleComplexNZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : CompleteSpace ↥(NZ1 T P)

@[instance_reducible]

noncomputable instance RS.Finiteness.instAddCommGroupSubtypeNC1MemSubmoduleComplexNZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : AddCommGroup ↥(NZ1 T P)

Equations

• RS.Finiteness.instAddCommGroupSubtypeNC1MemSubmoduleComplexNZ1 T P = (RS.Finiteness.NZ1 T P).addCommGroup

instance RS.Finiteness.instIsTopologicalAddGroupSubtypeNC1MemSubmoduleComplexNZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : IsTopologicalAddGroup ↥(NZ1 T P)

@[instance_reducible]

noncomputable instance RS.Finiteness.instNormedAddCommGroupSubtypeNC1MemSubmoduleComplexNZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : NormedAddCommGroup ↥(NZ1 T P)

Equations

• RS.Finiteness.instNormedAddCommGroupSubtypeNC1MemSubmoduleComplexNZ1 T P = (RS.Finiteness.NZ1 T P).normedAddCommGroup

@[instance_reducible]

noncomputable instance RS.Finiteness.instNormedSpaceComplexSubtypeNC1MemSubmoduleNZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : NormedSpace ℂ ↥(NZ1 T P)

Equations

• RS.Finiteness.instNormedSpaceComplexSubtypeNC1MemSubmoduleNZ1 T P = (RS.Finiteness.NZ1 T P).normedSpace

theorem RS.Finiteness.mem_NZ1_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (f : NC1 T P) : f ∈ NZ1 T P ↔ ∀ (t : Fin T.n × Fin T.n × Fin T.n), (d1NC T P) f t = 0

theorem RS.Finiteness.NZ1.rel_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) {f : NC1 T P} (hf : f ∈ NZ1 T P) (a b c : Fin T.n) {W : TopologicalSpace.Opens X} (h : W ≤ P a ⊓ P b ⊓ P c) (hbc : W ≤ P b ⊓ P c) (hac : W ≤ P a ⊓ P c) (hab : W ≤ P a ⊓ P b) : (restrictCLM hbc) (f (b, c)) - (restrictCLM hac) (f (a, c)) + (restrictCLM hab) (f (a, b)) = 0

The cocycle-relation workhorse (mirrors Cech.Refinement's Z1.rel_res): any cocycle-relation triple, restricted to any smaller open W (via arbitrary — by proof irrelevance, any — witnessing inequalities).

noncomputable def RS.Finiteness.resNC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P P' : Fin T.n → TopologicalSpace.Opens X) (h : ∀ (i : Fin T.n), P' i ≤ P i) : NC0 T P →L[ℂ] NC0 T P'

Restriction of 0-cochains along a same-index shrinking P' ≤ P.

Equations

• RS.Finiteness.resNC0 T P P' h = ContinuousLinearMap.pi fun (i : Fin T.n) => RS.Finiteness.restrictCLM ⋯ ∘SL ContinuousLinearMap.proj i

noncomputable def RS.Finiteness.resNC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P P' : Fin T.n → TopologicalSpace.Opens X) (h : ∀ (i : Fin T.n), P' i ≤ P i) : NC1 T P →L[ℂ] NC1 T P'

Restriction of 1-cochains along a same-index shrinking P' ≤ P.

Equations

• RS.Finiteness.resNC1 T P P' h = ContinuousLinearMap.pi fun (p : Fin T.n × Fin T.n) => RS.Finiteness.restrictCLM ⋯ ∘SL ContinuousLinearMap.proj p

@[simp]

theorem RS.Finiteness.resNC1_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P P' : Fin T.n → TopologicalSpace.Opens X) (h : ∀ (i : Fin T.n), P' i ≤ P i) (f : NC1 T P) (p : Fin T.n × Fin T.n) : (resNC1 T P P' h) f p = (restrictCLM ⋯) (f p)

theorem RS.Finiteness.resNC1_mapsTo_NZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P P' : Fin T.n → TopologicalSpace.Opens X) (h : ∀ (i : Fin T.n), P' i ≤ P i) {f : NC1 T P} (hf : f ∈ NZ1 T P) : (resNC1 T P P' h) f ∈ NZ1 T P'

Restriction takes bounded cocycles to bounded cocycles (naturality of d1NC, via the NZ1.rel_res workhorse — mirrors Cech.Refinement's resC1_mem_Z1).

noncomputable def RS.Finiteness.resZ {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P P' : Fin T.n → TopologicalSpace.Opens X) (h : ∀ (i : Fin T.n), P' i ≤ P i) : ↥(NZ1 T P) →L[ℂ] ↥(NZ1 T P')

Restriction of bounded cocycles between same-index levels.

Equations

• RS.Finiteness.resZ T P P' h = (RS.Finiteness.resNC1 T P P' h ∘SL (RS.Finiteness.NZ1 T P).subtypeL).codRestrict (RS.Finiteness.NZ1 T P') ⋯

Forster 14.6(b): the trade subspace L and its two Schwartz-cospan projections

noncomputable def RS.Finiteness.tradeDefect {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : ↥(NZ1 T T.U) × ↥(NZ1 T T.V) × NC0 T T.W →L[ℂ] NC1 T T.W

Forster 14.6(b)'s defect map (ζ, ξ, η) ↦ ζ|𝔚 − ξ|𝔚 − δ𝔚 η on the triple product Z¹(𝔘) × Z¹(𝔙) × C⁰(𝔚) (§4.2/§5 step 1); its kernel is Forster's subspace L (tradeSpace).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Finiteness.tradeDefect_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (x : ↥(NZ1 T T.U) × ↥(NZ1 T T.V) × NC0 T T.W) (p : Fin T.n × Fin T.n) : (tradeDefect T) x p = (restrictCLM ⋯) (↑x.1 p) - (restrictCLM ⋯) (↑x.2.1 p) - ((restrictCLM ⋯) (x.2.2 p.2) - (restrictCLM ⋯) (x.2.2 p.1))

noncomputable def RS.Finiteness.tradeSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : Submodule ℂ (↥(NZ1 T T.U) × ↥(NZ1 T T.V) × NC0 T T.W)

Forster's subspace L (14.6(b)): triples (ζ, ξ, η) with ζ = ξ + δη on 𝔚, packaged as ContinuousLinearMap.ker (closed, hence complete for free).

Equations

• RS.Finiteness.tradeSpace T = (↑(RS.Finiteness.tradeDefect T)).ker

theorem RS.Finiteness.mem_tradeSpace_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (x : ↥(NZ1 T T.U) × ↥(NZ1 T T.V) × NC0 T T.W) : x ∈ tradeSpace T ↔ ∀ (p : Fin T.n × Fin T.n), (tradeDefect T) x p = 0

theorem RS.Finiteness.mem_tradeSpace_iff_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (x : ↥(NZ1 T T.U) × ↥(NZ1 T T.V) × NC0 T T.W) : x ∈ tradeSpace T ↔ ∀ (p : Fin T.n × Fin T.n), (restrictCLM ⋯) (↑x.1 p) = (restrictCLM ⋯) (↑x.2.1 p) + ((restrictCLM ⋯) (x.2.2 p.2) - (restrictCLM ⋯) (x.2.2 p.1))

Membership in L, rearranged to Forster's ζ = ξ + δη shape on each 𝔚-pair (the form TradeBounded.lean's §5 steps 2/6/8 consume).

instance RS.Finiteness.instCompleteSpaceSubtypeProdNC1UMemSubmoduleComplexNZ1VNC0WTradeSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : CompleteSpace ↥(tradeSpace T)

@[instance_reducible]

noncomputable instance RS.Finiteness.instNormedAddCommGroupSubtypeProdNC1UMemSubmoduleComplexNZ1VNC0WTradeSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : NormedAddCommGroup ↥(tradeSpace T)

Equations

• RS.Finiteness.instNormedAddCommGroupSubtypeProdNC1UMemSubmoduleComplexNZ1VNC0WTradeSpace T = (RS.Finiteness.tradeSpace T).normedAddCommGroup

@[instance_reducible]

noncomputable instance RS.Finiteness.instNormedSpaceComplexSubtypeProdNC1UMemSubmoduleNZ1VNC0WTradeSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : NormedSpace ℂ ↥(tradeSpace T)

Equations

• RS.Finiteness.instNormedSpaceComplexSubtypeProdNC1UMemSubmoduleNZ1VNC0WTradeSpace T = (RS.Finiteness.tradeSpace T).normedSpace

noncomputable def RS.Finiteness.tradePi {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : ↥(tradeSpace T) →L[ℂ] ↥(NZ1 T T.V)

The surjective leg π : L →L Z¹(𝔙), (ζ, ξ, η) ↦ ξ (14.6(b)'s projection; surjectivity = the qualitative trade, proved in TradeBounded.lean as tradePi_surjective; the norm constant of 14.6(b) is recovered inside schwartz_finite_cospan by exists_preimage_norm_le — design §5 step 7).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Finiteness.tradeCompact {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : ↥(tradeSpace T) →L[ℂ] ↥(NZ1 T T.V)

The compact leg v : L →L Z¹(𝔙), (ζ, ξ, η) ↦ ζ|𝔙 (compactness = Montel, assembled from isCompactOperator_restrictCLM — deferred, see the end-of-file note).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Finiteness.tradePi_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (x : ↥(tradeSpace T)) : (tradePi T) x = (↑x).2.1

@[simp]

theorem RS.Finiteness.tradeCompact_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (x : ↥(tradeSpace T)) : (tradeCompact T) x = (resZ T T.U T.V ⋯) (↑x).1