OAI/Geometry/HeilbronnTriangle/AuxiliaryWeights.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.AuxiliaryWeights.card_families_mem_le line 19
  2. abbrev OAI.Problem355.AuxiliaryWeights.AffineFamily line 39
  3. theorem OAI.Problem355.AuxiliaryWeights.affine_family_probability_le line 42
  4. theorem OAI.Problem355.AuxiliaryWeights.affine_family_inverse_probability_le line 75
  5. abbrev OAI.Problem355.AuxiliaryWeights.LinearFamily line 106
  6. theorem OAI.Problem355.AuxiliaryWeights.linear_family_probability_le line 109
  7. theorem OAI.Problem355.AuxiliaryWeights.linear_family_inverse_probability_le line 133
  8. theorem OAI.Problem355.AuxiliaryWeights.cubic_space_denominators line 155
  9. theorem OAI.Problem355.AuxiliaryWeights.affine_weight_le line 174
  10. theorem OAI.Problem355.AuxiliaryWeights.pair_weight_le line 186
  11. theorem OAI.Problem355.AuxiliaryWeights.singleton_weight_le line 198
  12. theorem OAI.Problem355.AuxiliaryWeights.affine_weight_le_eight line 210
  13. theorem OAI.Problem355.AuxiliaryWeights.pair_weight_le_four line 218
  14. theorem OAI.Problem355.AuxiliaryWeights.singleton_weight_le_two line 225
  15. theorem OAI.Problem355.AuxiliaryWeights.affine_triple_weight_le_eight line 238
  16. theorem OAI.Problem355.AuxiliaryWeights.linear_pair_weight_le_four line 271
  17. theorem OAI.Problem355.AuxiliaryWeights.nonzero_vector_weight_le_two line 304
  18. def OAI.Problem355.AuxiliaryWeights.affineMapsWithInputShift line 343
  19. theorem OAI.Problem355.AuxiliaryWeights.affineMapsWithInputShift_halfDensity line 346
  20. theorem OAI.Problem355.AuxiliaryWeights.affineMapsWithInputShift_nonempty line 355
  21. theorem OAI.Problem355.AuxiliaryWeights.allowed_shift_affine_weight_le_eight line 363