OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkLogTrees.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkLogLeafLists line 10
2. theorem OAI.Ostmann.bulkLogLeafLists_length line 15
3. theorem OAI.Ostmann.bulkLogLeafLists_length_le line 23
4. theorem OAI.Ostmann.movingBulkTreeLogWeight_eq_lists line 38
5. theorem OAI.Ostmann.movingBulkTreeLogWeight_eq_cutoff_product line 51

   Source documentation

   Every terminal logarithmic factor is retained. The constant spectator weight factors out once per actual leaf.

   theorem movingBulkTreeLogWeight_eq_cutoff_product {σ : Type*} (value tier : σ → ℕ)
       (hvalue : ∀ a, 0 < value a) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       {n : ℕ} (T : MovingSlotData σ n) :
       movingBulkTreeLogWeight value tier k outside cb cd T =
         logCellProfile ((outside.map (fun p => Real.log (p : ℝ))).sum - cd) ^ (2 ^ n) *
           ∏ j : Fin (bulkLogLeafLists tier k T).length,
             bulkLogCutoffWeight (fun a => (value a : ℝ)) cb ((bulkLogLeafLists tier k T)[j]) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingBulkTreeLogWeight, OAI.Ostmann.logCellProfile, OAI.Ostmann.bulkLogLeafLists, OAI.Ostmann.bulkLogCutoffWeight

6. theorem OAI.Ostmann.movingBulkPairLogWeight_eq_cutoff_product line 78

   Source documentation

   Both branches use their own actual terminal groups. The real logarithmic weights commute with conjugation, but remain inside the common prime average.

   theorem movingBulkPairLogWeight_eq_cutoff_product {σ : Type*} (value tier : σ → ℕ)
       (hvalue : ∀ a, 0 < value a) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       {n : ℕ} (T : Bool → MovingSlotData σ n) :
       let L := bulkLogLeafLists tier k (T false)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.bulkLogLeafLists