OAI/Combinatorics/Progressions/Estimates/MixedRootLosses.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedSwapSample line 12
  2. theorem OAI.Erdos3.mixedSwapSample_input line 15
  3. def OAI.Erdos3.NativeMultidegreeNilcharacter.divisionMixedExchangeCorrection line 25
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.divisionMixedExchangeCorrection_pointwise_error line 35
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.divisionMixedExchangeCorrection_mean_error line 49
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.divisionMixedExchangeCorrection_norm line 88
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_divisionMixedExchangeCorrection_expansion line 115
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_division_mixed_last_slots_equivalence line 161
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_division_mixed_tensor_last_slots_equivalence line 198
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_root_last_slots_equivalence line 235
  11. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedTensorExchangeCorrection line 262
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedTensorExchange_kernel line 268
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedTensorExchangeCorrection_norm line 277
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedTensorExchangeCorrection_mean_error line 287
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedTensorExchangeCorrection_expansion line 314
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.dilationTensorMixedExchangeCorrection_mean_error line 326
  17. def OAI.Erdos3.mixedCornerWeight line 363
  18. def OAI.Erdos3.mixedCornerSample line 365
  19. def OAI.Erdos3.mixedCanonicalSample line 368
  20. def OAI.Erdos3.mixedTailSortPermutation line 371
  21. def OAI.Erdos3.mixedHeadIndex line 374
  22. def OAI.Erdos3.mixedHeadPermutation line 377
  23. def OAI.Erdos3.mixedPreExchangeSample line 380
  24. def OAI.Erdos3.mixedPostExchangePermutation line 383
  25. def OAI.Erdos3.mixedExchangePermutation line 387
  26. theorem OAI.Erdos3.mixedPermuteSample_eq_comp line 393
  27. theorem OAI.Erdos3.mixedCornerSample_input line 398
  28. theorem OAI.Erdos3.mixedCornerSample_zeroCount line 401
  29. theorem OAI.Erdos3.mixedCanonicalSample_eq_sorted line 411
  30. theorem OAI.Erdos3.mixedCanonicalSample_of_first_one line 417
  31. theorem OAI.Erdos3.mixedCorner_exists_tail_one line 422
  32. theorem OAI.Erdos3.mixedHeadIndex_one line 431
  33. theorem OAI.Erdos3.mixedPreExchangeSample_one line 437
  34. theorem OAI.Erdos3.mixedCanonicalSample_of_first_zero line 443
  35. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootExchangeCorrection line 471
  36. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootExchangeCorrection_norm line 475
  37. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootExchangeCorrection_mean_error line 487
  38. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedRootExchangeCorrection_expansion line 506
  39. def OAI.Erdos3.mixedCornerCount line 535
  40. theorem OAI.Erdos3.mixedNonconstantCorner_card_eq line 537
  41. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRawCornerFactor line 546
  42. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRawCornerFactor_norm line 551
  43. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCornerExchangeFactor line 556
  44. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCornerExchangeFactor_norm line 568
  45. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCornerExchangeFactor_mean_error line 595
  46. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCanonicalTensor line 635
  47. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCanonicalTensor_norm line 639
  48. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCanonicalTensor_unit line 644
  49. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedNonconstantTensor_cross_symmetric line 652
  50. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCornerExchangeProduct line 660
  51. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCornerExchangeProduct_norm line 665
  52. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCornerExchangeProduct_mean_error line 679
  53. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_corner_exchange_expansion line 716
  54. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_corner_product_expansion line 777
  55. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPermutedDiagonalCorrection line 819
  56. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPermutedDiagonalCorrection_norm line 827
  57. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPermutedDiagonalCorrection_mean_error line 850
  58. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_permuted_diagonal_expansion line 912
  59. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootCornerCorrection line 980
  60. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootCornerCorrection_norm line 984
  61. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootCornerCorrection_mean_error line 999
  62. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedRootCornerCorrection_expansion line 1027
  63. def OAI.Erdos3.mixedRootTensorExponent line 1074
  64. def OAI.Erdos3.mixedRootCornerExponent line 1076
  65. def OAI.Erdos3.mixedRootCornerCoefficient line 1079
  66. theorem OAI.Erdos3.root_corner_loss_identity line 1082
  67. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedIntegrationRoot_outputDim line 1107
  68. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootCornerCorrection_mean_error_power line 1110