KomorebiSpace.lean

1 import KomorebiSpace.BoundedParity
2 import KomorebiSpace.CayleyHolonomyConditioning
3 import KomorebiSpace.Cohomology
4 import KomorebiSpace.CompositionSite
5 import KomorebiSpace.Correction
6 import KomorebiSpace.EuclideanCertificateCoordinates
7 import KomorebiSpace.Exactification
8 import KomorebiSpace.ExtensionFibers
9 import KomorebiSpace.KernelProjectionBounds
10 import KomorebiSpace.HilbertKernelProjection
11 import KomorebiSpace.LinearExactification
12 import KomorebiSpace.MarkedRealization
13 import KomorebiSpace.MarkedTransport
14 import KomorebiSpace.MarkedBoundaryChange
15 import KomorebiSpace.NormedDefects
16 import KomorebiSpace.ObstructionFloor
17 import KomorebiSpace.OverlapTransport
18 import KomorebiSpace.OverlapPathRepair
19 import KomorebiSpace.HolonomyTransport
20 import KomorebiSpace.AmplifiedTransport
21 import KomorebiSpace.AmplifiedHolonomy
22 import KomorebiSpace.AmplifiedRepair
23 import KomorebiSpace.HolonomyCoordinates
24 import KomorebiSpace.HolonomyRepair
25 import KomorebiSpace.OverlapResidualImage
26 import KomorebiSpace.ProjectiveExample
27 import KomorebiSpace.QuantitativeDescent
28 import KomorebiSpace.DescentClosedRange
29 import KomorebiSpace.Realization
30 import KomorebiSpace.AdjacentResolution
31 import KomorebiSpace.Cofinal
32 import KomorebiSpace.Profiles
33 import KomorebiSpace.ReindexedTransports
34 import KomorebiSpace.EventualCategory
35 import KomorebiSpace.CofinalTransports
36 import KomorebiSpace.RealizationFaithfulness
37 import KomorebiSpace.FiniteObservation
38 import KomorebiSpace.ReindexingExamples
39 import KomorebiSpace.RepairDynamics
40 import KomorebiSpace.RepairProjection
41 import KomorebiSpace.RepairExamples
42 import KomorebiSpace.ResidualPerturbation
43 import KomorebiSpace.MovingKernelBounds
44 import KomorebiSpace.MovingDescent
45 import KomorebiSpace.SplitDefectCharts
46 import KomorebiSpace.CoarseningCascade
47 import KomorebiSpace.CascadeProjections
48 import KomorebiSpace.CascadeLimits
49 import KomorebiSpace.CascadeBoundaryExamples
50 import KomorebiSpace.CascadeDensity
51 import KomorebiSpace.ResidualNaturality
52 import KomorebiSpace.SequenceCascade
53 import KomorebiSpace.SplitKernelPerturbation
54 import KomorebiSpace.Squares
55 import KomorebiSpace.SurjectiveKernelMotion
56 import KomorebiSpace.MovingKernelExamples
57 import KomorebiSpace.Towers
58 import KomorebiSpace.TowerCorrection
59 import KomorebiSpace.BanachTowers
60 import KomorebiSpace.BanachBlocks
61 import KomorebiSpace.BanachTowerExactification
62 import KomorebiSpace.ConstantTower
63 import KomorebiSpace.ResidualSampling
64 import KomorebiSpace.ResidualAliasing
65 import KomorebiSpace.ResidualProfiles
66 import KomorebiSpace.SamplingRepair
67 import KomorebiSpace.SplitTowerRepair
68 import KomorebiSpace.BanachReindexing
69 import KomorebiSpace.ScheduleNormObstruction
70 import KomorebiSpace.SplitTowerSemantics
71 import KomorebiSpace.SplitTowerCoordinates
72 import KomorebiSpace.GrowingTower
73 import KomorebiSpace.IdentityTowerObstruction
74 import KomorebiSpace.SplitTowerCanonicity
75 import KomorebiSpace.DyadicResidualSplit
76 import KomorebiSpace.DyadicResidualDetails
77 import KomorebiSpace.DyadicDetailExamples
78 import KomorebiSpace.DyadicResidualHierarchy
79 import KomorebiSpace.DyadicInfiniteReconstruction
80 import KomorebiSpace.SplitTowerPerturbation
81 import KomorebiSpace.SplittingDependence
82 import KomorebiSpace.ViewSections
83 import KomorebiSpace.GroupViewSystems
84 import KomorebiSpace.CocycleGaugeGroupoid
85 import KomorebiSpace.HolonomyViews
86 import KomorebiSpace.AmplifiedViews
87 import KomorebiSpace.HilbertHolonomyRepair
88 import KomorebiSpace.HolonomyExamples
89 import KomorebiSpace.HolonomyProjection
90 import KomorebiSpace.HolonomyConditioningExample
91 import KomorebiSpace.HolonomyGapCertificate
92 import KomorebiSpace.NonabelianExtension
93 import KomorebiSpace.NonabelianExtensionFibers
94 import KomorebiSpace.PatchViewSystem
95 import KomorebiSpace.SectionExtensionStages
96 import KomorebiSpace.SectionGluing
97 import KomorebiSpace.GaugeDescent
98 import KomorebiSpace.CocycleDescent
99 import KomorebiSpace.EffectiveCocycleDescent
100 import KomorebiSpace.DescentComparison
101 import KomorebiSpace.DescentDataGroupoid
102 import KomorebiSpace.DescentEquivalence
103 import KomorebiSpace.ResolutionViews
104 import KomorebiSpace.BanachViewBridge
105 import KomorebiSpace.SectionObstruction
106 import KomorebiSpace.AdditiveCocycleBridge
107 import KomorebiSpace.OverlapViewBridge
108 import KomorebiSpace.OverlapExamples
109 import KomorebiSpace.AmplifiedExamples
110 import KomorebiSpace.SectionExtensionExample
111 import KomorebiSpace.SectionExtensionFibers
112 import KomorebiSpace.SectionExactSequence
113 import KomorebiSpace.ObstructionRestriction
114 import KomorebiSpace.ExtensionChoiceExample
115 import KomorebiSpace.SiteDescent
116 import KomorebiSpace.StandardDescentBridge
117 import KomorebiSpace.CompositionStack
118 import KomorebiSpace.CompositionSiteExamples
119 import KomorebiSpace.ViewCorrespondence
120 import KomorebiSpace.ViewBoundaryExamples
121 import KomorebiSpace.CocycleExamples
122 import KomorebiSpace.EffectiveDescentExamples
123 import KomorebiSpace.ViewPullback
124 import KomorebiSpace.ViewEquivalence
125 import KomorebiSpace.SectionViewEquivalence
126 import KomorebiSpace.ViewSiteTransport
127 import KomorebiSpace.PatchViewEquivalence
128 import KomorebiSpace.RelativeCocycleRealization
129 import KomorebiSpace.RelativeSections
130 import KomorebiSpace.RelativeAmbiguity
131 import KomorebiSpace.ViewDuplication
132 import KomorebiSpace.FramingBoundaryExamples
133 import KomorebiSpace.WeightedGeometry
134 
135 import KomorebiSpace.FinitePrefixBoundary
136 import KomorebiSpace.DyadicSupport
137 import KomorebiSpace.ProtectedHilbertRepair
138 import KomorebiSpace.ProtectedLinearCertificates
139 import KomorebiSpace.FiniteRealizationExistence

Back to source controls