OAI/Combinatorics/Progressions/Estimates/DependentPatchValue.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.TriangularSlots line 14
  2. def OAI.Erdos3.TriangularSlots.residual line 22
  3. theorem OAI.Erdos3.TriangularSlots.integer_unique line 25
  4. structure OAI.Erdos3.PatchKernel line 51
  5. theorem OAI.Erdos3.TriangularSlots.contributing_unique line 63
  6. def OAI.Erdos3.TriangularSlots.patchValue line 67
  7. theorem OAI.Erdos3.TriangularSlots.patchValue_eq_of_nonzero line 69
  8. theorem OAI.Erdos3.TriangularSlots.patchValue_eq_zero line 76
  9. theorem OAI.Erdos3.TriangularSlots.patchValue_eq_at_residual line 80
  10. theorem OAI.Erdos3.TriangularSlots.patchValue_dist_le line 88
  11. theorem OAI.Erdos3.TriangularSlots.patchValue_mem_Icc line 107
  12. theorem OAI.Erdos3.TriangularSlots.patchValue_dist_of_residuals_close line 128
  13. def OAI.Erdos3.slotPrefix line 182
  14. def OAI.Erdos3.slotSuffix line 185
  15. theorem OAI.Erdos3.slotPrefix_append line 188
  16. theorem OAI.Erdos3.slotSuffix_append line 191
  17. theorem OAI.Erdos3.append_slotPrefix_slotSuffix line 194
  18. def OAI.Erdos3.TriangularSlots.append line 201
  19. theorem OAI.Erdos3.TriangularSlots.append_residual line 221
  20. theorem OAI.Erdos3.dist_append_same_left_le line 235
  21. theorem OAI.Erdos3.dist_append_same_right_le line 243
  22. def OAI.Erdos3.PatchKernel.freeze line 253
  23. theorem OAI.Erdos3.PatchKernel.freeze_value_dist_le line 263
  24. theorem OAI.Erdos3.rationalLiftCharacterTwistLip_le_exp line 281
  25. theorem OAI.Erdos3.rationalLiftCharacterTwistLip_le_exp_of_dim line 294
  26. theorem OAI.Erdos3.rationalLift_major_product_eq line 301
  27. theorem OAI.Erdos3.rationalLift_major_mean_eq line 319
  28. theorem OAI.Erdos3.rationalLift_major_correlation_data line 341
  29. theorem OAI.Erdos3.stable_sort_symm_lt line 376
  30. structure OAI.Erdos3.SlotInterleaving line 389
  31. def OAI.Erdos3.SlotInterleaving.left line 398
  32. def OAI.Erdos3.SlotInterleaving.right line 401
  33. def OAI.Erdos3.SlotInterleaving.fill line 404
  34. theorem OAI.Erdos3.SlotInterleaving.fill_left line 407
  35. theorem OAI.Erdos3.SlotInterleaving.fill_right line 411
  36. theorem OAI.Erdos3.SlotInterleaving.cases line 415
  37. theorem OAI.Erdos3.SlotInterleaving.fill_restrict line 420
  38. def OAI.Erdos3.SlotInterleaving.sorted line 426
  39. theorem OAI.Erdos3.SlotInterleaving.sorted_weight_mono line 435
  40. theorem OAI.Erdos3.dist_restrict_coordinates_le line 441
  41. theorem OAI.Erdos3.TriangularSlots.patchValue_freeze_dist_le line 459
  42. theorem OAI.Erdos3.TriangularSlots.contributing_prefix_eq line 465
  43. theorem OAI.Erdos3.TriangularSlots.patchValue_append_eq line 478
  44. theorem OAI.Erdos3.TriangularSlots.patchValue_freeze_prefix line 504
  45. theorem OAI.Erdos3.TriangularSlots.ext line 534
  46. def OAI.Erdos3.TriangularSlots.takePrefix line 542
  47. def OAI.Erdos3.TriangularSlots.dropPrefix line 553
  48. theorem OAI.Erdos3.TriangularSlots.append_take_drop line 564
  49. theorem OAI.Erdos3.TriangularSlots.takePrefix_residual line 578
  50. def OAI.Erdos3.TriangularSlots.interleave line 597
  51. theorem OAI.Erdos3.TriangularSlots.interleave_residual_left line 613
  52. theorem OAI.Erdos3.TriangularSlots.interleave_residual_right line 618
  53. def OAI.Erdos3.PatchKernel.product line 627
  54. theorem OAI.Erdos3.PatchKernel.product_lip line 661
  55. theorem OAI.Erdos3.PatchKernel.product_value_fill line 664
  56. theorem OAI.Erdos3.TriangularSlots.interleave_kernel_residual line 673
  57. theorem OAI.Erdos3.TriangularSlots.interleave_patchValue line 681
  58. theorem OAI.Erdos3.TriangularSlots.factorized_patchValue_at_lift line 717
  59. theorem OAI.Erdos3.TriangularSlots.factorized_patchValue line 754