OAI/Combinatorics/Progressions/Lattices/AffineSliceC2Difference.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.operatorPrecompose line 14
  2. theorem OAI.Erdos3.operatorPrecompose_apply line 18
  3. theorem OAI.Erdos3.operatorPrecompose_norm_le line 21
  4. theorem OAI.Erdos3.affineSlice_fderiv line 27
  5. theorem OAI.Erdos3.affineSlice_fderiv_norm_le line 32
  6. theorem OAI.Erdos3.affineSlice_second_fderiv_norm_le line 42
  7. theorem OAI.Erdos3.second_fderiv_sub line 80
  8. theorem OAI.Erdos3.affineSlice_first_difference_bound line 90
  9. theorem OAI.Erdos3.affineSlice_second_difference_bound line 100
  10. theorem OAI.Erdos3.affineSlice_c2_difference_bound line 115