CircleCoefficient.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

An unconditional circle class of coordinate index one

def OAI.CoarseAssembly.Analytic.compactFunctionForget line 16
theorem OAI.CoarseAssembly.Analytic.compactFunctionForget_lift line 24
def OAI.CoarseAssembly.Analytic.negativeCircleClass line 29
theorem OAI.CoarseAssembly.Analytic.negativeCircleClass_coordinate_index line 32
def OAI.CoarseAssembly.circleFundamental line 44
theorem OAI.CoarseAssembly.circleFundamental_coordinate_index line 48
def OAI.CoarseAssembly.provedCircleInput line 67
Source documentation
The complete published circle-index input, now a theorem.
```
def provedCircleInput : PublishedCircleInput :=
…
```
Mentions: OAI.CoarseAssembly.PublishedCircleInput

theorem OAI.CoarseAssembly.bounded_geometry_counterexample_from_additivity_index_gap line 76

Source documentation

Main theorem with the circle and compact-filling inputs discharged.

theorem bounded_geometry_counterexample_from_additivity_index_gap
    (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.CircleFamily, OAI.CoarseAssembly.FilledDisc, OAI.CoarseAssembly.PublishedBoundaryAssemblyInput, OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.UniformFiniteBalls