WordTransferFourier.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier factors and polynomial budgets of a concrete word history

theorem OAI.Ostmann.HistoryFormula.realValue_ratCast line 14
Source documentation
Rational reconstruction and the real polynomial specialization agree, including away from the integral support.
```
theorem HistoryFormula.realValue_ratCast {σ : Type*} (F : HistoryFormula σ) (x : σ → ℤ) :
    F.realValue x = (F.value (fun i => (x i : ℚ)) : ℝ) := by
…
```
Mentions: OAI.Ostmann.HistoryFormula
def OAI.Ostmann.WeightedWordLeaf.fourierValue line 27
def OAI.Ostmann.evaluatedFourierValue line 32

theorem OAI.Ostmann.WordTransferTemplate.fourier_product line 37

Source documentation

The Fourier product uses the actual terminal word products and every conjugation sign of the original frequency tree.

theorem WordTransferTemplate.fourier_product {σ : Type*} {n : ℕ}
    (template : WordTransferTemplate σ n) (x : σ → ℕ) (t : FrequencyTree ℤ n)
    (hn : NonzeroInternalFrequencies n t)
    (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t)
    (ψ : ℝ → ℂ) (X : ℝ) :
    ((template.weightedLeaves t hn .prime).map
      (WeightedWordLeaf.fourierValue ψ X (fun i => (x i : ℤ)))).prod =
    ((transferLeafList (wordTransferSystem σ) n (template.state x) t).map (fun z =>
      normalizedFourierProfile ψ (if z.2 then (z.1.2 : ℝ) else -(z.1.2 : ℝ))
        ((wordTransferLeafValue z.1.1 : ℝ) / X))).prod := by
…

Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem, OAI.Ostmann.WeightedWordLeaf.fourierValue, OAI.Ostmann.transferLeafList, OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.wordTransferLeafValue

theorem OAI.Ostmann.WordTransferTemplate.recursive_fourier_weight line 60

Source documentation

This identifies the original recursive weight with the constructed polynomial leaves; all real arithmetic and bin cutoffs stay in its exact support.

theorem WordTransferTemplate.recursive_fourier_weight {σ : Type*} {n : ℕ}
    (template : WordTransferTemplate σ n) (x : σ → ℕ) (t : FrequencyTree ℤ n)
    (hn : NonzeroInternalFrequencies n t)
    (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t)
    (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y) (X : ℝ)
    (leafCutoff : WordTransferState σ → ℤ → ℝ)
    (cutoff : WordTransferState σ → ℤ → ℤ → ℤ → ℝ) :
    recursiveTransferWeight (wordTransferSystem σ)
      (fun τ v => (leafCutoff τ v : ℂ) * normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v
        ((wordTransferLeafValue τ : ℝ) / X)) cutoff n (template.state x) t =
      (recursiveSupportFactor (wordTransferSystem σ) leafCutoff cutoff n (template.state x) t : ℂ) *
        ((template.weightedLeaves t hn .prime).map
…

Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem, OAI.Ostmann.WordTransferState, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.wordTransferLeafValue, OAI.Ostmann.recursiveSupportFactor

theorem OAI.Ostmann.WordTransferTemplate.weightedLeaves_cost line 77

Source documentation

The frequency-carrying leaves inherit the derived substitution budget.

theorem WordTransferTemplate.weightedLeaves_cost {σ : Type*} {n : ℕ}
    (template : WordTransferTemplate σ n) (t : FrequencyTree ℤ n)
    (hn : NonzeroInternalFrequencies n t) (B : ℕ) (hB : 1 ≤ B)
    (hwords : template.WordsBounded B) :
    ∀ z ∈ template.weightedLeaves t hn .prime, z.formula.cost ≤ B ^ (n + 1) := by
…

Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies