OAI/RingTheory/BassTrace/NormedVectors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A normed ambient space for finitely supported real vectors. The ℓ² norm controls affine topology and triangulations; balls use the separately defined transport metric.

  1. def OAI.BassTrace.Sparse.vectorEmbedding line 16
  2. lemma OAI.BassTrace.Sparse.vectorEmbedding_apply line 20
  3. lemma OAI.BassTrace.Sparse.vectorEmbedding_injective line 27
  4. lemma OAI.BassTrace.Sparse.coordinate_norm_le line 41
  5. def OAI.BassTrace.Sparse.coordinateCLM line 46
  6. lemma OAI.BassTrace.Sparse.coordinateCLM_apply line 49
  7. def OAI.BassTrace.Sparse.finitePairingCLM line 51
  8. lemma OAI.BassTrace.Sparse.finitePairingCLM_apply line 54
  9. lemma OAI.BassTrace.Sparse.finitePairingCLM_vanish line 58
  10. def OAI.BassTrace.Sparse.finsuppRelabelIsometry line 75