ScheduledFinalPermutation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The final parity reassignments as permutations of actual active slots

def OAI.Ostmann.scheduledWordH line 14
Source documentation
An actual copied word coordinate belongs to H at every depth.
```
noncomputable def scheduledWordH {I : Type*} (role : I → CopyScheduleRole)
    (n : ℕ) (t : Fin n → Bool) (i : {i : I // role i = .word}) :
    CopyScheduleH role n :=
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH
theorem OAI.Ostmann.scheduledWordH_injective line 20
def OAI.Ostmann.scheduledWordHEquiv line 29
def OAI.Ostmann.scheduledParityCoordinates line 44
def OAI.Ostmann.scheduledFinalPerm line 52
Source documentation
Only actual word coordinates are reassigned. Every other H coordinate, including future pivots and fresh anchors, is fixed.
```
noncomputable def scheduledFinalPerm {I : Type*} (role : I → CopyScheduleRole)
    (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
    (e : FinalParityReassignments n m) : Equiv.Perm (CopyScheduleH role (n + 1)) :=
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleH
theorem OAI.Ostmann.scheduledFinalPerm_word line 58
theorem OAI.Ostmann.scheduledFinalPerm_other line 73
theorem OAI.Ostmann.scheduledFinalPerm_injective line 81
theorem OAI.Ostmann.scheduledFinalPerm_origin line 97

theorem OAI.Ostmann.scheduledFinalPerm_product_prior line 112

Source documentation

Each original marginal is preserved, including different marginals for bulk, top, anchor and pivot roles.

theorem scheduledFinalPerm_product_prior {I A : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (n m : ℕ)
    (word : Fin m ≃ {i : I // role i = .word}) (e : FinalParityReassignments n m)
    (μ : I → A → ℝ) (x : CopyScheduleH role (n + 1) → A) :
    (∏ h, μ (copyScheduleOrigin (n + 1) h.val)
      (x (scheduledFinalPerm role n m word e h))) =
    ∏ h, μ (copyScheduleOrigin (n + 1) h.val) (x h) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.scheduledFinalPerm