OAI/NumberTheory/Ostmann/Arithmetic/UnitRangedOriginalPair.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.selected_unit_ranged_expanded_word_pair_bound line 12
2. theorem OAI.Ostmann.unit_ranged_expanded_word_pair_original_bound line 56

   Source documentation

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

   theorem unit_ranged_expanded_word_pair_original_bound {V : Type*} [Fintype V]
       (a b : V) (hab : a ≠ b) {n : ℕ}
       (template template' : WordTransferTemplate (ExpandedScheduledVariable V n) n)
       (U U' 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)
       (hU : U.WordsBounded B) (hU' : U'.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)
   …

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