MovingHistoryUniqueness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Rigidity of the actual moving-giant histories at fixed samples

theorem OAI.Ostmann.movingValidHistory_build_iff line 13

Source documentation

Frequencies stored in the slot data do not enter the products, bounds, or child slots in the rigidity predicate. They may be replaced by one fixed template before comparing two histories.

theorem movingValidHistory_build_iff {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ) (n : ℕ)
    (t u v : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (a : MovingSampleSlots σ n) (XL XR : ℕ) :
    ValidTransferHistory (movingSlotSystem value childBound pivotBound) n
      ⟨n, buildMovingSlotData n t small bulk a, XL, XR⟩ v ↔
    ValidTransferHistory (movingSlotSystem value childBound pivotBound) n
      ⟨n, buildMovingSlotData n u small bulk a, XL, XR⟩ v := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.buildMovingSlotData

theorem OAI.Ostmann.movingRecursiveWeight_history_unique line 53

Source documentation

Original support forces a unique full frequency history when all actual internal samples, top primes and the root frequency have been fixed.

theorem movingRecursiveWeight_history_unique {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (t u : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (a : MovingSampleSlots σ n) (XL XR : ℕ)
    (ht : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
      (movingSlotCutoff value childBound pivotBound E) n
      ⟨n, buildMovingSlotData n t small bulk a, XL, XR⟩ t ≠ 0)
    (hu : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
      (movingSlotCutoff value childBound pivotBound E) n
      ⟨n, buildMovingSlotData n u small bulk a, XL, XR⟩ u ≠ 0)
    (hroot : frequencyRoot n t = frequencyRoot n u) : t = u := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.frequencyRoot