OAI/NumberTheory/Ostmann/Arithmetic/MovingSlotStateRelabel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotState.map line 11
2. theorem OAI.Ostmann.MovingSlotState.map_depth line 14
3. theorem OAI.Ostmann.MovingSlotState.map_data line 17
4. theorem OAI.Ostmann.MovingSlotState.map_leftGiant line 20
5. theorem OAI.Ostmann.MovingSlotState.map_rightGiant line 23
6. theorem OAI.Ostmann.MovingSlotState.leftProduct_map line 26
7. theorem OAI.Ostmann.MovingSlotState.rightProduct_map line 33
8. theorem OAI.Ostmann.MovingSlotState.compensation_map line 40
9. theorem OAI.Ostmann.MovingSlotState.child_map line 47
10. theorem OAI.Ostmann.movingSlotSystem_leftState_map line 55
11. theorem OAI.Ostmann.movingSlotSystem_rightState_map line 61
12. theorem OAI.Ostmann.movingHistoryPivot_map line 67
13. theorem OAI.Ostmann.movingValidTransferNode_map line 75
14. theorem OAI.Ostmann.movingRecursiveWeight_map line 92

    Source documentation

    A relabeling evaluates every original pivot and guard, including the integer division by the sampled compensation product.

    theorem movingRecursiveWeight_map {σ τ : Type*} (f : σ → τ)
        (value : τ → ℕ) (childBound pivotBound : ℕ → ℕ)
        (leaf : MovingSlotState τ → ℤ → ℂ)
        (cutoff : MovingSlotState τ → ℤ → ℤ → ℤ → ℝ)
        (n : ℕ) (x : MovingSlotState σ) (t : FrequencyTree ℤ n) :
        recursiveTransferWeight (movingSlotSystem value childBound pivotBound) leaf cutoff n (x.map f) t =
          recursiveTransferWeight (movingSlotSystem (value ∘ f) childBound pivotBound)
            (fun x => leaf (x.map f)) (fun x => cutoff (x.map f)) n x t := by
    …

    Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem