OAI/Combinatorics/Progressions/Estimates/FourSlicedProductSmoothing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.SlicedProductBlock.pairCapNN line 14
  2. def OAI.Erdos3.SlicedProductBlock.fourDensity line 17
  3. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_cap line 20
  4. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_lipschitz line 27
  5. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_probability_density line 38
  6. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_test_integral line 51
  7. def OAI.Erdos3.SlicedProductBlock.uniformCap line 60
  8. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_uniform_bound line 63
  9. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_of_uniform_slice_width line 83