OAI/Combinatorics/Progressions/Linear/NativeCoefficientKernel.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realifyFunctional_lieTreeEval_rational line 17
  2. theorem OAI.Erdos3.rational_lieTree_kernel_of_real line 23
  3. def OAI.Erdos3.NativeRankInterval.refilteredHorizontalImage line 57
  4. theorem OAI.Erdos3.NativeRankInterval.refilteredHorizontalImage_frequency line 63
  5. theorem OAI.Erdos3.NativeRankInterval.refiltered_sunflower_bracket line 84
  6. theorem OAI.Erdos3.NativeRankInterval.refiltered_sunflower_representatives line 101
  7. def OAI.Erdos3.NativeRankInterval.SunflowerKernel line 120
  8. def OAI.Erdos3.NativeRankInterval.BracketKernel line 130
  9. theorem OAI.Erdos3.NativeRankInterval.sunflowerKernel_of_real line 138
  10. def OAI.Erdos3.NativeRankInterval.refilteredProjectionImage line 166
  11. theorem OAI.Erdos3.NativeRankInterval.refilteredHorizontalImage_eq line 169
  12. theorem OAI.Erdos3.exists_rank_interval_sunflower line 194
  13. theorem OAI.Erdos3.NativeRankInterval.real_rankProjection_frequency line 257
  14. theorem OAI.Erdos3.NativeRankInterval.real_refilteredHorizontalImage_frequency line 273
  15. def OAI.Erdos3.NativeDegreeRankFamily.fourRankBasis line 318
  16. theorem OAI.Erdos3.NativeRankInterval.rankProjection_coordinates line 331
  17. theorem OAI.Erdos3.NativeRankInterval.rankProjection_coordinates_logHeight line 350
  18. theorem OAI.Erdos3.NativeRankInterval.refilteredProjectionImage_mem_candidates line 382
  19. theorem OAI.Erdos3.NativeRankInterval.real_rankProjection_coordinates line 440
  20. theorem OAI.Erdos3.NativeRankInterval.real_rankProjection_abs_bound line 454
  21. theorem OAI.Erdos3.NativeRankInterval.real_rankProjection_grid line 462
  22. structure OAI.Erdos3.NativeRankInterval.SunflowerWitness line 498
  23. def OAI.Erdos3.NativeRankInterval.SunflowerWitness.projection line 531
  24. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projection_mem_candidates line 534
  25. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.horizontalImage_eq line 540
  26. theorem OAI.Erdos3.exists_rank_sunflower_witness line 549
  27. theorem OAI.Erdos3.exists_common_rank_projection_family line 600
  28. def OAI.Erdos3.NativeRankInterval.projectedCoefficient line 665
  29. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.exists_projected_corrections line 675
  30. def OAI.Erdos3.NativeRankInterval.SunflowerWitness.mono line 718
  31. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.mono_projection line 730
  32. def OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedRepresentative line 756
  33. def OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedDenominator line 763
  34. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedDenominator_pos line 767
  35. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedDenominator_bound line 770
  36. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedRepresentative_slow line 780
  37. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedRepresentative_grid line 796
  38. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedRepresentative_mem line 837
  39. def OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedRepresentativeLayer line 849
  40. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedRepresentative_horizontal line 855
  41. def OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedOrbitCoefficient line 871
  42. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedOrbitCoefficient_coe line 879
  43. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedOrbitCoefficient_horizontal line 884
  44. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedSymbol_native_component line 920
  45. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedOrbitCoefficient_native_component line 942
  46. theorem OAI.Erdos3.NativeDegreeRankFamily.logCoefficient_mem_rank_one line 973
  47. theorem OAI.Erdos3.NativeDegreeRankFamily.horizontalCoefficient_real_log line 982
  48. theorem OAI.Erdos3.NativeRankInterval.SunflowerWitness.projectedOrbitCoefficient_native_log_mod_kernel line 1003