OAI/Combinatorics/SumProduct/Alignment/PivotExtension01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceJointShift.raw_eval_nat line 17
  2. lemma OAI.SourceJointShift.raw_mass_nat line 52
  3. lemma OAI.SourceJointShift.law_eval_nat line 58
  4. lemma OAI.SourceJointShift.law_shift_event line 74
  5. lemma OAI.SourceJointShift.joint_pivot_disintegration line 91
  6. theorem OAI.SourceJointShift.raw_joint_shift line 108
  7. def OAI.SourcePivotExtension.conditioningLabel line 146
  8. def OAI.SourcePivotExtension.conditioningCell line 148
  9. def OAI.SourcePivotExtension.slotEvent line 150
  10. def OAI.SourcePivotExtension.conditionalSlotMass line 154
  11. lemma OAI.SourcePivotExtension.finite_real line 160
  12. lemma OAI.SourcePivotExtension.finite_ratio_bound line 167
  13. lemma OAI.SourcePivotExtension.support_ae line 224
  14. lemma OAI.SourcePivotExtension.joint_real line 236
  15. lemma OAI.SourcePivotExtension.conditional_mass_sum line 245
  16. lemma OAI.SourcePivotExtension.conditional_extension line 257
  17. theorem OAI.SourcePivotExtension.raw_pivot_extension line 278