OAI/NumberTheory/Ostmann/Construction/WordTransferCoefficient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.WordFourierParameters line 11
2. def OAI.Ostmann.WordFourierParameters.frequency line 23
3. def OAI.Ostmann.WordFourierParameters.factors line 28
4. def OAI.Ostmann.WordFourierParameters.polynomials line 34
5. def OAI.Ostmann.WordFourierParameters.keep line 39
6. def OAI.Ostmann.WordFourierParameters.budget line 43
7. def OAI.Ostmann.WordFourierParameters.coefficient line 47
8. theorem OAI.Ostmann.WordFourierParameters.coefficient_local line 57

   Source documentation

   No representation hypothesis is needed: these are the exact polynomial and residue gates constructed from the original branching data.

   theorem coefficient_local (p : WordFourierParameters n) (template : WordTransferTemplate σ n)
       (t : FrequencyTree ℤ n) (hn : NonzeroInternalFrequencies n t) (a : σ → ℤ) (coord : σ) (z : ℤ) :
       p.coefficient template t hn (Function.update a coord z) =
         guardedHistoryAmplitude (wordGuardNumerators (template.guardAt t hn))
           (wordGuardDenominators (template.guardAt t hn)) (wordGuardModuli (template.guardAt t hn))
           a coord (p.factors template t hn a coord) (p.polynomials template t hn a coord)
           (keep template t hn) z := by
   …

   Mentions: OAI.Ostmann.WordFourierParameters, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.guardedHistoryAmplitude, OAI.Ostmann.wordGuardNumerators, OAI.Ostmann.wordGuardDenominators, OAI.Ostmann.wordGuardModuli, OAI.Ostmann.WordFourierParameters.keep

9. theorem OAI.Ostmann.WordFourierParameters.factors_budget line 77
10. theorem OAI.Ostmann.WordFourierParameters.budget_nonneg line 81
11. theorem OAI.Ostmann.WordFourierParameters.complexity_bound line 88

    Source documentation

    The complete partition complexity is polynomial in the word size for fixed depth, including every original support inequality.

    theorem complexity_bound (p : WordFourierParameters n) (template : WordTransferTemplate σ n)
        (t : FrequencyTree ℤ n) (hn : NonzeroInternalFrequencies n t) (a : σ → ℤ) (coord : σ)
        (B : ℕ) (hB : 1 ≤ B) (hwords : template.WordsBounded B) :
        polynomialWeightComplexity (p.factors template t hn a coord) (p.polynomials template t hn a coord) ≤
          (3 * 2 ^ n + 3 * (2 ^ n - 1)) * B ^ (n + 1) := by
    …

    Mentions: OAI.Ostmann.WordFourierParameters, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.polynomialWeightComplexity