OAI/Analysis/DiamondDistortion/Relations.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DiamondDistortion.InfimalCost.Relation line 20

   Source documentation

   A prescribed output of finite input coordinates, allowing all countable finite-cost representations rather than only finite ones.

   structure Relation (E F G : Type*) [SeminormedAddCommGroup E] [NormedSpace ℝ E]
       [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] where
   …

2. def OAI.DiamondDistortion.InfimalCost.Relation.seminorm line 28
3. lemma OAI.DiamondDistortion.InfimalCost.Relation.representation_eq line 30
4. lemma OAI.DiamondDistortion.InfimalCost.Relation.le_representation line 36
5. lemma OAI.DiamondDistortion.InfimalCost.Relation.near_representation line 40
6. lemma OAI.DiamondDistortion.InfimalCost.Relation.eq_sInf line 49
7. lemma OAI.DiamondDistortion.InfimalCost.Relation.bound line 59