OAI/NumberTheory/Ostmann/Arithmetic/RangedExpandedWordPairBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.rangedWordTransferPairBound line 12
2. theorem OAI.Ostmann.selected_ranged_expanded_word_pair_bound line 25
3. theorem OAI.Ostmann.ranged_expanded_word_pair_original_bound line 68

   Source documentation

   Every remaining coordinate keeps its own original harmonic prior. Only the displayed numerical estimate remains to be specialized.

   theorem ranged_expanded_word_pair_original_bound {V : Type*} [Fintype V]
       (a b : V) (hab : a ≠ b) {n : ℕ}
       (template template' : WordTransferTemplate (ExpandedScheduledVariable V n) n)
       (D D' : WordRangeDecoration (ExpandedScheduledVariable V n) n) (t t' : FrequencyTree ℤ n)
       (hn : NonzeroInternalFrequencies n t) (hn' : NonzeroInternalFrequencies n t')
       (B : ℕ) (hB : 1 ≤ B) (hwords : template.WordsBounded B) (hwords' : template'.WordsBounded B)
       (hD : D.WordsBounded B) (hD' : D'.WordsBounded B)
       (hz : ∀ s ∈ allFrequencyList n t, s ≠ 0) (hz' : ∀ s ∈ allFrequencyList n t', s ≠ 0)
       (f f' : WordFourierParameters n)
       (χ : V → ∀ p : ℕ, DirichletCharacter ℂ p) (graph : V → V → ℤ)
       (unary : V → ℕ → ℂ) (hunary : ∀ i x, ‖unary i x‖ ≤ 1)
       (hself : graph a a = 0 ∧ graph b b = 0) (hreverse : graph b a = 0)
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.allFrequencyList, OAI.Ostmann.WordFourierParameters