OAI/Combinatorics/Progressions/Estimates/DiagonalWrapComparison.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.cyclicCarry line 14
  2. def OAI.Erdos3.circleCarryCutoff line 17
  3. def OAI.Erdos3.smoothCyclicCarry line 20
  4. theorem OAI.Erdos3.circleCarryCutoff_range line 23
  5. theorem OAI.Erdos3.circleCarryCutoff_lipschitz line 26
  6. theorem OAI.Erdos3.circle_dist_half_of_unit_interval line 35
  7. theorem OAI.Erdos3.smoothCyclicCarry_eq_of_outside line 42
  8. theorem OAI.Erdos3.smoothCyclicCarry_mean_error line 85
  9. theorem OAI.Erdos3.exists_smoothCyclicCarry_expansion line 118
  10. theorem OAI.Erdos3.smoothCyclicCarry_fixed_shift_mean_error line 165
  11. theorem OAI.Erdos3.exists_fixed_shift_smoothCyclicCarry_expansion line 193
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quadratic_diagonal_expansion line 216
  13. def OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticDiagonalDerivative line 278
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticMixedTriple line 282
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticDiagonalDerivative_norm line 287
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticMixedTriple_norm line 292
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticDiagonalDerivative_unit line 299
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticMixedTriple_unit line 304
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quadratic_diagonal_derivative_equivalence line 309
  20. def OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicDiagonalDerivative line 367
  21. def OAI.Erdos3.NativeMultidegreeNilcharacter.wrappedDiagonalDerivative line 372
  22. def OAI.Erdos3.NativeMultidegreeNilcharacter.diagonalWrapCoefficient line 376
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.wrappedDiagonalDerivative_norm line 380
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.diagonalWrapCoefficient_norm line 385
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.wrappedDiagonalDerivative_resolution line 390
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicDiagonalDerivative_branches line 410
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_diagonalWrapCoefficient_expansion line 429