OAI/NumberTheory/Ostmann/Construction/WordTransferUniformCoefficient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.list_prod_complex_gate line 11
2. theorem OAI.Ostmann.list_prod_getElem_of_length line 20
3. theorem OAI.Ostmann.list_forall_getElem_of_length line 26
4. def OAI.Ostmann.WordFourierParameters.uniform line 37
5. theorem OAI.Ostmann.polynomialLeafProduct_indexed line 46
6. theorem OAI.Ostmann.WordFourierParameters.uniform_coefficient line 65

   Source documentation

   This equality derives the coefficient on natural assignments from its support and Fourier reconstruction.

   theorem WordFourierParameters.uniform_coefficient {σ : Type*} {n : ℕ}
       (template : WordTransferTemplate σ n) (t : FrequencyTree ℤ n)
       (hn : NonzeroInternalFrequencies n t) (profile : 𝓢(ℝ, ℂ))
       (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (x : σ → ℕ) :
       (WordFourierParameters.uniform n profile X lo hi hlo hhi).coefficient
         template t hn (fun i => (x i : ℤ)) =
         if ValidTransferHistory (wordTransferSystem σ) n (template.state x) t then
           polynomialLeafProduct (template.weightedLeaves t hn .prime) profile X lo hi (fun i => (x i : ℤ))
         else 0 := by
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.WordFourierParameters.uniform, OAI.Ostmann.WordFourierParameters.coefficient, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem, OAI.Ostmann.polynomialLeafProduct

7. theorem OAI.Ostmann.WordTransferTemplate.recursive_weight_coefficient line 79

   Source documentation

   Exact identification with the weight used in the original amplitude.

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

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