OAI/NumberTheory/Ostmann/Construction/WordRangeWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordRangeDecoration.weight line 12
2. theorem OAI.Ostmann.WordRangeDecoration.weight_eq line 28
3. def OAI.Ostmann.WordFourierParameters.rangedCoefficient line 53
4. theorem OAI.Ostmann.WordRangeDecoration.weight_coefficient line 61

   Source documentation

   The polynomial range coefficient is the literal recursive weight with all bins at every node, not a replacement support assumption.

   theorem WordRangeDecoration.weight_coefficient {σ : Type*} {n : ℕ}
       (D : WordRangeDecoration σ n) (template : WordTransferTemplate σ n)
       (x : σ → ℕ) (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
       (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y) (X lo hi : ℝ)
       (hlo : 1 ≤ lo) (hhi : lo ≤ hi) :
       D.weight
         (fun τ v => (if (wordTransferLeafValue τ : ℝ) / X ∈ Set.Icc lo hi then (1 : ℂ) else 0) *
           normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v ((wordTransferLeafValue τ : ℝ) / X))
         template x t =
         (WordFourierParameters.uniform n (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).rangedCoefficient
           D template t ht (fun i => (x i : ℤ)) := by
   …

   Mentions: OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.wordTransferLeafValue, OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.WordFourierParameters.uniform