OAI/Analysis/DiamondDistortion/InfimalCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DiamondDistortion.InfimalCost.Presentation line 21

   Source documentation

   Quotient construction of the exact infimum over all linear representations. No infimum or supremum is assumed to be attained.

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

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