OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkLogWeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingBulkListLogWeight line 12
2. def OAI.Ostmann.movingBulkLeafLogWeight line 17
3. def OAI.Ostmann.movingBulkTreeLogWeight line 23
4. theorem OAI.Ostmann.movingBulkListLogWeight_bounds line 31
5. theorem OAI.Ostmann.movingBulkTreeLogWeight_bounds line 39
6. theorem OAI.Ostmann.movingDataWeight_bulk_log line 52

   Source documentation

   Real logarithmic weights survive all right-branch conjugations and factor out as their literal product over the terminal bulk groups.

   theorem movingDataWeight_bulk_log {σ : Type*} (value : σ → ℕ) (tier : σ → ℕ)
       (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       {n : ℕ} (T : MovingSlotData σ n) :
       movingDataWeight (fun T s => (movingBulkLeafLogWeight value tier k outside cb cd T : ℂ) * F T s) E T =
         (movingBulkTreeLogWeight value tier k outside cb cd T : ℂ) * movingDataWeight F E T := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingDataWeight, OAI.Ostmann.movingBulkLeafLogWeight, OAI.Ostmann.movingBulkTreeLogWeight

7. theorem OAI.Ostmann.movingBulkTreeLogWeight_sample line 68

   Source documentation

   The selected tier is exactly the original bulk. Restored compensation slots have smaller tiers and cannot enter either logarithmic cutoff.

   theorem movingBulkTreeLogWeight_sample {σ : Type*} (value : σ → ℕ) (tier : σ → ℕ)
       (k : ℕ) (outside : List ℕ) (cb cd : ℝ) (n : ℕ)
       (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
       (a : MovingSampleSlots σ n) (hn : n ≤ k)
       (hsmall : ∀ i ∈ flattenMovingSlots n small, tier i ≠ k)
       (hbulk : ∀ i ∈ flattenMovingSlots n bulk, tier i = k)
       (ha : a.Levels tier) :
       movingBulkTreeLogWeight value tier k outside cb cd (buildMovingSlotData n t small bulk a) =
         treeLeafProduct n (treeLeafMap (movingBulkListLogWeight value outside cb cd) n bulk) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingBulkTreeLogWeight, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingBulkListLogWeight