OAI/Geometry/HeilbronnTriangle/LiftingProbability.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.LiftingProbability.sum_comp_of_constant_fibres line 12
  2. theorem OAI.Problem355.LiftingProbability.sum_uniform_lift line 29
  3. abbrev OAI.Problem355.LiftingProbability.TripleIn line 38
  4. theorem OAI.Problem355.LiftingProbability.card_triples line 41
  5. def OAI.Problem355.LiftingProbability.inclusionMass line 52
  6. theorem OAI.Problem355.LiftingProbability.inclusionMass_nonneg line 57
  7. theorem OAI.Problem355.LiftingProbability.sum_inclusionMass line 64
  8. def OAI.Problem355.LiftingProbability.mainMass line 80
  9. theorem OAI.Problem355.LiftingProbability.mainMass_nonneg line 84
  10. theorem OAI.Problem355.LiftingProbability.sum_mainMass line 89
  11. def OAI.Problem355.LiftingProbability.auxiliaryMass line 98
  12. theorem OAI.Problem355.LiftingProbability.auxiliaryMass_nonneg line 102
  13. theorem OAI.Problem355.LiftingProbability.sum_auxiliaryMass line 107
  14. def OAI.Problem355.LiftingProbability.residueMass line 116
  15. theorem OAI.Problem355.LiftingProbability.sum_residueMass line 121
  16. def OAI.Problem355.LiftingProbability.liftedMass line 130
  17. theorem OAI.Problem355.LiftingProbability.liftedMass_nonneg line 135
  18. theorem OAI.Problem355.LiftingProbability.sum_liftedMass line 143
  19. def OAI.Problem355.LiftingProbability.auxiliaryWeight line 156
  20. theorem OAI.Problem355.LiftingProbability.lifting_normalization line 160
  21. theorem OAI.Problem355.LiftingProbability.liftedMass_eq_weight line 166
  22. theorem OAI.Problem355.LiftingProbability.exact_lifting_identity line 187
  23. def OAI.Problem355.LiftingProbability.conditionalColumnMass line 202
  24. theorem OAI.Problem355.LiftingProbability.conditionalColumnMass_nonneg line 207
  25. theorem OAI.Problem355.LiftingProbability.sum_conditionalColumnMass line 214
  26. theorem OAI.Problem355.LiftingProbability.product_conditionalColumnMass line 244
  27. theorem OAI.Problem355.LiftingProbability.sum_independent_indicators line 272
  28. def OAI.Problem355.LiftingProbability.pushforwardMass line 293
  29. theorem OAI.Problem355.LiftingProbability.averaged_columns_eq_liftedMass line 298