OAI/Combinatorics/Progressions/Dynamics/BudgetedOpenImageComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.weighted_divergence_pointwise line 15
2. theorem OAI.Erdos3.coordinate_derivative_integrable line 56
3. theorem OAI.Erdos3.weighted_divergence_integral_bound line 64
4. theorem OAI.Erdos3.selectedInverseField_norm_le line 105
5. theorem OAI.Erdos3.selectedInverseField_derivative_norm_le line 119
6. theorem OAI.Erdos3.selected_inverse_divergence_bound line 158
7. theorem OAI.Erdos3.imageTranslationBound_of_inverse_budget line 200
8. theorem OAI.Erdos3.open_domain_image_comparison_of_inverse_bounds line 246