OAI/Combinatorics/Progressions/Dynamics/InitialBudgetJointReplacement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.replacementCutoffInputLog line 10
  2. def OAI.Erdos3.replacementCommonInputLog line 13
  3. theorem OAI.Erdos3.replacementCutoffInputLog_bounds line 16
  4. theorem OAI.Erdos3.replacementCommonInputLog_bounds line 33
  5. theorem OAI.Erdos3.replacement_binary_power_le_exp line 52
  6. theorem OAI.Erdos3.replacement_ternary_power_le_exp line 59
  7. theorem OAI.Erdos3.replacementCutoffInputLog_power_bounds line 66
  8. theorem OAI.Erdos3.parameter_min_of_log_scale line 75
  9. theorem OAI.Erdos3.replacement_selected_parameter_bounds line 95
  10. theorem OAI.Erdos3.replacement_common_geometric_bounds line 127
  11. theorem OAI.Erdos3.selectedPhysicalReplacementThreshold_le_exp line 148
  12. theorem OAI.Erdos3.initial_budget_weighted_physical_replacement line 182
  13. theorem OAI.Erdos3.initial_budget_joint_physical_replacement line 268