OAI/Combinatorics/Progressions/Fourier/PivotAnnihilatorFrequencyCode.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_positive_fourier_projection line 18
  2. def OAI.Erdos3.frequencyCodeKernel line 62
  3. theorem OAI.Erdos3.mem_frequencyCodeKernel line 66
  4. theorem OAI.Erdos3.exists_frequency_basis_code line 80
  5. theorem OAI.Erdos3.exists_common_frequency_kernel line 115
  6. theorem OAI.Erdos3.exists_restricted_frequency_basis_real_kernel line 150
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_bounded_positive_fourier_basis line 195
  8. def OAI.Erdos3.frequencyCodeIndices line 264
  9. theorem OAI.Erdos3.mem_frequencyCodeIndices line 267
  10. theorem OAI.Erdos3.finiteFrequencyKernel_codeIndices line 276
  11. theorem OAI.Erdos3.restrictedFrequencySpan_eq_of_kernel_eq line 289
  12. theorem OAI.Erdos3.exists_common_significant_frequency_basis line 305
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_positive_fourier_projection_basis line 377
  14. theorem OAI.Erdos3.NilpotentLieFiltration.pivotAnnihilatorIdeal_codeIndices line 437
  15. theorem OAI.Erdos3.NilpotentLieFiltration.quotientLie_heq_of_ideal_eq line 449
  16. theorem OAI.Erdos3.NilpotentLieFiltration.pivotQuotientFiltration_codeIndices_heq line 456