OAI/Combinatorics/Progressions/Estimates/SelectedOutputL1.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.selectedOutputSlice line 14
  2. theorem OAI.Erdos3.selectedOutputSlice_lipschitz line 18
  3. theorem OAI.Erdos3.selectedOutputSlice_support_right line 25
  4. theorem OAI.Erdos3.selectedOutputSlice_support_left line 33
  5. def OAI.Erdos3.retainedSelectedOutputEquiv line 41
  6. theorem OAI.Erdos3.retainedSelectedOutputEquiv_preserving line 46
  7. theorem OAI.Erdos3.retainedSelectedOutput_integrable line 53
  8. theorem OAI.Erdos3.retainedSelectedOutput_integral line 60
  9. theorem OAI.Erdos3.selectedOutput_restricted_l1 line 79