OAI/Topology/CoarseAssembly/SampledHomotopy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual finite samples of an analytic homotopy

The inactive summands are degenerate character cycles on the same Hilbert space. Thus the ambient countable Hilbert sum does not depend on the samples.

  1. def OAI.CoarseAssembly.Analytic.sampledCycle line 18
  2. theorem OAI.CoarseAssembly.Analytic.sampledCycle_active line 40
  3. theorem OAI.CoarseAssembly.Analytic.sampledCycle_inactive_degenerate line 45
  4. theorem OAI.CoarseAssembly.Analytic.sampledCycle_unital line 54
  5. theorem OAI.CoarseAssembly.Analytic.sampledCycle_selfAdjoint line 64
  6. theorem OAI.CoarseAssembly.Analytic.sampledCycle_norm_le line 73
  7. def OAI.CoarseAssembly.Analytic.sampledFiniteSum line 81
  8. theorem OAI.CoarseAssembly.Analytic.sampledFiniteSum_unital line 88
  9. theorem OAI.CoarseAssembly.Analytic.sampledFiniteSum_selfAdjoint line 94
  10. theorem OAI.CoarseAssembly.Analytic.sampledFiniteSum_norm_le line 100