OAI/Combinatorics/Progressions/Estimates/NativeWeightPairRemoval.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeIntegerExpansion.select_sample_product_correlation line 20
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_frozen_translation_expansion line 58
  3. def OAI.Erdos3.untranslatedMixedProduct line 105
  4. def OAI.Erdos3.mixedParallelogramProduct line 113
  5. theorem OAI.Erdos3.untranslatedMixedProduct_eq line 118
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_replaced_mixed_translation_expansion line 137
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_parallelogram_equivalence line 176
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_parallelogram_expansion line 198
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_remainder_expansion_of_evaluation_coordinates line 227
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_remainder_expansion line 266
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_untranslated_mixed_reduction line 292
  12. def OAI.Erdos3.MixedTranslationReductionStatement line 333
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixed_translation_reduction_transfer line 369
  14. abbrev OAI.Erdos3.MixedExpansionIndex line 420
  15. structure OAI.Erdos3.NativeMixedReductionData line 424
  16. def OAI.Erdos3.NativeMixedReductionData.translationTerm line 449
  17. def OAI.Erdos3.NativeMixedReductionData.lowerTerm line 453
  18. def OAI.Erdos3.NativeMixedReductionData.correction line 457
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_translation_reduction line 472
  20. def OAI.Erdos3.translatedMixedProduct line 509
  21. structure OAI.Erdos3.NativeMixedReductionData.TranslationCode line 528
  22. def OAI.Erdos3.NativeMixedReductionData.translationCoordinates line 534
  23. structure OAI.Erdos3.NativeMixedReductionData.LowerCode line 539
  24. def OAI.Erdos3.NativeMixedReductionData.translationGlobal line 543
  25. def OAI.Erdos3.NativeMixedReductionData.translationLower line 548
  26. theorem OAI.Erdos3.NativeMixedReductionData.translationGlobal_sample line 552
  27. structure OAI.Erdos3.NativeMixedReductionData.ReductionCode line 561
  28. def OAI.Erdos3.NativeMixedReductionData.globalError line 565
  29. theorem OAI.Erdos3.star_finite_expect line 583
  30. theorem OAI.Erdos3.NativeMixedReductionData.translation_negative line 593
  31. theorem OAI.Erdos3.NativeMixedReductionData.translation_positive line 602
  32. theorem OAI.Erdos3.NativeMixedReductionData.correction_factorization line 629
  33. def OAI.Erdos3.NativeMixedReductionData.translationTermExpansion line 666
  34. def OAI.Erdos3.NativeMixedReductionData.secondInput line 672
  35. def OAI.Erdos3.NativeMixedReductionData.fourthInput line 677
  36. def OAI.Erdos3.NativeMixedReductionData.parallelogramInput line 688
  37. def OAI.Erdos3.NativeMixedReductionData.translationGlobalExpansion line 693
  38. def OAI.Erdos3.NativeMixedReductionData.lowerTermExpansion line 701
  39. def OAI.Erdos3.NativeMixedReductionData.translationLowerExpansion line 708
  40. def OAI.Erdos3.NativeMixedReductionData.parallelogramTermExpansion line 715
  41. def OAI.Erdos3.mixedErrorPairBudget line 733
  42. def OAI.Erdos3.mixedErrorBudget line 735
  43. theorem OAI.Erdos3.le_mixedErrorPairBudget line 738
  44. def OAI.Erdos3.NativeMixedReductionData.globalErrorExpansion line 749
  45. theorem OAI.Erdos3.exists_mixed_error_budget line 759
  46. def OAI.Erdos3.NativeIntegerExpansion.translate line 784
  47. def OAI.Erdos3.NativeIntegerExpansion.fourPoint line 789
  48. theorem OAI.Erdos3.native_weight_pair_removal line 810