OAI/Topology/CoarseAssembly/Definitions.lean

GitHub source file

198 declarations, 0 contain sorry, 0 declared as axioms

A bounded-geometry counterexample to coarse Novikov

The concrete graph union has an infinite-order class killed by its ordinary reduced coarse assembly map, including after rationalization.

  1. def OAI.CoarseAssembly.blockLinear line 31

    Also declared: ComparatorChallenges/CoarseAssembly.lean:31 (same declaration text).

  2. def OAI.CoarseAssembly.blockOperator line 40

    Also declared: ComparatorChallenges/CoarseAssembly.lean:40 (same declaration text).

  3. def OAI.CoarseAssembly.blockIsometry line 63

    Also declared: ComparatorChallenges/CoarseAssembly.lean:63 (same declaration text).

  4. def OAI.CoarseAssembly.flattenVector line 96

    Also declared: ComparatorChallenges/CoarseAssembly.lean:96 (same declaration text).

  5. def OAI.CoarseAssembly.rowVector line 128

    Also declared: ComparatorChallenges/CoarseAssembly.lean:128 (same declaration text).

  6. def OAI.CoarseAssembly.unflattenVector line 144

    Also declared: ComparatorChallenges/CoarseAssembly.lean:144 (same declaration text).

  7. def OAI.CoarseAssembly.flattenEquiv line 168

    Also declared: ComparatorChallenges/CoarseAssembly.lean:168 (same declaration text).

  8. def OAI.CoarseAssembly.operatorConjugation line 262

    Also declared: ComparatorChallenges/CoarseAssembly.lean:262 (same declaration text).

  9. def OAI.CoarseAssembly.operatorConjugationHom line 265

    Also declared: ComparatorChallenges/CoarseAssembly.lean:265 (same declaration text).

  10. abbrev OAI.CoarseAssembly.Congruence.ArithmeticGroup line 302

    Also declared: ComparatorChallenges/CoarseAssembly.lean:302 (same declaration text).

  11. abbrev OAI.CoarseAssembly.Congruence.Quotient line 304

    Also declared: ComparatorChallenges/CoarseAssembly.lean:304 (same declaration text).

  12. def OAI.CoarseAssembly.Congruence.reduce line 306

    Also declared: ComparatorChallenges/CoarseAssembly.lean:306 (same declaration text).

  13. def OAI.CoarseAssembly.Congruence.diagonal line 309

    Also declared: ComparatorChallenges/CoarseAssembly.lean:309 (same declaration text).

  14. def OAI.CoarseAssembly.Congruence.holonomy line 313

    Also declared: ComparatorChallenges/CoarseAssembly.lean:313 (same declaration text).

  15. def OAI.CoarseAssembly.Congruence.residueMap line 324

    Also declared: ComparatorChallenges/CoarseAssembly.lean:324 (same declaration text).

  16. def OAI.CoarseAssembly.Congruence.quotientMap line 327

    Also declared: ComparatorChallenges/CoarseAssembly.lean:327 (same declaration text).

  17. def OAI.CoarseAssembly.flattenOperator line 345

    Also declared: ComparatorChallenges/CoarseAssembly.lean:345 (same declaration text).

  18. def OAI.CoarseAssembly.discreteGraphMetric line 366

    Also declared: ComparatorChallenges/CoarseAssembly.lean:366 (same declaration text).

  19. def OAI.CoarseAssembly.connectedGraphMetric line 381

    Also declared: ComparatorChallenges/CoarseAssembly.lean:381 (same declaration text).

  20. def OAI.CoarseAssembly.graphMetricOrDiscrete line 393

    Also declared: ComparatorChallenges/CoarseAssembly.lean:393 (same declaration text).

  21. def OAI.CoarseAssembly.separatedDist line 411

    Also declared: ComparatorChallenges/CoarseAssembly.lean:411 (same declaration text).

  22. def OAI.CoarseAssembly.separatedMetric line 415

    Also declared: ComparatorChallenges/CoarseAssembly.lean:415 (same declaration text).

  23. abbrev OAI.CoarseAssembly.DiscreteRoe.Module line 595

    Also declared: ComparatorChallenges/CoarseAssembly.lean:595 (same declaration text).

  24. abbrev OAI.CoarseAssembly.DiscreteRoe.Operator line 597

    Also declared: ComparatorChallenges/CoarseAssembly.lean:597 (same declaration text).

  25. def OAI.CoarseAssembly.DiscreteRoe.insert line 600

    Also declared: ComparatorChallenges/CoarseAssembly.lean:600 (same declaration text).

  26. def OAI.CoarseAssembly.DiscreteRoe.coordinate line 603

    Also declared: ComparatorChallenges/CoarseAssembly.lean:603 (same declaration text).

  27. def OAI.CoarseAssembly.DiscreteRoe.entry line 606

    Also declared: ComparatorChallenges/CoarseAssembly.lean:606 (same declaration text).

  28. def OAI.CoarseAssembly.DiscreteRoe.CompactEntries line 609

    Also declared: ComparatorChallenges/CoarseAssembly.lean:609 (same declaration text).

  29. def OAI.CoarseAssembly.DiscreteRoe.PropagationLE line 620

    Also declared: ComparatorChallenges/CoarseAssembly.lean:620 (same declaration text).

  30. def OAI.CoarseAssembly.DiscreteRoe.Generator line 623

    Also declared: ComparatorChallenges/CoarseAssembly.lean:623 (same declaration text).

  31. def OAI.CoarseAssembly.DiscreteRoe.algebra line 626

    Also declared: ComparatorChallenges/CoarseAssembly.lean:626 (same declaration text).

  32. instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 629) line 629
  33. def OAI.CoarseAssembly.DiscreteRoe.MapsToRoe line 664

    Also declared: ComparatorChallenges/CoarseAssembly.lean:664 (same declaration text).

  34. def OAI.CoarseAssembly.DiscreteRoe.conjugationHom line 668

    Also declared: ComparatorChallenges/CoarseAssembly.lean:668 (same declaration text).

  35. def OAI.CoarseAssembly.UniformFiniteBalls line 692

    Also declared: ComparatorChallenges/CoarseAssembly.lean:692 (same declaration text).

  36. abbrev OAI.CoarseAssembly.LatticeVertex line 711

    Also declared: ComparatorChallenges/CoarseAssembly.lean:711 (same declaration text).

  37. def OAI.CoarseAssembly.latticeRadius line 713

    Also declared: ComparatorChallenges/CoarseAssembly.lean:713 (same declaration text).

  38. def OAI.CoarseAssembly.triangularGraph line 716

    Also declared: ComparatorChallenges/CoarseAssembly.lean:716 (same declaration text).

  39. def OAI.CoarseAssembly.Disc line 722

    Also declared: ComparatorChallenges/CoarseAssembly.lean:722 (same declaration text).

  40. instance OAI.CoarseAssembly.(instance at line 724) line 724
  41. def OAI.CoarseAssembly.discGraph line 737

    Also declared: ComparatorChallenges/CoarseAssembly.lean:737 (same declaration text).

  42. def OAI.CoarseAssembly.discDepth line 742

    Also declared: ComparatorChallenges/CoarseAssembly.lean:742 (same declaration text).

  43. def OAI.CoarseAssembly.latticeCharge line 752

    Also declared: ComparatorChallenges/CoarseAssembly.lean:752 (same declaration text).

  44. def OAI.CoarseAssembly.Congruence.chosenHolonomyUnit line 786

    Also declared: ComparatorChallenges/CoarseAssembly.lean:786 (same declaration text).

  45. def OAI.CoarseAssembly.symmetricMoves line 843

    Also declared: ComparatorChallenges/CoarseAssembly.lean:843 (same declaration text).

  46. abbrev OAI.CoarseAssembly.FiberVertex line 846

    Also declared: ComparatorChallenges/CoarseAssembly.lean:846 (same declaration text).

  47. instance OAI.CoarseAssembly.(instance at line 848) line 848
  48. def OAI.CoarseAssembly.fiberCoordinate line 850

    Also declared: ComparatorChallenges/CoarseAssembly.lean:850 (same declaration text).

  49. def OAI.CoarseAssembly.fiberCharge line 853

    Also declared: ComparatorChallenges/CoarseAssembly.lean:853 (same declaration text).

  50. def OAI.CoarseAssembly.LiftStep line 856

    Also declared: ComparatorChallenges/CoarseAssembly.lean:856 (same declaration text).

  51. def OAI.CoarseAssembly.fiberedGraph line 864

    Also declared: ComparatorChallenges/CoarseAssembly.lean:864 (same declaration text).

  52. def OAI.CoarseAssembly.discBoundaryBase line 921

    Also declared: ComparatorChallenges/CoarseAssembly.lean:921 (same declaration text).

  53. def OAI.CoarseAssembly.fiberBoundaryBase line 926

    Also declared: ComparatorChallenges/CoarseAssembly.lean:926 (same declaration text).

  54. abbrev OAI.CoarseAssembly.BaseUnion line 940

    Also declared: ComparatorChallenges/CoarseAssembly.lean:940 (same declaration text).

  55. abbrev OAI.CoarseAssembly.BaseFiber line 942

    Also declared: ComparatorChallenges/CoarseAssembly.lean:942 (same declaration text).

  56. abbrev OAI.CoarseAssembly.VertexUnion line 944

    Also declared: ComparatorChallenges/CoarseAssembly.lean:944 (same declaration text).

  57. instance OAI.CoarseAssembly.baseUnionDecidableEq line 946

    Also declared: ComparatorChallenges/CoarseAssembly.lean:946 (same declaration text).

  58. instance OAI.CoarseAssembly.vertexUnionDecidableEq line 948

    Also declared: ComparatorChallenges/CoarseAssembly.lean:948 (same declaration text).

  59. def OAI.CoarseAssembly.componentMetric line 951

    Also declared: ComparatorChallenges/CoarseAssembly.lean:951 (same declaration text).

  60. def OAI.CoarseAssembly.componentUnionMetric line 955

    Also declared: ComparatorChallenges/CoarseAssembly.lean:955 (same declaration text).

  61. def OAI.CoarseAssembly.vertexUnionMetric line 960

    Also declared: ComparatorChallenges/CoarseAssembly.lean:960 (same declaration text).

  62. def OAI.CoarseAssembly.positiveElementaryMove line 978

    Also declared: ComparatorChallenges/CoarseAssembly.lean:978 (same declaration text).

  63. def OAI.CoarseAssembly.elementaryMoves line 981

    Also declared: ComparatorChallenges/CoarseAssembly.lean:981 (same declaration text).

  64. abbrev OAI.CoarseAssembly.AmpleSpace line 985

    Also declared: ComparatorChallenges/CoarseAssembly.lean:985 (same declaration text).

  65. structure OAI.CoarseAssembly.Analytic.HilbertSpace line 1000

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1000 (same declaration text).

  66. instance OAI.CoarseAssembly.Analytic.(instance at line 1010) line 1010
  67. abbrev OAI.CoarseAssembly.Analytic.End line 1012

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1012 (same declaration text).

  68. structure OAI.CoarseAssembly.Analytic.OddCycle line 1016

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1016 (same declaration text).

  69. def OAI.CoarseAssembly.Analytic.OddCycle.Degenerate line 1031

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1031 (same declaration text).

  70. def OAI.CoarseAssembly.Analytic.OddCycle.precomp line 1036

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1036 (same declaration text).

  71. structure OAI.CoarseAssembly.Analytic.OddCycle.UnitaryEquivalent line 1044

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1044 (same declaration text).

  72. def OAI.CoarseAssembly.Analytic.OddCycle.UnitaryEquivalent.precomp line 1050

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1050 (same declaration text).

  73. structure OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum line 1056

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1056 (same declaration text).

  74. def OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.precomp line 1068

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1068 (same declaration text).

  75. abbrev OAI.CoarseAssembly.Analytic.Interval line 1079

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1079 (same declaration text).

  76. def OAI.CoarseAssembly.Analytic.start line 1081

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1081 (same declaration text).

  77. def OAI.CoarseAssembly.Analytic.finish line 1083

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1083 (same declaration text).

  78. structure OAI.CoarseAssembly.Analytic.OddHomotopy line 1085

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1085 (same declaration text).

  79. def OAI.CoarseAssembly.Analytic.OddHomotopy.eval line 1100

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1100 (same declaration text).

  80. def OAI.CoarseAssembly.Analytic.OddHomotopy.precomp line 1108

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1108 (same declaration text).

  81. inductive OAI.CoarseAssembly.Analytic.CycleRelation line 1135

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1135 (same declaration text).

  82. def OAI.CoarseAssembly.Analytic.relations line 1145

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1145 (same declaration text).

  83. abbrev OAI.CoarseAssembly.Analytic.OddK line 1148

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1148 (same declaration text).

  84. def OAI.CoarseAssembly.Analytic.cycleClass line 1150

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1150 (same declaration text).

  85. def OAI.CoarseAssembly.Analytic.precompFree line 1157

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1157 (same declaration text).

  86. def OAI.CoarseAssembly.Analytic.precomp line 1160

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1160 (same declaration text).

  87. def OAI.CoarseAssembly.Analytic.OddCycle.compactPerturb line 1242

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1242 (same declaration text).

  88. def OAI.CoarseAssembly.Analytic.OddCycle.localCompactPerturb line 1337

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1337 (same declaration text).

  89. def OAI.CoarseAssembly.Analytic.symmetricCutDown line 1408

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1408 (same declaration text).

  90. def OAI.CoarseAssembly.Analytic.OddCycle.scalarRestriction line 1424

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1424 (same declaration text).

  91. def OAI.CoarseAssembly.Analytic.representedCorrection line 1440

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1440 (same declaration text).

  92. def OAI.CoarseAssembly.Analytic.OddCycle.cutDown line 1443

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1443 (same declaration text).

  93. def OAI.CoarseAssembly.Analytic.completedRepresentation line 1605

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1605 (same declaration text).

  94. def OAI.CoarseAssembly.Analytic.OddCycle.characterExtension line 1661

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1661 (same declaration text).

  95. abbrev OAI.CoarseAssembly.Analytic.LocallyFiniteK1 line 1716

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1716 (same declaration text).

  96. def OAI.CoarseAssembly.Analytic.pullback line 1718

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1718 (same declaration text).

  97. def OAI.CoarseAssembly.Analytic.pushforward line 1722

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1722 (same declaration text).

  98. structure OAI.CoarseAssembly.Analytic.Coarsening line 1725

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1725 (same declaration text).

  99. def OAI.CoarseAssembly.Analytic.Coarsening.map line 1737

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1737 (same declaration text).

  100. abbrev OAI.CoarseAssembly.Analytic.Coarsening.Homology line 1741

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1741 (same declaration text).

  101. structure OAI.CoarseAssembly.Rips.Point line 1761

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1761 (same declaration text).

  102. def OAI.CoarseAssembly.Rips.coordinates line 1769

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1769 (same declaration text).

  103. instance OAI.CoarseAssembly.Rips.(instance at line 1771) line 1771
  104. instance OAI.CoarseAssembly.Rips.(instance at line 1774) line 1774
  105. def OAI.CoarseAssembly.Rips.coarsen line 1787

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1787 (same declaration text).

  106. def OAI.CoarseAssembly.Rips.inclusion line 1793

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1793 (same declaration text).

  107. def OAI.CoarseAssembly.Rips.coarsening line 1866

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1866 (same declaration text).

  108. abbrev OAI.CoarseAssembly.Rips.KX1 line 1897

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1897 (same declaration text).

  109. def OAI.CoarseAssembly.Rips.vertex line 1916

    Also declared: ComparatorChallenges/CoarseAssembly.lean:1916 (same declaration text).

  110. instance OAI.CoarseAssembly.Rips.(instance at line 1945) line 1945
  111. def OAI.CoarseAssembly.Analytic.zeroExtension line 2062

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2062 (same declaration text).

  112. def OAI.CoarseAssembly.Analytic.zeroExtensionHom line 2085

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2085 (same declaration text).

  113. def OAI.CoarseAssembly.Analytic.cayleyDenominator line 2174

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2174 (same declaration text).

  114. def OAI.CoarseAssembly.Analytic.cayleyUnitary line 2192

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2192 (same declaration text).

  115. def OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary line 2233

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2233 (same declaration text).

  116. def OAI.CoarseAssembly.Analytic.boundedTransform line 2251

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2251 (same declaration text).

  117. def OAI.CoarseAssembly.Analytic.OddCycle.bounded line 2276

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2276 (same declaration text).

  118. def OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint line 2482

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2482 (same declaration text).

  119. def OAI.CoarseAssembly.Analytic.OddCycle.regularize line 2597

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2597 (same declaration text).

  120. def OAI.CoarseAssembly.Rips.sqrtCoordinate line 2734

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2734 (same declaration text).

  121. def OAI.CoarseAssembly.DiscreteRoe.partitionMap line 2766

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2766 (same declaration text).

  122. def OAI.CoarseAssembly.DiscreteRoe.partitionIsometry line 2769

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2769 (same declaration text).

  123. def OAI.CoarseAssembly.DiscreteRoe.constantBlock line 2823

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2823 (same declaration text).

  124. def OAI.CoarseAssembly.DiscreteRoe.partitionCompression line 2826

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2826 (same declaration text).

  125. def OAI.CoarseAssembly.isometricExtension line 2845

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2845 (same declaration text).

  126. def OAI.CoarseAssembly.DiscreteRoe.algebraicRoe line 2874

    Also declared: ComparatorChallenges/CoarseAssembly.lean:2874 (same declaration text).

  127. def OAI.CoarseAssembly.DiscreteRoe.RoeMultiplier line 3154

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3154 (same declaration text).

  128. def OAI.CoarseAssembly.DiscreteRoe.roeIdealizer line 3158

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3158 (same declaration text).

  129. def OAI.CoarseAssembly.DiscreteRoe.localizedSpatialOperator line 3204

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3204 (same declaration text).

  130. def OAI.CoarseAssembly.Rips.representedSqrt line 3225

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3225 (same declaration text).

  131. def OAI.CoarseAssembly.Rips.ripsSpatialOperator line 3228

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3228 (same declaration text).

  132. def OAI.CoarseAssembly.extendedFunction line 3294

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3294 (same declaration text).

  133. def OAI.CoarseAssembly.inclusionVector line 3297

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3297 (same declaration text).

  134. def OAI.CoarseAssembly.inclusionIsometry line 3340

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3340 (same declaration text).

  135. def OAI.CoarseAssembly.Analytic.ampleIsometry line 3430

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3430 (same declaration text).

  136. def OAI.CoarseAssembly.DiscreteRoe.coefficientIsometry line 3478

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3478 (same declaration text).

  137. def OAI.CoarseAssembly.DiscreteRoe.coefficientExtension line 3483

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3483 (same declaration text).

  138. def OAI.CoarseAssembly.DiscreteRoe.diagonalFamily line 3502

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3502 (same declaration text).

  139. def OAI.CoarseAssembly.Rips.mapPoint line 3526

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3526 (same declaration text).

  140. def OAI.CoarseAssembly.Rips.unmapPoint line 3542

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3542 (same declaration text).

  141. def OAI.CoarseAssembly.separatedComponent line 3571

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3571 (same declaration text).

  142. abbrev OAI.CoarseAssembly.TopologicalK1.InvertibleMatrix line 3590

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3590 (same declaration text).

  143. abbrev OAI.CoarseAssembly.TopologicalK1.StableGL line 3592

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3592 (same declaration text).

  144. def OAI.CoarseAssembly.TopologicalK1.IsStabilization line 3594

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3594 (same declaration text).

  145. inductive OAI.CoarseAssembly.TopologicalK1.Relation line 3599

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3599 (same declaration text).

  146. def OAI.CoarseAssembly.TopologicalK1.relations line 3608

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3608 (same declaration text).

  147. abbrev OAI.CoarseAssembly.TopologicalK1.Group line 3611

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3611 (same declaration text).

  148. def OAI.CoarseAssembly.TopologicalK1.matrixClass line 3613

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3613 (same declaration text).

  149. def OAI.CoarseAssembly.TopologicalK1.mapGL line 3620

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3620 (same declaration text).

  150. def OAI.CoarseAssembly.TopologicalK1.mapFree line 3623

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3623 (same declaration text).

  151. def OAI.CoarseAssembly.TopologicalK1.map line 3626

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3626 (same declaration text).

  152. def OAI.CoarseAssembly.OperatorKTheory.scalarMap line 3742

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3742 (same declaration text).

  153. abbrev OAI.CoarseAssembly.OperatorKTheory.K1 line 3745

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3745 (same declaration text).

  154. def OAI.CoarseAssembly.OperatorKTheory.unitizationMap line 3751

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3751 (same declaration text).

  155. def OAI.CoarseAssembly.OperatorKTheory.map line 3755

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3755 (same declaration text).

  156. def OAI.CoarseAssembly.OperatorKTheory.relativePart line 3801

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3801 (same declaration text).

  157. def OAI.CoarseAssembly.OperatorKTheory.relativeUnitary line 3803

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3803 (same declaration text).

  158. def OAI.CoarseAssembly.OperatorKTheory.relativeMatrix line 3842

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3842 (same declaration text).

  159. def OAI.CoarseAssembly.OperatorKTheory.relativeClass line 3848

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3848 (same declaration text).

  160. def OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra line 3914

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3914 (same declaration text).

  161. instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 3935) line 3935
  162. def OAI.CoarseAssembly.DiscreteRoe.multiplierRoeIdeal line 3965

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3965 (same declaration text).

  163. def OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryUnitary line 3973

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3973 (same declaration text).

  164. def OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass line 3978

    Also declared: ComparatorChallenges/CoarseAssembly.lean:3978 (same declaration text).

  165. def OAI.CoarseAssembly.DiscreteRoe.separatedFamilyMultiplier line 4108

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4108 (same declaration text).

  166. def OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary line 4460

    Source comment

    The self-contained construction includes its support proofs.

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4460 (same declaration text).

    def separatedFamilyBoundary (hself : ∀ i, IsSelfAdjoint (A i))
    (hsq : ∀ i, IsCompactOperator ((A i * A i - (1 : OAI.CoarseAssembly.DiscreteRoe.Operator (V i) H)).toFun)) :
    letI := OAI.CoarseAssembly.separatedMetric o
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.separatedMetric

  167. def OAI.CoarseAssembly.DiscreteRoe.partitionConjugate line 4878

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4878 (same declaration text).

  168. def OAI.CoarseAssembly.Analytic.localizedOperator line 4919

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4919 (same declaration text).

  169. def OAI.CoarseAssembly.Analytic.localizedCycle line 4922

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4922 (same declaration text).

  170. def OAI.CoarseAssembly.Rips.ampleRipsOperator line 4987

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4987 (same declaration text).

  171. def OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary line 4995

    Source comment

    The self-contained construction includes its support proofs.

    Also declared: ComparatorChallenges/CoarseAssembly.lean:4995 (same declaration text).

    def ampleRipsFamilyBoundary (o : ∀ i, V i) (r : ℝ) (hr : 0 ≤ r)
    (c : ∀ i, OAI.CoarseAssembly.Analytic.OddCycle C(OAI.CoarseAssembly.Rips.Point (V i) r, ℂ)) (hπ : ∀ i, (c i).representation 1 = 1)
    (hF : ∀ i, IsSelfAdjoint (c i).operator)
    (C : ℝ) (hC : 0 ≤ C) (hnorm : ∀ i, ‖(c i).operator‖ ≤ C) :
    letI := OAI.CoarseAssembly.separatedMetric o
