OAI/Combinatorics/Progressions/Fourier/ControlledReplicatedFrequency.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency line 14
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency_apply line 18
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency_permute line 23
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency_basis_full line 35
  5. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency_basis_ne line 42
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedTopCoefficient_blockLayerMap line 58
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency_blockLayerMap_top line 67
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.replicatedFrequency_blockLayerMap_ne line 75
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer_top_frequency line 96
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonTop_frequency line 131
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonTop_frequency line 151
  12. def OAI.Erdos3.replicatedFrequencyHeight line 185
  13. theorem OAI.Erdos3.replicatedFrequencyHeight_pos line 187
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.replicatedFrequency_basis_height line 199
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.replicatedFrequency_finBasis_height line 218
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_replicatedFrequency_denominator line 225
  17. def OAI.Erdos3.replicatedFrequencyDenominatorBudget line 246
  18. theorem OAI.Erdos3.replicatedFrequencyHeight_le_exp line 249
  19. theorem OAI.Erdos3.replicatedFrequencyHeight_ceil_exp line 260
  20. theorem OAI.Erdos3.replicatedFrequencyDenominator_le_exp line 267
  21. def OAI.Erdos3.squarefreeFrequencyInputBudget line 292
  22. def OAI.Erdos3.squarefreeFrequencyModelBudget line 295
  23. theorem OAI.Erdos3.squarefreeInputBudget_le_frequency line 300
  24. theorem OAI.Erdos3.squarefreeFrequencyInputBudget_nonneg line 306
  25. theorem OAI.Erdos3.squarefreeFrequencyInputBudget_le_model line 310
  26. theorem OAI.Erdos3.squarefree_frequency_grid_budget line 315
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeLattice_frequency_integral line 351
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeRealLattice_frequency_integral line 361
  29. theorem OAI.Erdos3.exists_squarefreeFrequency_cost line 380
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_replicated_frequency line 405