CircleInputReduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reducing the circle input to one explicit index computation

theorem OAI.CoarseAssembly.bounded_geometry_counterexample_of_circle_index_one line 19

Source documentation

The circle pairing and winding laws are now proved. Only a circle class whose coordinate index is one is required from circle index theory.

theorem bounded_geometry_counterexample_of_circle_index_one
    (αcircle : LocallyFiniteK1 WindingCircle)
    (hcircle : compactIndexPairing (circleUnitary (ContinuousMap.id WindingCircle)) αcircle = 1)
    (hadd : CountableAdditivityInput CircleFamily) (hfill : CountableAdditivityInput FilledDisc)
    (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 ℚ) :=
…

Mentions: OAI.CoarseAssembly.WindingCircle, OAI.CoarseAssembly.circleUnitary, OAI.CoarseAssembly.CircleFamily, OAI.CoarseAssembly.FilledDisc, OAI.CoarseAssembly.PublishedBoundaryAssemblyInput, OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.UniformFiniteBalls