OAI/Geometry/CylinderCovering/Rational/DictionaryCost.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RationalDictionary.CostTransfer.orthonormalWeight_eq_weight line 11
2. lemma OAI.RationalDictionary.CostTransfer.uncenteredDomain_measurable line 19
3. lemma OAI.RationalDictionary.CostTransfer.labelMap_injective line 32
4. lemma OAI.RationalDictionary.CostTransfer.labelMap_domain line 35
5. lemma OAI.RationalDictionary.CostTransfer.labelMap_deriv line 48
6. lemma OAI.RationalDictionary.CostTransfer.labelMap_abs_det line 60
7. lemma OAI.RationalDictionary.CostTransfer.labelMap_integral line 66
8. lemma OAI.RationalDictionary.CostTransfer.weight_dictionary line 73
9. theorem OAI.RationalDictionary.CostTransfer.weightedCost_dictionary line 92
10. theorem OAI.RationalDictionary.CostTransfer.cost_dictionary line 113