OAI/Combinatorics/Progressions/Estimates/QuadraticBoundedFamily.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.productMultidegreeLayerBasis line 17
  2. def OAI.Erdos3.RationalFilteredNilmanifold.productMultidegreeLayerFinBasis line 23
  3. def OAI.Erdos3.RationalFilteredNilmanifold.piMultidegree line 30
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.productMultidegreeLayerBasis_logHeight line 35
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.piMultidegree_complexity line 55
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_bounded_multidegree_product_family line 77
  7. def OAI.Erdos3.RationalFilteredNilmanifold.HasBoundedBinaryMultidegreeFamily line 155
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_bounded_binary_multidegree_family line 182
  9. structure OAI.Erdos3.NativeBoundedMultidegreeFamily line 266
  10. def OAI.Erdos3.NativeBoundedMultidegreeFamily.eval line 294
  11. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.eval_multidegree line 296
  12. def OAI.Erdos3.NativeBoundedMultidegreeFamily.mono line 303
  13. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.mono_eval line 308
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_product_with_bounded_family line 317
  15. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.norm_eval line 406
  16. def OAI.Erdos3.NativeBoundedMultidegreeFamily.slice line 412
  17. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.slice_eval line 417
  18. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.slice_orbit_eval line 426
  19. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.slice_norm line 444
  20. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.slice_complexity line 448
  21. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.slice_observable line 452
  22. theorem OAI.Erdos3.NativeUnitRankFamily.withOrbit_eval line 464
  23. def OAI.Erdos3.NativeUnitRankFamily.toVerticalFamily line 487
  24. theorem OAI.Erdos3.NativeUnitRankFamily.toVerticalFamily_eval line 504
  25. def OAI.Erdos3.NativeBoundedMultidegreeFamily.toNilcharacter line 521
  26. theorem OAI.Erdos3.NativeBoundedMultidegreeFamily.toNilcharacter_eval line 537
  27. theorem OAI.Erdos3.exists_native_correlation_of_unit_products line 560
  28. def OAI.Erdos3.QuadraticMarked.parameter line 629
  29. theorem OAI.Erdos3.QuadraticMarked.parameter_mul line 632
  30. theorem OAI.Erdos3.QuadraticMarked.parameter_inv line 636
  31. def OAI.Erdos3.QuadraticMarked.affineElement line 639
  32. theorem OAI.Erdos3.QuadraticMarked.affineElement_phase line 642
  33. def OAI.Erdos3.QuadraticMarked.centeredElement line 647
  34. theorem OAI.Erdos3.QuadraticMarked.centeredElement_phase line 651
  35. theorem OAI.Erdos3.QuadraticMarked.centeredElement_retraction_coord line 657
  36. theorem OAI.Erdos3.QuadraticMarked.localCharacter_centeredElement line 683
  37. def OAI.Erdos3.QuadraticMarked.localOrbit line 712
  38. theorem OAI.Erdos3.QuadraticMarked.localOrbit_eval line 719
  39. def OAI.Erdos3.QuadraticMarked.latticeCorrection line 746
  40. theorem OAI.Erdos3.QuadraticMarked.latticeCorrection_mem line 750
  41. theorem OAI.Erdos3.QuadraticMarked.localOrbit_right_normalization line 758
  42. theorem OAI.Erdos3.QuadraticMarked.localOrbit_quotient line 771
  43. theorem OAI.Erdos3.QuadraticMarked.localOrbit_observable line 787
  44. theorem OAI.Erdos3.exists_quadratic_bounded_family line 820