OAI/Combinatorics/Progressions/Lattices/CommonAffineOrbitEvaluation.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.monomialLinearMap line 16
  2. theorem OAI.Erdos3.VectorPolynomial.realMonomial_eval line 23
  3. def OAI.Erdos3.VectorPolynomial.realAffinePolynomial line 32
  4. theorem OAI.Erdos3.VectorPolynomial.realAffinePolynomial_eval line 37
  5. theorem OAI.Erdos3.realMonomial_mem_markedPolynomialLayer line 47
  6. theorem OAI.Erdos3.realAffinePolynomial_mem_marked line 61
  7. def OAI.Erdos3.correlationExponent line 86
  8. theorem OAI.Erdos3.correlationExponent_apply line 89
  9. theorem OAI.Erdos3.eval_correlation_monomial line 97
  10. def OAI.Erdos3.affineMixedLog line 104
  11. theorem OAI.Erdos3.affineMixedLog_eval line 109
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.affineMixedLog_adapted line 128
  13. def OAI.Erdos3.MultidegreeLieFiltration.affineMixedOrbit line 137
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.affineMixedOrbit_eval line 140
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.affineMixedOrbit_at_zero line 145
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.affineMixedOrbit_normalized line 153
  17. theorem OAI.Erdos3.markedShiftLayerPolynomialMap_mem line 178
  18. theorem OAI.Erdos3.markedShiftLayerPolynomialMap_quotient_mem line 185
  19. def OAI.Erdos3.markedAffineShiftCoefficient line 193
  20. def OAI.Erdos3.markedDirectionalShiftCoefficient line 200
  21. theorem OAI.Erdos3.markedAffineShiftCoefficient_quotient_mem line 208
  22. theorem OAI.Erdos3.markedDirectionalShiftCoefficient_quotient_mem line 216
  23. theorem OAI.Erdos3.markedAffineShiftCoefficient_eval line 224
  24. theorem OAI.Erdos3.markedDirectionalShiftCoefficient_eval line 230
  25. theorem OAI.Erdos3.markedAffineShiftCoefficient_shift_eval line 237
  26. def OAI.Erdos3.markedAffineBaseCoefficient line 266
  27. def OAI.Erdos3.markedAffineSlopeCoefficient line 269
  28. def OAI.Erdos3.markedAffineMixedLift line 272
  29. theorem OAI.Erdos3.markedAffineMixedLift_eval line 276
  30. def OAI.Erdos3.markedAffineMixedOrbit line 286
  31. theorem OAI.Erdos3.markedAffineMixedOrbit_eval line 298
  32. theorem OAI.Erdos3.markedAffineMixedOrbit_at_zero line 312
  33. theorem OAI.Erdos3.markedAffineMixedOrbit_normalized line 317
  34. def OAI.Erdos3.realMarkedPolynomialLift line 337
  35. theorem OAI.Erdos3.realMarkedPolynomialLift_mem line 343
  36. theorem OAI.Erdos3.realMarkedPolynomialLift_eval line 358
  37. def OAI.Erdos3.realMarkedQuotientCoefficient line 373
  38. theorem OAI.Erdos3.realMarkedPolynomialLift_quotient_mem line 379
  39. def OAI.Erdos3.realMarkedAffineMixedOrbit line 392
  40. theorem OAI.Erdos3.realMarkedAffineMixedOrbit_eval line 400
  41. theorem OAI.Erdos3.realMarkedAffineMixedOrbit_at_zero line 408
  42. theorem OAI.Erdos3.realMarkedAffineMixedOrbit_normalized line 413
  43. def OAI.Erdos3.NativeRankRelation.CommonData.realAffineMarkedBase line 442
  44. def OAI.Erdos3.NativeRankRelation.CommonData.realAffineMarkedSlope line 449
  45. theorem OAI.Erdos3.NativeRankRelation.CommonData.realAffineMarkedBase_eval line 460
  46. theorem OAI.Erdos3.NativeRankRelation.CommonData.realAffineMarkedSlope_eval line 472
  47. def OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedOrbit line 485
  48. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedOrbit_at_zero line 490
  49. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedOrbit_normalized line 495
  50. def OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedLift line 523
  51. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedOrbit_eval line 534
  52. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonAffineMarkedLift_eval line 547