OAI/Combinatorics/Progressions/Probability/WeightedSliceFamilyLaw.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_pi_transport line 13
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_pi_transport line 40
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_pi_transport_fintype line 51
  4. theorem OAI.Erdos3.finiteImageMass_eq_of_complexMean line 90
  5. def OAI.Erdos3.zeroScalarCubeIntervalEquiv line 108
  6. theorem OAI.Erdos3.integerScalarCubeWeights_zero_mean line 132
  7. theorem OAI.Erdos3.integerScalarCubeWeights_zero_complexMean line 140
  8. theorem OAI.Erdos3.principalTupleIntegers_zero line 159
  9. theorem OAI.Erdos3.principalTupleWeights_zero_complexMean line 169
  10. theorem OAI.Erdos3.principalTupleWeights_zero_mean line 181
  11. theorem OAI.Erdos3.principalTupleWeights_zero_law line 191
  12. theorem OAI.Erdos3.progressionSupportedCube_nonempty line 216
  13. def OAI.Erdos3.uniformProgressionCubeWeights line 226
  14. theorem OAI.Erdos3.uniformProgressionCubeWeights_complexMean line 231
  15. theorem OAI.Erdos3.progressionCubeFamily_complexMean line 237
  16. theorem OAI.Erdos3.progressionCubeBlocks_complexMean line 256
  17. theorem OAI.Erdos3.progressionCubeBlocks_imageMass line 278
  18. theorem OAI.Erdos3.weightedSliceFamily_complexMean line 306
  19. theorem OAI.Erdos3.weightedSliceBlocks_complexMean line 319
  20. def OAI.Erdos3.moderateSliceWeights line 334
  21. theorem OAI.Erdos3.moderateSlice_complexMean line 339
  22. theorem OAI.Erdos3.moderateSliceBlocks_complexMean line 358