OAI/NumberTheory/Ostmann/Construction/FixedPivotUnitPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.fixed_pivot_unit_ranged_original_pair_bound line 12

   Source documentation

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

   theorem fixed_pivot_unit_ranged_original_pair_bound {V : Type*} [Fintype V]
       (a b : V) (hab : a ≠ b) {n : ℕ}
       (template template' : WordTransferTemplate (ExpandedScheduledVariable (Option V) n) n)
       (U U' D D' : WordRangeDecoration (ExpandedScheduledVariable (Option 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)
       (χ : Option V → ∀ p : ℕ, DirichletCharacter ℂ p) (graph : Option V → Option V → ℤ)
       (unary : Option 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