OAI/Topology/CoarseAssembly/AveragingPropagation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite propagation of the averaging powers

The left regular generators move at most one graph edge. The global lazy average therefore has propagation one, and its powers have the expected linear propagation bound on the actual separated union.

  1. theorem OAI.CoarseAssembly.translation_single_zero line 21
  2. theorem OAI.CoarseAssembly.lazyAverage_single_zero line 33
  3. theorem OAI.CoarseAssembly.leftMove_distance line 53
  4. def OAI.CoarseAssembly.spatialLazyAverage line 74
  5. theorem OAI.CoarseAssembly.spatialLazyAverage_propagation line 79
  6. theorem OAI.CoarseAssembly.spatialAveragingPower_eq_pow line 107
  7. theorem OAI.CoarseAssembly.spatialAveragingPower_propagation line 130
  8. theorem OAI.CoarseAssembly.concrete_transfer_of_gap line 146

    Source documentation

    The concrete spatial transfer now requires only the published uniform Kazhdan-gap specialization for these actual averages.

    theorem concrete_transfer_of_gap (S : Finset ArithmeticGroup) (t : ℤ_[2]ˣ)
    (hS : S.Nonempty) (hgap : UniformAveragingGap S H) :
    letI : MetricSpace VertexUnion := vertexUnionMetric S t
…

    Mentions: OAI.CoarseAssembly.UniformAveragingGap, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.vertexUnionMetric