OAI/Combinatorics/Progressions/Probability/SelectedDensityNormalization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.selectedCoefficientMeasurableEquiv line 11
  2. theorem OAI.Erdos3.selectedCoefficientMeasurableEquiv_preserving line 19
  3. theorem OAI.Erdos3.selectedCoefficientProfile_measure line 29
  4. theorem OAI.Erdos3.selectedCoefficientProfile_integrable line 39
  5. theorem OAI.Erdos3.selectedCoefficient_matrix_apply line 55
  6. theorem OAI.Erdos3.selectedCoefficientDensity_law line 69
  7. theorem OAI.Erdos3.selectedCoefficientEquiv_sub line 103
  8. theorem OAI.Erdos3.selectedCoefficientProfile_input_translate line 111
  9. theorem OAI.Erdos3.selectedCoefficientDensity_input_translate line 119
  10. theorem OAI.Erdos3.selectedCoefficientDensity_normalized_congr line 151