OAI/Combinatorics/Progressions/Probability/AdaptiveCouplingComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productTruncatedPairing_sum_left line 18
  2. theorem OAI.Erdos3.productAtomTruncatedPairing_sum_source line 25
  3. theorem OAI.Erdos3.productTruncatedPairing_leaf_partition line 39
  4. theorem OAI.Erdos3.productTruncatedPairing_leaf_partition_empty line 54
  5. def OAI.Erdos3.adaptiveLeafPairMass line 79
  6. theorem OAI.Erdos3.adaptiveLeafPairMass_sum line 83
  7. theorem OAI.Erdos3.adaptiveLeafPairMass_sum_empty line 92
  8. def OAI.Erdos3.adaptiveLeafCouplingWeights line 98
  9. theorem OAI.Erdos3.adaptiveLeafCouplingWeights_mean line 107
  10. theorem OAI.Erdos3.productTruncatedPairing_leaf_sigma line 117
  11. theorem OAI.Erdos3.productTruncatedPairing_leaf_bound line 127
  12. theorem OAI.Erdos3.adaptive_atom_comparison_total line 158