OAI/Combinatorics/Progressions/Estimates/ScalarCubeBoundaryCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarCubeLinearMap line 12
  2. theorem OAI.Erdos3.scalarCubeLinearMap_apply line 16
  3. theorem OAI.Erdos3.scalarCubeLinearMap_single line 21
  4. theorem OAI.Erdos3.scalarCubeLinearMap_norm_le line 27
  5. theorem OAI.Erdos3.scalarCubeValue_fderiv_norm_le line 34
  6. theorem OAI.Erdos3.scalarCubeFace_fderiv_norm_le line 42
  7. theorem OAI.Erdos3.scalarCubeBoundaryCutoff_compact line 53
  8. theorem OAI.Erdos3.scalarCubeBoundaryCutoff_fderiv_norm_le line 60