…

    Mentions: OAI.CoarseAssembly.Analytic.OddCycle, OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.separatedMetric

  172. def OAI.CoarseAssembly.DiscreteRoe.inclusionHom line 5312

    Source comment

    The self-contained construction includes its support proofs.

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5312 (same declaration text).

    def inclusionHom (e : X ↪ Y) (he : ∀ x y, dist (e x) (e y) ≤ dist x y) :
    OAI.CoarseAssembly.DiscreteRoe.algebra (X := X) (H := H) →⋆ₙₐ[ℂ] OAI.CoarseAssembly.DiscreteRoe.algebra (X := Y) (H := H) := by
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.algebra

  173. structure OAI.CoarseAssembly.Rips.ControlledCycleFamily line 5456

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5456 (same declaration text).

  174. def OAI.CoarseAssembly.Rips.ControlledCycleFamily.boundary line 5466

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5466 (same declaration text).

  175. def OAI.CoarseAssembly.Rips.regularizedFamily line 5491

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5491 (same declaration text).

  176. def OAI.CoarseAssembly.Rips.analyticFamilyIndexFree line 5762

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5762 (same declaration text).

  177. def OAI.CoarseAssembly.Rips.analyticFamilyIndex line 5772

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5772 (same declaration text).

  178. def OAI.CoarseAssembly.separatedRipsMap line 5803

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5803 (same declaration text).

  179. def OAI.CoarseAssembly.separatedRipsEmbedding line 5845

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5845 (same declaration text).

  180. def OAI.CoarseAssembly.Analytic.compactFunctionLift line 5901

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5901 (same declaration text).

  181. def OAI.CoarseAssembly.Rips.lateRipsFunctionHom line 5928

    Also declared: ComparatorChallenges/CoarseAssembly.lean:5928 (same declaration text).

  182. def OAI.CoarseAssembly.Rips.ripsPointCharacter line 6093

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6093 (same declaration text).

  183. def OAI.CoarseAssembly.Rips.separatedRipsIndex line 6097

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6097 (same declaration text).

  184. structure OAI.CoarseAssembly.Analytic.CoarseningMorphism line 6180

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6180 (same declaration text).

  185. structure OAI.CoarseAssembly.Analytic.CompatibleIndexFamily line 6186

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6186 (same declaration text).

  186. def OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.assembly line 6197

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6197 (same declaration text).

  187. def OAI.CoarseAssembly.Rips.separatedIndexFamily line 6219

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6219 (same declaration text).

  188. def OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.transport line 6249

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6249 (same declaration text).

  189. def OAI.CoarseAssembly.Rips.embeddingMap line 6313

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6313 (same declaration text).

  190. def OAI.CoarseAssembly.Rips.embeddingCoarsening line 6452

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6452 (same declaration text).

  191. def OAI.CoarseAssembly.TotalRoe line 6489

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6489 (same declaration text).

  192. instance OAI.CoarseAssembly.(instance at line 6491) line 6491
  193. abbrev OAI.CoarseAssembly.FiberedUnion line 6510

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6510 (same declaration text).

  194. def OAI.CoarseAssembly.totalToFiber line 6533

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6533 (same declaration text).

  195. def OAI.CoarseAssembly.totalToFiberCoarsening line 6536

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6536 (same declaration text).

  196. def OAI.CoarseAssembly.fiberReindexRoeHom line 6569

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6569 (same declaration text).

  197. def OAI.CoarseAssembly.constructedTotalIndex line 6591

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6591 (same declaration text).

  198. def OAI.CoarseAssembly.constructedCoarseAssembly line 6610

    Also declared: ComparatorChallenges/CoarseAssembly.lean:6610 (same declaration text).