OAI/Combinatorics/Progressions/Estimates/MarkedPureEvaluation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.markedShiftEval_lie_of_zero_phase line 15
  2. def OAI.Erdos3.markedBaseEvaluation line 33
  3. theorem OAI.Erdos3.markedBaseEvaluation_map line 40
  4. theorem OAI.Erdos3.markedBaseEvaluation_lie line 44
  5. def OAI.Erdos3.markedBaseEvaluationLie line 57
  6. theorem OAI.Erdos3.markedBaseEvaluationLie_apply line 63
  7. theorem OAI.Erdos3.markedBaseEvaluation_real_map line 68
  8. def OAI.Erdos3.monoidHomOfSurjectiveComposition line 90
  9. theorem OAI.Erdos3.markedBaseEvaluation_real_incl line 110
  10. def OAI.Erdos3.markedPureEvaluation line 119
  11. theorem OAI.Erdos3.markedPureEvaluation_inclusion line 124
  12. def OAI.Erdos3.markedPureEvaluationHom line 139
  13. theorem OAI.Erdos3.markedPureEvaluationHom_coord line 154
  14. theorem OAI.Erdos3.markedPureEvaluationHom_lattice line 164
  15. def OAI.Erdos3.markedPureSpaceMap line 171
  16. theorem OAI.Erdos3.markedPureSpaceMap_mk line 179