OAI/Combinatorics/Progressions/Estimates/PreparedFiniteScheduleUniversalMaskProductiveGood.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.FinitePrecenterInputFamily line 10
  2. structure OAI.Erdos3.FinitePrecenterSelectedModels line 19
  3. def OAI.Erdos3.FinitePrecenterInputFamily.withModels line 27
  4. abbrev OAI.Erdos3.FinitePrecenterValidPrefix line 35
  5. def OAI.Erdos3.FinitePrecenterModelSelection.step line 49
  6. theorem OAI.Erdos3.FinitePrecenterModelSelection.step_eq line 54
  7. def OAI.Erdos3.FinitePrecenterModelSelection.modelPrefix line 60
  8. theorem OAI.Erdos3.FinitePrecenterModelSelection.prefix_zero line 74
  9. theorem OAI.Erdos3.FinitePrecenterModelSelection.prefix_succ line 77
  10. theorem OAI.Erdos3.FinitePrecenterModelSelection.prefix_castSucc line 83
  11. theorem OAI.Erdos3.FinitePrecenterModelSelection.prefix_last line 88
  12. theorem OAI.Erdos3.FinitePrecenterModelSelection.prefix_castLE line 94
  13. def OAI.Erdos3.FinitePrecenterModelSelection.selected line 115
  14. theorem OAI.Erdos3.FinitePrecenterModelSelection.selected_eq_step line 118
  15. theorem OAI.Erdos3.FinitePrecenterModelSelection.selected_eq_withModels line 127
  16. theorem OAI.Erdos3.FinitePrecenterModelSelection.selected_castLE line 135
  17. theorem OAI.Erdos3.FinitePrecenterModelSelection.exists_selection line 142
  18. abbrev OAI.Erdos3.ExternalHistoryMaskIndex line 173
  19. def OAI.Erdos3.externalHistoryMaskFamily line 176
  20. theorem OAI.Erdos3.externalHistoryMaskFamily_at line 184
  21. theorem OAI.Erdos3.externalNetMaskFamily_norm_le line 193
  22. theorem OAI.Erdos3.externalHistoryMaskFamily_norm_le line 205
  23. theorem OAI.Erdos3.externalHistoryMaskFamily_real_norm_le_exp line 217
  24. theorem OAI.Erdos3.externalHistoryMaskIndex_card_le_exp line 230
  25. def OAI.Erdos3.externalHistoryPrecenterInputFamily line 275
  26. theorem OAI.Erdos3.externalHistoryPrecenterInputFamily_input line 282
  27. theorem OAI.Erdos3.externalHistoryPrecenterInputFamily_at line 288
  28. theorem OAI.Erdos3.externalHistoryPrecenterInputFamily_withModels_input line 295
  29. theorem OAI.Erdos3.externalHistoryPrecenterInputFamily_withModels_models line 301
  30. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleExternalMaskProductiveGood line 440
  31. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleUniversalMaskProductiveGood line 618