WordTransferWeightIdentity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Identification of the original recursive weight with its polynomial leaves

theorem OAI.Ostmann.recursiveTransferWeight_flat line 12

theorem OAI.Ostmann.WordTransferTemplate.leaf_product_value line 30

Source documentation

Transport an arbitrary terminal factor through the actual frequency and word-value reconstruction, retaining its conjugation flag.

theorem WordTransferTemplate.leaf_product_value {σ : Type*} {n : ℕ}
    (template : WordTransferTemplate σ n) (x : σ → ℕ) (t : FrequencyTree ℤ n)
    (hn : NonzeroInternalFrequencies n t)
    (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t)
    (F : Bool → ℤ → ℝ → ℂ) :
    ((template.weightedLeaves t hn .prime).map (fun z =>
      F z.positive z.frequency (z.formula.realValue (fun i => (x i : ℤ))))).prod =
    ((transferLeafList (wordTransferSystem σ) n (template.state x) t).map (fun z =>
      F z.2 z.1.2 (wordTransferLeafValue z.1.1))).prod := by
…

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

def OAI.Ostmann.polynomialLeafProduct line 46

theorem OAI.Ostmann.WordTransferTemplate.recursive_weight_polynomial_leaves line 55

Source documentation

The original weight with its terminal bins equals the constructed polynomial coefficient on precisely its original arithmetic support.

theorem WordTransferTemplate.recursive_weight_polynomial_leaves {σ : Type*} {n : ℕ}
    (template : WordTransferTemplate σ n) (x : σ → ℕ) (t : FrequencyTree ℤ n)
    (hn : NonzeroInternalFrequencies n t)
    (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y) (X 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 =
      if ValidTransferHistory (wordTransferSystem σ) n (template.state x) t then
        polynomialLeafProduct (template.weightedLeaves t hn .prime) (𝓕 ψ : 𝓢(ℝ, ℂ))
          X lo hi (fun i => (x i : ℤ)) else 0 := 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.ValidTransferHistory, OAI.Ostmann.polynomialLeafProduct