OAI/NumberTheory/Ostmann/Construction/WordUnitCoefficient.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordRangeDecoration.unitAt line 11
2. theorem OAI.Ostmann.WordRangeDecoration.unitAt_mem line 16
3. def OAI.Ostmann.wordUnitNumerators line 21
4. def OAI.Ostmann.wordUnitDenominators line 24
5. def OAI.Ostmann.wordUnitModuli line 27
6. theorem OAI.Ostmann.WordRangeDecoration.unitAt_all line 29
7. theorem OAI.Ostmann.WordRangeDecoration.unitAt_period line 42
8. theorem OAI.Ostmann.guardedHistoryAmplitude_extra_units line 51
9. def OAI.Ostmann.WordFourierParameters.unitRangedCoefficient line 71
10. theorem OAI.Ostmann.WordFourierParameters.unitRangedCoefficient_local line 79

    Source documentation

    All inherited unit tests are literal divisibility tests on the constructed numerators, with the same polynomial inequalities and smooth factors.

    theorem unitRangedCoefficient_local {σ : Type*} {n : ℕ} (p : WordFourierParameters n)
        (U D : WordRangeDecoration σ n) (template : WordTransferTemplate σ n)
        (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (a : σ → ℤ) (coord : σ) (z : ℤ) :
        p.unitRangedCoefficient U D template t ht (Function.update a coord z) =
          guardedHistoryAmplitude
            (Fin.append (wordGuardNumerators (template.guardAt t ht)) (wordUnitNumerators (U.unitAt template t ht)))
            (Fin.append (wordGuardDenominators (template.guardAt t ht)) (wordUnitDenominators (U.unitAt template t ht)))
            (Fin.append (wordGuardModuli (template.guardAt t ht)) (wordUnitModuli (U.unitAt template t ht)))
            a coord (p.factors template t ht a coord) (p.rangedPolynomials D template t ht a coord)
            (rangedKeep D template t ht) z := by
    …

    Mentions: OAI.Ostmann.WordFourierParameters, OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.guardedHistoryAmplitude, OAI.Ostmann.wordGuardNumerators, OAI.Ostmann.wordUnitNumerators, OAI.Ostmann.wordGuardDenominators, OAI.Ostmann.wordUnitDenominators, OAI.Ostmann.wordGuardModuli, OAI.Ostmann.wordUnitModuli, OAI.Ostmann.WordFourierParameters.rangedKeep

11. theorem OAI.Ostmann.WordFourierParameters.unitRangedCoefficient_nat line 95

    Source documentation

    On valid natural histories these are exactly the recursively inherited unit conditions, including the original leaf-frequency conditions.

    theorem unitRangedCoefficient_nat {σ : Type*} {n : ℕ} (p : WordFourierParameters n)
        (U D : WordRangeDecoration σ n) (template : WordTransferTemplate σ n)
        (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (x : σ → ℕ)
        (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t) :
        p.unitRangedCoefficient U D template t ht (fun i => (x i : ℤ)) =
          (if U.UnitsAt template x t then 1 else 0) *
            p.rangedCoefficient D template t ht (fun i => (x i : ℤ)) := by
    …

    Mentions: OAI.Ostmann.WordFourierParameters, OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem

12. theorem OAI.Ostmann.WordFourierParameters.coefficient_eq_zero_of_not_valid line 107
13. theorem OAI.Ostmann.WordFourierParameters.unitRangedCoefficient_nat_all line 117