OAI/Combinatorics/Progressions/Polynomial/LocalPhaseMarkedObservable.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedOrbit line 28
  2. def OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedSmallElement line 38
  3. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedOrbit_eval line 45
  4. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineCorrectingElement_eq_parameter line 77
  5. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedOrbit_right_normalization line 94
  6. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedOrbit_quotient line 132
  7. theorem OAI.Erdos3.realMarkedParameterDirection_coordinate line 164
  8. theorem OAI.Erdos3.realMarkedParameterDirection_coordinate_le line 172
  9. theorem OAI.Erdos3.realMarkedParameterDirection_coordinateL2Norm_le line 188
  10. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedSmallElement_coordinateL2Norm_le line 213
  11. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedSmallElement_dist_le line 254
  12. theorem OAI.Erdos3.NativeRankRelation.CommonData.realAffineMarkedSlope_zero line 294
  13. theorem OAI.Erdos3.NativeRankRelation.CommonData.realAffineMarkedBase_shift_eval line 300
  14. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedLift_shift_eval line 314
  15. def OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedLift line 338
  16. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedLift_eval line 347
  17. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedSmallElement_inv line 368
  18. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedLift_conjugation line 384
  19. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedOrbit_lift_factorization line 402
  20. theorem OAI.Erdos3.markedQuotientPhase_real_map line 439
  21. theorem OAI.Erdos3.realMarkedShiftTranslate_phase line 447
  22. theorem OAI.Erdos3.realMarkedAffineShift_phase line 456
  23. theorem OAI.Erdos3.realMarkedPolynomialLift_phase line 465
  24. def OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluation line 494
  25. def OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluationLie line 500
  26. theorem OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluation_map line 506
  27. theorem OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluation_real_map line 515
  28. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedLift_base_projection line 527
  29. theorem OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluation_top_mem line 542
  30. theorem OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluation_top_frequency line 554
  31. theorem OAI.Erdos3.NativeRankRelation.CommonData.markedDependentEvaluation_real_top_frequency line 569
  32. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedLift_phase line 587
  33. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedLift_pure line 607
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_bounded_left_translated_unit line 639
  35. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedSmallElement_coordinate_le line 704
  36. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedObservable_factorization line 714