OAI/Geometry/HeilbronnTriangle/DigitBadTripleAverage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.DigitBadTripleAverage.labelTripleEquiv line 15
  2. theorem OAI.Problem355.DigitBadTripleAverage.uniform_label_average line 21
  3. lemma OAI.Problem355.DigitBadTripleAverage.injective_labels line 39
  4. theorem OAI.Problem355.DigitBadTripleAverage.expectation_le_six line 45
  5. theorem OAI.Problem355.DigitBadTripleAverage.latent_expectation_le_six line 81
  6. theorem OAI.Problem355.DigitBadTripleAverage.expectation_le_six_prime_labels line 100
  7. theorem OAI.Problem355.DigitBadTripleAverage.expectation_le_of_lifting_bound line 120
  8. def OAI.Problem355.DigitColumnLaw.labelsEquiv line 147
  9. theorem OAI.Problem355.DigitColumnLaw.expectation_labels_le_of_repeated line 153
  10. theorem OAI.Problem355.DigitColumnLaw.expectation_triple_le_of_repeated line 177
  11. theorem OAI.Problem355.DigitColumnLaw.bad_triple_expectation_le line 191