OAI/Topology/CoarseAssembly/UniformCycleNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded representatives for countable families

  1. theorem OAI.CoarseAssembly.Analytic.involution_norm_le_one line 14
  2. def OAI.CoarseAssembly.Analytic.normalizedCycle line 23
  3. theorem OAI.CoarseAssembly.Analytic.normalizedCycle_class line 26
  4. theorem OAI.CoarseAssembly.Analytic.normalizedCycle_selfAdjoint line 30
  5. theorem OAI.CoarseAssembly.Analytic.normalizedCycle_sq line 34
  6. theorem OAI.CoarseAssembly.Analytic.normalizedCycle_norm line 38
  7. def OAI.CoarseAssembly.Analytic.normalizedFamilyCycle line 44

    Source documentation

    Actual locally finite cycle for an arbitrary countable family of compact-source cycles.

    def normalizedFamilyCycle (c : ∀ j, OddCycle C(Y j, ℂ)) : OddCycle C₀(Sigma Y, ℂ) :=
…

    Mentions: OAI.CoarseAssembly.Analytic.OddCycle