ExpandedWordPairBound.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The constructed prime-word coefficient under the original product law

def OAI.Ostmann.expandedPrimeValues line 14
Source documentation
Unused internal coordinates start at one; each is overwritten before use.
```
def expandedPrimeValues {V : Type*} (n : ℕ) (x : V → ℤ) : ExpandedScheduledVariable V n → ℤ
  | .inl v => x v
  | .inr _ => 1
```
Mentions: OAI.Ostmann.ExpandedScheduledVariable
theorem OAI.Ostmann.expandedPrimeValues_update line 18
def OAI.Ostmann.wordCoordinateUpdate line 28
theorem OAI.Ostmann.expandedPrimeValues_twoCoordinate line 31
theorem OAI.Ostmann.finiteEdgeWeight_twoCoordinate_reindex line 43
def OAI.Ostmann.wordTransferPairBound line 61
theorem OAI.Ostmann.selected_expanded_word_pair_bound line 73

theorem OAI.Ostmann.expanded_word_pair_original_bound line 115

Source documentation

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

theorem expanded_word_pair_original_bound {V : Type*} [Fintype V]
    (a b : V) (hab : a ≠ b) {n : ℕ}
    (template template' : WordTransferTemplate (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)
    (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)
    (P : Finset ℕ) (Q : V → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
…

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