OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSupportedSampleTerm_bulk_log line 11
2. theorem OAI.Ostmann.movingSupportedSampledWeight_bulk_log line 33

   Source documentation

   Extracting the logarithmic weights does not restrict the independent compensation prior. Its zero terms vanish; every remaining draw has the prescribed tier and therefore gives the same external bulk factor.

   theorem movingSupportedSampledWeight_bulk_log {σ : Type} [Fintype σ]
       (value tier : σ → ℕ) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       (μ : ℕ → σ → ℝ) (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
       (hn : n ≤ k) (hsmall : ∀ i ∈ flattenMovingSlots n small, tier i ≠ k)
       (hbulk : ∀ i ∈ flattenMovingSlots n bulk, tier i = k) (XL XR : ℕ) :
       movingSupportedSampledWeight value outside μ childBound pivotBound
           (fun x s => (movingBulkLeafLogWeight value tier k outside cb cd x.data : ℂ) * F x s)
           E n t small bulk XL XR =
         ((treeLeafProduct n (treeLeafMap (movingBulkListLogWeight value outside cb cd) n bulk) : ℝ) : ℂ) *
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingSupportedSampledWeight, OAI.Ostmann.movingBulkLeafLogWeight, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingBulkListLogWeight

3. theorem OAI.Ostmann.movingFrequencyCoefficient_bulk_log line 58