OAI/Combinatorics/Progressions/Estimates/AveragedModeledPatchTransfer.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PatchKernel.weightBounded line 20
  2. theorem OAI.Erdos3.PatchKernel.weightBounded_lip line 33
  3. theorem OAI.Erdos3.PatchKernel.weightBounded_value line 38
  4. theorem OAI.Erdos3.PatchKernel.weightBounded_tsum line 45
  5. theorem OAI.Erdos3.recoveredIntegerLift_eq_add_sum line 64
  6. theorem OAI.Erdos3.recoveredIntegerLift_projection line 70
  7. theorem OAI.Erdos3.recoveredIntegerLift_residue line 77
  8. theorem OAI.Erdos3.recoveredIntegerLift_discrete_data line 85
  9. abbrev OAI.Erdos3.PolynomialPatch.withRecoveredWeight line 105
  10. def OAI.Erdos3.PolynomialPatch.recoveredPatch line 110
  11. theorem OAI.Erdos3.PolynomialPatch.recoveredPatch_lip line 119
  12. theorem OAI.Erdos3.PolynomialPatch.insertAffineLifts_value line 126
  13. theorem OAI.Erdos3.PolynomialPatch.recoveredPatch_value_at_lift line 140
  14. theorem OAI.Erdos3.PolynomialPatch.recoveredPatch_value line 160
  15. theorem OAI.Erdos3.PolynomialPatch.recoveredPatch_value_eq_family line 206
  16. theorem OAI.Erdos3.exists_fiberwise_recovered_patch line 233
  17. theorem OAI.Erdos3.PolynomialPatch.recoveredPatch_value_eq_buffered line 315
  18. theorem OAI.Erdos3.exists_buffered_recovered_patch line 334
  19. theorem OAI.Erdos3.exists_fiberwise_weighted_patch line 363
  20. theorem OAI.Erdos3.exists_discrete_weighted_recovered_patch line 401
  21. theorem OAI.Erdos3.exists_weighted_recovered_patch line 439
  22. theorem OAI.Erdos3.exists_discounted_recovered_patch line 484
  23. theorem OAI.Erdos3.exists_modeled_discounted_patch line 532
  24. def OAI.Erdos3.PolynomialPatch.recursiveRecoveredPatch line 588
  25. theorem OAI.Erdos3.PolynomialPatch.recursiveRecoveredPatch_value line 600
  26. theorem OAI.Erdos3.PolynomialPatch.recursiveRecoveredPatch_lip line 612
  27. theorem OAI.Erdos3.exists_recursive_discounted_recovered_patch line 630
  28. theorem OAI.Erdos3.finite_model_test_difference_weighted line 680
  29. theorem OAI.Erdos3.exists_productive_averaged_model_transfer line 695
  30. theorem OAI.Erdos3.exists_averaged_buffered_score line 717
  31. theorem OAI.Erdos3.exists_averaged_modeled_discounted_patch line 751