OAI/Topology/CoarseAssembly/ExplicitBoundaryConclusion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.explicitBoundaryStage line 30
2. def OAI.CoarseAssembly.explicitBoundaryClass line 34
3. def OAI.CoarseAssembly.explicitCounterexampleClass line 37
4. def OAI.CoarseAssembly.explicitRealFiberStage line 40
5. theorem OAI.CoarseAssembly.explicitRealFiberStage_cast line 44
6. theorem OAI.CoarseAssembly.explicitBoundaryStage_base_zero line 50
7. theorem OAI.CoarseAssembly.explicitBoundaryClass_base_zero line 58
8. theorem OAI.CoarseAssembly.explicitCounterexampleClass_image line 65
9. theorem OAI.CoarseAssembly.explicitCounterexampleClass_infinite_order line 86
10. theorem OAI.CoarseAssembly.explicitCounterexampleClass_index_zero line 93
11. theorem OAI.CoarseAssembly.bounded_geometry_counterexample_from_index_gap line 99

    Source documentation

    The full geometric conclusion, with only canonical assembly and the fixed-generator published Kazhdan gap remaining. The particular countable class and its filling are proved.

    theorem bounded_geometry_counterexample_from_index_gap
        (index : PublishedBoundaryAssemblyInput) (hgap : PublishedKazhdanInput) :
        ProperSpace VertexUnion ∧ UniformFiniteBalls VertexUnion ∧
          (∀ x y : VertexUnion, x ≠ y → 1 ≤ dist x y) ∧
          ∃ α : KX1 VertexUnion,
            (∀ n : ℤ, n ≠ 0 → n • α ≠ 0) ∧ index.total.assembly α = 0 ∧
            (1 : ℚ) ⊗ₜ[ℤ] α ≠ 0 ∧
            ¬ Function.Injective index.total.assembly ∧
            ¬ Function.Injective (index.total.assembly.toIntLinearMap.lTensor ℚ) := by
    …

    Mentions: OAI.CoarseAssembly.PublishedBoundaryAssemblyInput, OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.UniformFiniteBalls