OAI/Topology/CoarseAssembly/SpatialAveraging.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform spatial approximation from the published gap

The gap hypothesis is the norm estimate for the explicitly defined lazy regular-representation averages. The direct-sum convergence and its identification with the actual spatial constant-fiber projection are proved here, as required by the transfer construction.

  1. def OAI.CoarseAssembly.UniformAveragingGap line 27

    Source documentation

    The precise uniform operator consequence of the Kazhdan estimate for the chosen generators, on the coefficient Hilbert space used by the Roe module. For the standard generators this is the specialization of BHV, Proposition 1.3.2 and Example 1.7.4, described in manuscript §5.2.

    def UniformAveragingGap (S : Finset ArithmeticGroup) (H : Type*)
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Prop :=
…
  2. theorem OAI.CoarseAssembly.fiberAveragingPower_norm line 32
  3. def OAI.CoarseAssembly.spatialAveragingPower line 40
  4. theorem OAI.CoarseAssembly.spatialAveragingPower_tendsto line 45