MovingGiantAncestorValues.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual moving giants are the selected proper ancestor quotients

The preorder pivot array is divided by its own sampled compensation product. The current giants use exactly these quotients, rather than the composite pivots that enter the generic transfer-history recursion.

def OAI.Ostmann.movingNodeGiant line 17
def OAI.Ostmann.movingGiantArray line 21

theorem OAI.Ostmann.movingNodeAtPath_giants line 29

Source documentation

Following a path updates the two giants with the actual quotient at each proper prefix. The hypothesis just names these computed values.

theorem movingNodeAtPath_giants {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) (n : ℕ) (T : MovingSlotData σ n)
    (t : FrequencyTree ℤ n) (XL XR : ℕ) (path : List Bool) (hp : path.length < n)
    (d : ℕ) (p : ℕ → ℤ)
    (hanc : ∀ k < path.length, p (d + k) =
      (movingNodeGiant value childBound pivotBound
        (transferNodeAtPath (movingSlotSystem value childBound pivotBound) n
          ⟨n, T, XL, XR⟩ t (path.take k)) : ℤ)) :
    let z := (transferNodeAtPath (movingSlotSystem value childBound pivotBound) n
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingNodeGiant, OAI.Ostmann.transferNodeAtPath, OAI.Ostmann.movingSlotSystem

theorem OAI.Ostmann.movingGiantArray_sources line 80

Source documentation

The source expression in the ancestor scheme evaluates to the actual natural giant on each side of a preorder node.

theorem movingGiantArray_sources {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) (n : ℕ) (T : MovingSlotData σ n)
    (t : FrequencyTree ℤ n) (XL XR : ℕ) (j : Fin (2 ^ n - 1)) :
    let p := movingGiantArray value childBound pivotBound n ⟨n, T, XL, XR⟩ t
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingGiantArray