OAI/Combinatorics/Progressions/Estimates/QuarticRootExchange.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_unit_complex_inner_le_one line 13
  2. def OAI.Erdos3.complexCrossContraction line 22
  3. theorem OAI.Erdos3.complexCrossContraction_rank_one line 26
  4. theorem OAI.Erdos3.complexCrossContraction_unit line 39
  5. theorem OAI.Erdos3.complexCrossContraction_sum line 50
  6. theorem OAI.Erdos3.norm_complexCrossContraction_positive_mixture line 63
  7. theorem OAI.Erdos3.norm_sub_complexCrossContraction_le_sum line 83
  8. theorem OAI.Erdos3.norm_complexCrossContraction_le_card line 116
  9. theorem OAI.Erdos3.mean_complexCrossContraction_error_le_card line 135
  10. theorem OAI.Erdos3.exists_native_cross_contraction line 167
  11. def OAI.Erdos3.quarticSampledInput line 220
  12. theorem OAI.Erdos3.quarticSampledInput_map line 223
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.division_dilation_integer_representative line 235
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_rational_division_equivalence line 250
  15. def OAI.Erdos3.quarticSwapSample line 349
  16. def OAI.Erdos3.NativeMultidegreeNilcharacter.divisionQuarticExchangeCorrection line 355
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.divisionQuarticExchangeCorrection_pointwise_error line 365
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.divisionQuarticExchangeCorrection_mean_error line 379
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.divisionQuarticExchangeCorrection_norm line 418
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_divisionQuarticExchangeCorrection_expansion line 446
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_sampled_rational_division_equivalence line 491
  22. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticTensorExchangeCorrection line 582
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticTensorExchange_kernel line 588
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticTensorExchangeCorrection_norm line 597
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticTensorExchangeCorrection_mean_error line 607
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticTensorExchangeCorrection_expansion line 634
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.dilationTensorQuarticExchangeCorrection_mean_error line 646
  28. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootExchangeCorrection line 673
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootExchangeCorrection_norm line 677
  30. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootExchangeCorrection_mean_error line 689
  31. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticRootExchangeCorrection_expansion line 711