OAI/NumberTheory/Ostmann/Arithmetic/RecursiveFrequencySupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frequencyTreeMap line 12
2. theorem OAI.Ostmann.frequencyRoot_map line 16
3. theorem OAI.Ostmann.frequencyLeafWeight_map line 20
4. theorem OAI.Ostmann.recursiveTransferWeight_children_nonzero line 27
5. theorem OAI.Ostmann.recursiveTransferWeight_leaf_cutoff line 48
6. theorem OAI.Ostmann.recursiveTransferWeight_square_with_leaf_cutoff line 63

   Source documentation

   The square bound retains the actual leaf-frequency indicator. No extra leaf frequencies are introduced when support restrictions are dropped.

   theorem recursiveTransferWeight_square_with_leaf_cutoff {State : Type*}
       (sys : TransferHistorySystem State) (leaf : State → ℤ → ℂ)
       (cutoff : State → ℤ → ℤ → ℤ → ℝ) (B : ℝ) (hB : 0 ≤ B)
       (hsize : ∀ σ v, ‖leaf σ v‖ ^ 2 ≤ B)
       (hcut : ∀ σ s v w, |cutoff σ s v w| ≤ 1)
       (V : ℕ) (hleaf : ∀ σ v, leaf σ v ≠ 0 → v.natAbs ≤ V)
       (S : Finset ℤ) (n : ℕ) (σ : State) (t : FrequencyTree S n) :
       ‖recursiveTransferWeight sys leaf cutoff n σ (frequencyTreeMap Subtype.val n t)‖ ^ 2 ≤
         B ^ (2 ^ n) * frequencyLeafWeight (singleFrequencyLeaf S V) n t := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.frequencyTreeMap, OAI.Ostmann.frequencyLeafWeight, OAI.Ostmann.singleFrequencyLeaf