OAI/Combinatorics/Progressions/Estimates/MixedArrayReference.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.pi_count_measure line 14
  2. theorem OAI.Erdos3.uniformPMF_toMeasure_pi line 22
  3. theorem OAI.Erdos3.pi_smul_finite line 38
  4. def OAI.Erdos3.mixedArrayRegroup line 57
  5. theorem OAI.Erdos3.mixedArrayRegroup_apply line 62
  6. theorem OAI.Erdos3.mixedArrayRegroup_measurePreserving line 65
  7. def OAI.Erdos3.mixedScalarArrayLaw line 78
  8. theorem OAI.Erdos3.mixedScalarArrayLaw_probability line 83
  9. theorem OAI.Erdos3.mixedScalarArrayLaw_regroup line 91
  10. def OAI.Erdos3.mixedArrayReference line 111
  11. instance OAI.Erdos3.mixedArrayReference_sigmaFinite line 115
  12. theorem OAI.Erdos3.mixedArrayRegroup_volume_count line 120
  13. def OAI.Erdos3.orthonormalArrayChart line 131
  14. theorem OAI.Erdos3.orthonormalArrayChart_apply line 137
  15. theorem OAI.Erdos3.orthonormalArrayChart_measurePreserving line 142
  16. theorem OAI.Erdos3.orthonormalArrayChart_scaled_reference line 151
  17. def OAI.Erdos3.arrayResidueChart line 161
  18. theorem OAI.Erdos3.arrayResidueChart_measurePreserving line 166