OAI/Combinatorics/Progressions/Dynamics/PreparedEarlyStructuralPowerBudget.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.preparationCoordinateCap line 11
  2. def OAI.Erdos3.preparationModulusCap line 13
  3. def OAI.Erdos3.preparationOscillationCap line 16
  4. def OAI.Erdos3.preparationShrink line 19
  5. theorem OAI.Erdos3.preparationShrink_one_le line 23
  6. theorem OAI.Erdos3.preparationCoordinateCap_bounds line 35
  7. theorem OAI.Erdos3.preparation_section_bound line 44
  8. theorem OAI.Erdos3.preparation_step_caps line 60
  9. theorem OAI.Erdos3.preparation_large_side line 82
  10. theorem OAI.Erdos3.preparation_side_loss line 97
  11. theorem OAI.Erdos3.preparationCoordinateCap_real_bound line 123
  12. theorem OAI.Erdos3.exists_preparation_input_power_budget line 136
  13. theorem OAI.Erdos3.early_preparationCoordinateCap_bound line 212
  14. theorem OAI.Erdos3.exists_prepared_early_structural_power_budget line 225