OAI/Combinatorics/Progressions/Estimates/MixedFrozenMiddleRows.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.MixedWeightCorner line 12
  2. def OAI.Erdos3.mixedWeightSupportEquiv line 15
  3. theorem OAI.Erdos3.mixedWeightCorner_card line 22
  4. theorem OAI.Erdos3.mixedCornerWeight_zero_iff line 30
  5. theorem OAI.Erdos3.mixedCornerWeight_le line 41
  6. theorem OAI.Erdos3.mixedCornerWeight_pos line 46
  7. def OAI.Erdos3.mixedWeightOneEquiv line 51
  8. def OAI.Erdos3.mixedWeightSample line 54
  9. abbrev OAI.Erdos3.MixedWeightBlock line 65
  10. def OAI.Erdos3.mixedWeightBlockCorner line 67
  11. theorem OAI.Erdos3.mixedWeightBlockCorner_injective line 74
  12. theorem OAI.Erdos3.mixedWeightBlockCorner_surjective line 84
  13. def OAI.Erdos3.mixedWeightBlockEquiv line 93
  14. theorem OAI.Erdos3.mixedWeightBlock_canonical line 97
  15. def OAI.Erdos3.mixedWeightMerge line 103
  16. theorem OAI.Erdos3.mixedWeightMerge_block line 108
  17. theorem OAI.Erdos3.mixedWeightSample_first_input line 124
  18. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWeightTensor line 138
  19. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedFirstTensor line 142
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWeightTensor_norm line 145
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWeightTensor_unit line 151
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedFirstTensor_norm line 159
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedFirstTensor_unit line 164
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWeightTensor_first line 168
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCanonicalTensor_weight_merge line 175
  26. abbrev OAI.Erdos3.MixedHigherCorner line 203
  27. def OAI.Erdos3.mixedGroupedWeightMerge line 205
  28. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedHigherTensor line 215
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedHigherTensor_norm line 219
  30. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedHigherTensor_unit line 224
  31. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCanonicalTensor_grouped_merge line 232
  32. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_original_mixed_first_tensor_equivalence line 253
  33. abbrev OAI.Erdos3.MixedMiddleCorner line 275
  34. def OAI.Erdos3.mixedSplitHigherMerge line 277
  35. theorem OAI.Erdos3.mixedSplitHigherMerge_castSucc line 281
  36. theorem OAI.Erdos3.mixedSplitHigherMerge_last line 286
  37. theorem OAI.Erdos3.mixedWeightSample_last_input line 292
  38. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedMiddleTensor line 306
  39. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedMiddleTensor_norm line 310
  40. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedMiddleTensor_unit line 315
  41. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedHigherTensor_split line 324
  42. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCanonicalTensor_split_merge line 337
  43. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedOriginalWeightCorrection line 358
  44. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedOriginalWeightCorrection_pointwise_error line 368
  45. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedOriginalWeightCorrection_mean_error line 405
  46. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedOriginalWeightCorrection_expansion line 430
  47. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_middle_factor_row_expansion line 507
  48. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedMiddleTensor_row_expansion line 558