MovingSampledRecursion.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Expanding the sampled giant recursion into its literal histories

This is the recursion of Section 7.4 (7.10)--(7.11), rather than the whole-atom recursion of Section 4. Each root sample is used by both children. The child sample trees are independent under the original finite law.

def OAI.Ostmann.MovingSlotData.frequencyTree line 16
theorem OAI.Ostmann.buildMovingSlotData_frequencyTree line 21
def OAI.Ostmann.movingFrequencySkeleton line 31
Source documentation
Discard descendant prime data, keeping all their frequencies. Root cutoffs may still impose the cross-branch frequency tests of Section 7.4.
```
def movingFrequencySkeleton (σ : Type*) : (n : ℕ) → FrequencyTree ℤ n → MovingSlotData σ n
  | 0, t => .leaf t []
  | n + 1, t => .node t.1 [] [] []
      (movingFrequencySkeleton σ n t.2.1) (movingFrequencySkeleton σ n t.2.2)
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.MovingSlotData
def OAI.Ostmann.MovingSlotData.rootData line 36
def OAI.Ostmann.movingRootState line 41
def OAI.Ostmann.movingLocalExtra line 48
Source documentation
Original node factors depend on the current prime lists, two giants and complete frequency tree, not on prime samples which will be made later.
```
noncomputable def movingLocalExtra {σ : Type*}
    (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (x : MovingSlotState σ) (s v w : ℤ) : ℝ :=
…
```
Mentions: OAI.Ostmann.MovingSlotState
def OAI.Ostmann.movingSampleRootFactor line 53

theorem OAI.Ostmann.movingSample_weight_node line 66

Source documentation

The actual termwise node identity, including failed integer and divisibility tests. The new giant is the quotient of the composite pivot.

theorem movingSample_weight_node {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (t : FrequencyTree ℤ (n + 1))
    (small bulk : TreeLeafTuple (List σ) (n + 1))
    (a : TreeLeafTuple (Fin 4 → σ) n) (l r : MovingSampleSlots σ n) (XL XR : ℕ) :
    let u := movingCompensationSlots n a
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingCompensationSlots

def OAI.Ostmann.movingSampledWeight line 130

Source documentation

The finite expansion keeps every internal sample's original prior.

noncomputable def movingSampledWeight {σ : Type*} [Fintype σ] (value : σ → ℕ)
    (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) : ℂ :=
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple

theorem OAI.Ostmann.movingSampledWeight_node line 139