MovingTransferSlots.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Reindexing the original pivot, compensation, and surviving slots

theorem OAI.Ostmann.movingRegularTransform_equiv line 12

Source documentation

Reindexing changes neither the cofactor nor its local transform.

theorem movingRegularTransform_equiv {I J : Type*} [Fintype I] [Fintype J]
    (e : I ≃ J) (p : J → ℕ) [∀ j, NeZero (p j)]
    (g : ∀ j, ZMod (p j) → ℂ) (D : ℕ) (s : ℤ) :
    let _ : ∀ i, NeZero (p (e i)) := fun _i => inferInstance
…

def OAI.Ostmann.movingTransferSlotEquiv line 26
Source documentation
The first block is the removed giant and compensation. The second is one surviving giant and its remaining regular slots.
```
def movingTransferSlotEquiv (n r m : ℕ) :
    ((Unit ⊕ (TreeLeafIndex n × Fin 4)) ⊕ (Unit ⊕ MovingRegularSlot n r m)) ≃
      (Bool ⊕ MovingRegularSlot n (4 + r) m) where
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot
theorem OAI.Ostmann.movingTransferSlotEquiv_pivot line 66
theorem OAI.Ostmann.movingTransferSlotEquiv_old_giant line 69

theorem OAI.Ostmann.movingTransferSlotEquiv_values line 74

Source documentation

The reindexing inserts precisely the same sampled compensation vector which appears in the two child coefficients.

theorem movingTransferSlotEquiv_values {A : Type*} (value : A → ℕ) (n r m : ℕ)
    (u : TreeLeafIndex n × Fin 4 → A) (y : MovingRegularSlot n r m → A) (XL XR : ℕ) :
    (fun i => Sum.elim (fun b => if b then XL else XR)
      (value ∘ movingRestoreSample n r m u y) (movingTransferSlotEquiv n r m i)) =
    Sum.elim (Sum.elim (fun _ : Unit => XL) (value ∘ u))
      (Sum.elim (fun _ : Unit => XR) (value ∘ y)) := by
…

Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingRestoreSample, OAI.Ostmann.movingTransferSlotEquiv