OAI/Analysis/FiniteFactor/Polynomial.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteFactor.product_has_low_nonzero_coeff line 8

    Also declared: ComparatorChallenges/ProductBrown.lean:10 (same declaration text).

  2. abbrev OAI.FiniteFactor.Coefficients line 20

    Also declared: ComparatorChallenges/ProductBrown.lean:22 (same declaration text).

  3. def OAI.FiniteFactor.coefficientPolynomial line 22

    Also declared: ComparatorChallenges/ProductBrown.lean:24 (same declaration text).

  4. theorem OAI.FiniteFactor.coefficientPolynomial_coeff line 25

    Also declared: ComparatorChallenges/ProductBrown.lean:27 (same declaration text).

  5. def OAI.FiniteFactor.productCoefficient line 31

    Also declared: ComparatorChallenges/ProductBrown.lean:33 (same declaration text).

  6. theorem OAI.FiniteFactor.productCoefficient_eq line 35

    Also declared: ComparatorChallenges/ProductBrown.lean:37 (same declaration text).

  7. theorem OAI.FiniteFactor.continuous_productCoefficient line 43

    Also declared: ComparatorChallenges/ProductBrown.lean:45 (same declaration text).

  8. def OAI.FiniteFactor.lowCoefficients line 54

    Also declared: ComparatorChallenges/ProductBrown.lean:56 (same declaration text).

  9. theorem OAI.FiniteFactor.continuous_lowCoefficients line 57

    Also declared: ComparatorChallenges/ProductBrown.lean:59 (same declaration text).

  10. theorem OAI.FiniteFactor.lowCoefficients_ne_zero line 60

    Also declared: ComparatorChallenges/ProductBrown.lean:62 (same declaration text).

  11. def OAI.FiniteFactor.admissibleCoefficients line 72

    Also declared: ComparatorChallenges/ProductBrown.lean:74 (same declaration text).

  12. theorem OAI.FiniteFactor.isCompact_admissibleCoefficients line 75

    Also declared: ComparatorChallenges/ProductBrown.lean:77 (same declaration text).

  13. theorem OAI.FiniteFactor.uniform_product_coefficient_bound line 83

    Also declared: ComparatorChallenges/ProductBrown.lean:85 (same declaration text).

  14. def OAI.FiniteFactor.laurentProductCoefficient line 115

    Source documentation

    Coefficient of z^r in the two Laurent polynomials supported on [-K,K]. The finite indices enumerate each Laurent exponent exactly once as i-K.

    noncomputable def laurentProductCoefficient (K : ℕ) (A B : ℤ → ℂ) (r : ℤ) : ℂ :=
…
  15. theorem OAI.FiniteFactor.shifted_productCoefficient line 120
  16. theorem OAI.FiniteFactor.laurent_product_uniform_lower_bound line 134