OAI/Combinatorics/Progressions/Dynamics/ScalarCubeProductRiemannBudget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.scalarCubeGridBoundaryConstant_pos line 13
  2. def OAI.Erdos3.scalarCubeRiemannAllowance line 19
  3. theorem OAI.Erdos3.scalarCubeRiemannAllowance_nonneg line 22
  4. theorem OAI.Erdos3.scalarCubeGrid_small_error_of_length line 29
  5. theorem OAI.Erdos3.scalarCubeResidueWeights_riemann_of_length line 40
  6. def OAI.Erdos3.scalarCubeRiemannLog line 68
  7. theorem OAI.Erdos3.scalarCubeRiemannBoundary_le_exp line 71
  8. def OAI.Erdos3.progressionSliceLengthLog line 118
  9. theorem OAI.Erdos3.progressionSlice_scale_bounds line 121
  10. theorem OAI.Erdos3.scalarCubeRiemannAllowance_mul_mesh_le line 225
  11. theorem OAI.Erdos3.scalarCubeResidueWeights_pi_riemann_of_lengths line 235
  12. theorem OAI.Erdos3.scalarCubeResidueWeights_pi_riemann_uniform_tolerance line 255