OAI/Topology/CoarseAssembly/CongruenceSpectral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Applying the integral spectral certificate to the finite congruence fibers

The required gap follows from surjectivity of elementary reduction.

  1. def OAI.CoarseAssembly.elementaryReduction line 21
  2. def OAI.CoarseAssembly.elementaryRegular line 24
  3. def OAI.CoarseAssembly.elementaryLaplacian line 29
  4. theorem OAI.CoarseAssembly.certificateGenerators_subset line 33
  5. theorem OAI.CoarseAssembly.elementaryEnergy_le line 37
  6. theorem OAI.CoarseAssembly.elementaryKernel_projection line 56
  7. theorem OAI.CoarseAssembly.elementaryEnergy_gap line 66
  8. theorem OAI.CoarseAssembly.publishedKazhdanInput_of_elementaryReduction line 79

    Source documentation

    The required published gap follows from the integral certificate and surjectivity onto the specified finite quotients.

    theorem publishedKazhdanInput_of_elementaryReduction
    (hsurj : ∀ k, Function.Surjective (elementaryReduction k)) : PublishedKazhdanInput := by
…

    Mentions: OAI.CoarseAssembly.elementaryReduction, OAI.CoarseAssembly.PublishedKazhdanInput