OAI/Analysis/StrictMeans/NormalizedTargets.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.upperArea_ne_zero line 11
2. lemma OAI.StrictInverseFirstPower.expected_source_mass line 22
3. def OAI.StrictInverseFirstPower.badSourceTest line 37
4. lemma OAI.StrictInverseFirstPower.measurable_badSourceTest line 40
5. lemma OAI.StrictInverseFirstPower.badSourceTest_rebase line 43
6. lemma OAI.StrictInverseFirstPower.good_targets_bad_source_mass_zero line 50
7. lemma OAI.StrictInverseFirstPower.affine_law_base_good line 71