OAI/Combinatorics/Progressions/Probability/MeasureGoodAtomTransfer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_measure_productive_good_path line 13
2. theorem OAI.Erdos3.exists_measure_productive_averaged_model_transfer line 34
3. theorem OAI.Erdos3.integral_weighted_model_error_le line 65
4. theorem OAI.Erdos3.exists_measure_productive_path_off_exception line 103
5. theorem OAI.Erdos3.exists_measure_model_transfer_off_exception line 135
6. theorem OAI.Erdos3.exists_measure_averaged_buffered_score line 170
7. theorem OAI.Erdos3.exists_measure_averaged_modeled_discounted_patch line 214
8. theorem OAI.Erdos3.exists_measure_model_transfer_of_good_atom_bounds line 283
9. theorem OAI.Erdos3.exists_measure_model_transfer_of_uniform_good_comparison line 319