OAI/Combinatorics/Progressions/Polynomial/BufferedSampledCurrentGradePhase.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sampledTopPhase_remainder line 12
  2. theorem OAI.Erdos3.sampledTopPhase_homogeneousComponent line 29
  3. theorem OAI.Erdos3.sampledTopPhase_remainder_totalDegree line 41
  4. theorem OAI.Erdos3.sampledTopPhase_coordinate_homogeneous line 50
  5. theorem OAI.Erdos3.sampledCurrentGrade_sampledCurrentGrade_realifyFunctional_basis_coord line 56
  6. theorem OAI.Erdos3.NilpotentLieFiltration.quotientFunctional_kills_fast line 74
  7. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_component_quotient line 82
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_homogeneousPullback line 96
  9. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_component_homogeneousPullback line 110
  10. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_homogeneousComponent_homogeneousPullback line 131
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_functional_homogeneous line 145
  12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_sampledCurrentGrade_lower_phase line 157
  13. theorem OAI.Erdos3.NilpotentLieFiltration.sampledCurrentGrade_phase_lowTagged_eval line 184
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientPolynomial_lowTagged_aeval line 217
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_sampledCurrentGrade_lowTagged_lower_phase line 238
  16. def OAI.Erdos3.majorPhasePlateauKernel line 275
  17. theorem OAI.Erdos3.majorPhasePlateauKernel_lip line 294
  18. theorem OAI.Erdos3.majorPhasePlateauKernel_one line 297
  19. def OAI.Erdos3.VectorPolynomial.majorPhaseNearestLift line 311
  20. theorem OAI.Erdos3.VectorPolynomial.majorPhaseNearestLift_close line 316
  21. def OAI.Erdos3.VectorPolynomial.majorPhasePlateauSignal line 325
  22. theorem OAI.Erdos3.VectorPolynomial.majorPhasePlateauSignal_norm_le_one line 330
  23. theorem OAI.Erdos3.VectorPolynomial.majorPhaseNearestLift_eq_of_close line 339
  24. theorem OAI.Erdos3.VectorPolynomial.majorPhasePlateauSignal_eq_phase line 352
  25. def OAI.Erdos3.VectorPolynomial.integerSampledRealChart line 375
  26. theorem OAI.Erdos3.VectorPolynomial.integerSampledRealChart_eval line 379
  27. def OAI.Erdos3.VectorPolynomial.integerSampledSpatial line 385
  28. def OAI.Erdos3.VectorPolynomial.integerSampledLowTags line 389
  29. theorem OAI.Erdos3.VectorPolynomial.majorPhasePlateauSignal_integerChart_eq line 395
  30. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bufferedSampledCurrentGrade_phase line 431