OAI/Analysis/StrictMeans/PairingCovariance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.sourcePartner_eq_available line 11
  2. lemma OAI.StrictInverseFirstPower.sourcePairingDomain_rebase_iff line 22
  3. lemma OAI.StrictInverseFirstPower.sourcePartner_rebase line 32
  4. def OAI.StrictInverseFirstPower.partnerRatio line 45
  5. lemma OAI.StrictInverseFirstPower.measurable_partnerRatio line 52
  6. lemma OAI.StrictInverseFirstPower.partnerRatio_gt_one line 59
  7. lemma OAI.StrictInverseFirstPower.partnerRatio_nonneg line 68
  8. lemma OAI.StrictInverseFirstPower.partnerRatio_rebase line 74
  9. def OAI.StrictInverseFirstPower.truncatedPairingDomain line 88
  10. lemma OAI.StrictInverseFirstPower.measurableSet_truncatedPairingDomain line 93
  11. lemma OAI.StrictInverseFirstPower.affineProduct_re line 104
  12. lemma OAI.StrictInverseFirstPower.truncatedPairingDomain_rebase line 107