OAI/Combinatorics/Progressions/Estimates/ScalarCubeDomain.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.positiveInequalityDomain line 15
  2. theorem OAI.Erdos3.positiveInequalityDomain_isOpen line 18
  3. def OAI.Erdos3.inequalityBoundaryCutoff line 26
  4. theorem OAI.Erdos3.inequalityBoundaryCutoff_range line 30
  5. theorem OAI.Erdos3.inequalityBoundaryCutoff_smooth line 35
  6. theorem OAI.Erdos3.inequalityBoundaryCutoff_tsupport_subset line 40
  7. theorem OAI.Erdos3.inequalityBoundaryCutoff_tsupport_domain line 48
  8. theorem OAI.Erdos3.inequalityBoundaryCutoff_compact line 55
  9. theorem OAI.Erdos3.inequalityBoundaryCutoff_eq_one line 63
  10. theorem OAI.Erdos3.inequalityBoundaryCutoff_fderiv_norm_le line 68
  11. theorem OAI.Erdos3.halfspaceCutoff_measurable line 91
  12. theorem OAI.Erdos3.halfspaceCutoff_integral_loss_le line 95
  13. theorem OAI.Erdos3.inequalityBoundaryCutoff_integral_loss_le line 115
  14. def OAI.Erdos3.scalarCubeValue line 134
  15. theorem OAI.Erdos3.scalarCubeValue_empty line 138
  16. theorem OAI.Erdos3.scalarCubeValue_singleton line 142
  17. theorem OAI.Erdos3.scalarCubeValue_contDiff line 146
  18. def OAI.Erdos3.scalarCubeDomain line 153
  19. def OAI.Erdos3.scalarCubeFace line 156
  20. theorem OAI.Erdos3.scalarCubeFace_contDiff line 160
  21. theorem OAI.Erdos3.positiveInequalityDomain_scalarCubeFace line 167
  22. theorem OAI.Erdos3.scalarCubeDomain_isOpen line 181
  23. theorem OAI.Erdos3.scalarCubeDomain_coordinate_abs_lt_one line 186
  24. theorem OAI.Erdos3.scalarCubeDomain_isBounded line 197
  25. def OAI.Erdos3.scalarCubeCenter line 206
  26. theorem OAI.Erdos3.scalarCubeValue_center line 210
  27. theorem OAI.Erdos3.scalarCubeDomain_nonempty line 214
  28. theorem OAI.Erdos3.scalarCubeFace_card line 221
  29. theorem OAI.Erdos3.booleanAffinePolynomial_eval_scalarCubeValue line 224