OAI/NumberTheory/Ostmann/Arithmetic/RecursiveLeafExpansion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.transferLeafList line 13

   Source documentation

   The flag records the conjugations accumulated from right branches.

   noncomputable def transferLeafList {State : Type*} (sys : TransferHistorySystem State) :
       (n : ℕ) → State → FrequencyTree ℤ n → List ((State × ℤ) × Bool)
     | 0, σ, v => [((σ, v), true)]
     | n + 1, σ, t =>
         let P := historyPivot sys σ t.1 (frequencyRoot n t.2.1) (frequencyRoot n t.2.2)
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.historyPivot, OAI.Ostmann.frequencyRoot

2. theorem OAI.Ostmann.transferLeafList_length line 21
3. def OAI.Ostmann.signedLeafValue line 31
4. theorem OAI.Ostmann.signedLeafValue_flip line 35
5. theorem OAI.Ostmann.signedLeafProduct_flip line 41
6. def OAI.Ostmann.recursiveSupportFactor line 52

   Source documentation

   Leaf bins and all intermediate arithmetic/range gates are real. They remain real under every conjugation in the frequency tree.

   noncomputable def recursiveSupportFactor {State : Type*} (sys : TransferHistorySystem State)
       (leafCutoff : State → ℤ → ℝ) (cutoff : State → ℤ → ℤ → ℤ → ℝ) :
       (n : ℕ) → State → FrequencyTree ℤ n → ℝ
     | 0, σ, v => leafCutoff σ v
     | n + 1, σ, t =>
         let v := frequencyRoot n t.2.1
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.frequencyRoot

7. theorem OAI.Ostmann.recursiveTransferWeight_leaf_expansion line 67

   Source documentation

   This equality uses the original recursive weight, including its actual reconstructed pivots and its validity tests.

   theorem recursiveTransferWeight_leaf_expansion {State : Type*}
       (sys : TransferHistorySystem State) (F : State → ℤ → ℂ)
       (leafCutoff : State → ℤ → ℝ) (cutoff : State → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
       recursiveTransferWeight sys (fun σ v => (leafCutoff σ v : ℂ) * F σ v) cutoff n σ t =
         (recursiveSupportFactor sys leafCutoff cutoff n σ t : ℂ) *
           ((transferLeafList sys n σ t).map (signedLeafValue F)).prod := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.recursiveSupportFactor, OAI.Ostmann.transferLeafList, OAI.Ostmann.signedLeafValue

8. theorem OAI.Ostmann.recursiveFourierWeight_leaf_expansion line 91

   Source documentation

   Every leaf conjugation is absorbed into its frequency; the Fourier profile remains the same fixed Schwartz function throughout the tree.

   theorem recursiveFourierWeight_leaf_expansion {State : Type*}
       (sys : TransferHistorySystem State) (ψ : 𝓢(ℝ, ℂ))
       (hreal : ∀ x, conj (ψ x) = ψ x) (scale : State → ℝ)
       (leafCutoff : State → ℤ → ℝ) (cutoff : State → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
       recursiveTransferWeight sys
         (fun σ v => (leafCutoff σ v : ℂ) * normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v (scale σ))
         cutoff n σ t =
         (recursiveSupportFactor sys leafCutoff cutoff n σ t : ℂ) *
           ((transferLeafList sys n σ t).map (fun z =>
             normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ))
               (if z.2 then (z.1.2 : ℝ) else -(z.1.2 : ℝ)) (scale z.1.1))).prod := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.recursiveSupportFactor, OAI.Ostmann.transferLeafList