MovingBulkFrames.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed nonbulk factors and literal bulk products at each moving node

structure OAI.Ostmann.MovingFrameConstants line 10
def OAI.Ostmann.movingFrameConstants line 17
Source documentation
These factors are computed from the fixed small and internal samples; no bulk coordinate or giant value is used.
```
def movingFrameConstants {σ : Type*} (value : σ → ℕ) :
    (n : ℕ) → TreeLeafTuple (List σ) n → MovingSampleSlots σ n →
      List Bool → MovingFrameConstants
  | 0, _, .leaf, _ => ⟨1, 1, 1⟩
  | n + 1, small, .node a l r, path =>
      let u := movingCompensationSlots n a
…
```
Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.MovingFrameConstants, OAI.Ostmann.movingCompensationSlots

def OAI.Ostmann.movingBulkProducts line 31

Source documentation

The two child bulk products in the same root-to-node order.

def movingBulkProducts {σ : Type*} (value : σ → ℕ) :
    (n : ℕ) → TreeLeafTuple (List σ) n → List Bool → ℕ × ℕ
  | 0, _, _ => (1, 1)
  | n + 1, bulk, [] =>
      (MovingSlotReversal.naturalProduct value (flattenMovingSlots n bulk.1),
        MovingSlotReversal.naturalProduct value (flattenMovingSlots n bulk.2))
  | n + 1, bulk, false :: path => movingBulkProducts value n bulk.1 path
  | n + 1, bulk, true :: path => movingBulkProducts value n bulk.2 path

/-- Every actual transfer node has its fixed small factor, its current giant,
and precisely the bulk product from its own child subtree. -/

Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.flattenMovingSlots

theorem OAI.Ostmann.movingNodeAtPath_products line 42

Source documentation

Every actual transfer node has its fixed small factor, its current giant, and precisely the bulk product from its own child subtree.

theorem movingNodeAtPath_products {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) (n : ℕ) (t : FrequencyTree ℤ n)
    (small bulk : TreeLeafTuple (List σ) n) (a : MovingSampleSlots σ n)
    (XL XR : ℕ) (path : List Bool) (hp : path.length < n) :
    let z := (transferNodeAtPath (movingSlotSystem value childBound pivotBound) n
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.transferNodeAtPath, OAI.Ostmann.movingSlotSystem