OAI/Combinatorics/Progressions/Estimates/BooleanSelectedDerivativeBound.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.imageTranslationBound_of_weighted_fields line 20
  2. theorem OAI.Erdos3.imageTranslationBound_of_right_inverse_fields line 34
  3. theorem OAI.Erdos3.divergence_image_comparison line 66
  4. theorem OAI.Erdos3.local_weighted_image_derivative_identity line 121
  5. theorem OAI.Erdos3.local_weighted_image_derivative_bound line 143
  6. theorem OAI.Erdos3.imageTranslationBound_of_local_weighted_fields line 166
  7. theorem OAI.Erdos3.contDiff_mul_of_local_right line 192
  8. def OAI.Erdos3.selectedDerivative line 206
  9. def OAI.Erdos3.selectedInverseField line 210
  10. theorem OAI.Erdos3.selectedInverseField_contDiffAt line 214
  11. theorem OAI.Erdos3.selectedInverseField_column line 227
  12. theorem OAI.Erdos3.selectedWeightedField_spec line 234
  13. theorem OAI.Erdos3.imageTranslationBound_of_selected_inverse line 251
  14. def OAI.Erdos3.booleanSelectedInjection line 271
  15. theorem OAI.Erdos3.booleanSelectedInjection_norm_le line 277
  16. theorem OAI.Erdos3.booleanSelectedDerivative_eq line 286
  17. def OAI.Erdos3.productMinorInverseBound line 299
  18. theorem OAI.Erdos3.productMinorInverseBound_nonneg line 302
  19. theorem OAI.Erdos3.boolean_selected_inverse_bound line 309
  20. theorem OAI.Erdos3.selectedInverseField_contDiffAt_of_local line 338
  21. theorem OAI.Erdos3.local_selectedWeightedField_spec line 350
  22. theorem OAI.Erdos3.imageTranslationBound_of_local_selected_inverse line 371
  23. theorem OAI.Erdos3.selected_inverse_image_comparison_sqrt line 395
  24. theorem OAI.Erdos3.selectedDerivative_sub_norm_le line 441
  25. theorem OAI.Erdos3.selected_inverse_perturbation line 449
  26. theorem OAI.Erdos3.booleanSelectedInjection_single line 469
  27. theorem OAI.Erdos3.booleanSelectedDerivative_entry line 475
  28. theorem OAI.Erdos3.booleanSelectedDerivative_contDiff line 487
  29. def OAI.Erdos3.productMinorDerivativeBound line 496
  30. theorem OAI.Erdos3.productMinorDerivativeBound_nonneg line 499
  31. theorem OAI.Erdos3.boolean_selected_derivative_bound line 505