OAI/Combinatorics/Progressions/Fourier/JoinedFrequencyQuotientInjectivity.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalHeightLE.inv line 14
  2. theorem OAI.Erdos3.exists_bounded_frequency_direction line 28
  3. theorem OAI.Erdos3.rationalLogHeight_nat_inv_mul line 76
  4. def OAI.Erdos3.dividedFrequency line 91
  5. theorem OAI.Erdos3.dividedFrequency_compensate line 93
  6. theorem OAI.Erdos3.dividedFrequency_height line 99
  7. def OAI.Erdos3.frequencyKernelProjection line 116
  8. theorem OAI.Erdos3.frequencyKernelProjection_apply line 119
  9. theorem OAI.Erdos3.frequencyKernelProjection_range line 122
  10. theorem OAI.Erdos3.frequencyKernel_spanning line 134
  11. theorem OAI.Erdos3.frequencyKernel_spanning_height line 140
  12. theorem OAI.Erdos3.realifyFunctional_eq_rid line 168
  13. theorem OAI.Erdos3.mem_realified_frequency_kernel_iff line 176
  14. def OAI.Erdos3.finiteFrequencyKernel line 198
  15. theorem OAI.Erdos3.mem_finiteFrequencyKernel line 203
  16. theorem OAI.Erdos3.finiteFrequencyKernel_le line 213
  17. theorem OAI.Erdos3.mem_real_finiteFrequencyKernel line 216
  18. def OAI.Erdos3.restrictedFrequencySpan line 227
  19. theorem OAI.Erdos3.mem_restrictedFrequencySpan_coannihilator line 231
  20. theorem OAI.Erdos3.mem_restrictedFrequencySpan_iff line 240
  21. theorem OAI.Erdos3.realifyFunctional_comp line 263
  22. theorem OAI.Erdos3.projected_frequency_zero_on_kernel line 270
  23. theorem OAI.Erdos3.projected_real_frequency_zero_on_kernel line 281
  24. theorem OAI.Erdos3.basisGradedSubmodule_iInf line 308
  25. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_grade_fixed line 321
  26. theorem OAI.Erdos3.NilpotentLieFiltration.frequency_zero_on_refiltered_top line 330
  27. theorem OAI.Erdos3.NilpotentLieFiltration.real_frequency_zero_on_refiltered_top line 340
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_positive_frequency_projection_of_decomposition line 367
  29. theorem OAI.Erdos3.finiteFrequencyKernel_eq_map_coannihilator line 441
  30. theorem OAI.Erdos3.finiteFrequencyKernel_eq_of_span_eq line 453
  31. theorem OAI.Erdos3.exists_restricted_frequency_basis line 459
  32. theorem OAI.Erdos3.restrictedFrequencySpan_finRange line 482
  33. def OAI.Erdos3.NilpotentLieFiltration.pivotAnnihilatorIdeal line 504
  34. theorem OAI.Erdos3.NilpotentLieFiltration.mem_pivotAnnihilatorIdeal line 508
  35. def OAI.Erdos3.NilpotentLieFiltration.pivotQuotientMarkedMap line 516
  36. def OAI.Erdos3.NilpotentLieFiltration.pivotQuotientFrequency line 520
  37. theorem OAI.Erdos3.NilpotentLieFiltration.pivotQuotientMarkedMap_mk line 525
  38. theorem OAI.Erdos3.NilpotentLieFiltration.pivotQuotientFrequency_mk line 529
  39. def OAI.Erdos3.NilpotentLieFiltration.pivotProductQuotientMap line 533
  40. def OAI.Erdos3.NilpotentLieFiltration.pivotProductMarkedMap line 537
  41. theorem OAI.Erdos3.NilpotentLieFiltration.pivotProductMarkedMap_quotient line 541
  42. def OAI.Erdos3.NilpotentLieFiltration.joinedFrequencyTop line 547
  43. theorem OAI.Erdos3.NilpotentLieFiltration.mem_joinedFrequencyTop line 552
  44. def OAI.Erdos3.NilpotentLieFiltration.joinedFrequencyQuotientTop line 559
  45. theorem OAI.Erdos3.NilpotentLieFiltration.joinedFrequencyQuotientTop_constraint line 563
  46. theorem OAI.Erdos3.NilpotentLieFiltration.joinedFrequencyQuotientTop_kernel_eq_zero line 570
  47. theorem OAI.Erdos3.NilpotentLieFiltration.joinedFrequencyQuotientTop_injective line 587
  48. theorem OAI.Erdos3.NilpotentLieFiltration.joinedFastTop_kernel_eq_zero line 599