OAI/Topology/CoarseAssembly/SigmaCycle.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Assembling uniformly bounded normalized Fredholm cycles

  1. theorem OAI.CoarseAssembly.Analytic.norm_commutator_le line 16
  2. def OAI.CoarseAssembly.Analytic.sigmaCycleOperator line 26
  3. theorem OAI.CoarseAssembly.Analytic.sigmaCycleOperator_selfAdjoint line 29
  4. theorem OAI.CoarseAssembly.Analytic.sigmaCycleOperator_sq line 36
  5. def OAI.CoarseAssembly.Analytic.sigmaCommutatorBlocks line 44
  6. theorem OAI.CoarseAssembly.Analytic.sigmaCommutator_norm line 49
  7. theorem OAI.CoarseAssembly.Analytic.sigmaCommutator_uniform_bound line 57
  8. theorem OAI.CoarseAssembly.Analytic.sigmaCommutator_norm_tendsto line 63
  9. theorem OAI.CoarseAssembly.Analytic.sigmaCycleOperator_commutator line 69
  10. def OAI.CoarseAssembly.Analytic.sigmaCycle line 87

    Source documentation

    A countable family of normalized cycles gives an actual locally finite cycle.

    def sigmaCycle (hself : ∀ j, IsSelfAdjoint (c j).operator)
    (hsq : ∀ j, (c j).operator * (c j).operator = 1) : OddCycle C₀(Sigma Y, ℂ) where
…

    Mentions: OAI.CoarseAssembly.Analytic.OddCycle