OAI/Analysis/StrictMeans/TransportBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.StrictInverseFirstPower.upperArea line 11
2. lemma OAI.StrictInverseFirstPower.coe_upperArea_preserving line 13
3. lemma OAI.StrictInverseFirstPower.upperArea_lintegral line 18
4. lemma OAI.StrictInverseFirstPower.upper_source_area_formula line 25
5. lemma OAI.StrictInverseFirstPower.unsignedTargetWeight_height line 36
6. lemma OAI.StrictInverseFirstPower.partnerRatio_weight line 48
7. lemma OAI.StrictInverseFirstPower.fiberSum_indicator line 59
8. lemma OAI.StrictInverseFirstPower.fiberSum_congr line 69
9. lemma OAI.StrictInverseFirstPower.sourcePartner_injectiveOn line 76