OAI/Probability/CubeShuffle/Physical.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.insertNth_castSucc_snoc line 9
2. lemma OAI.CubeShuffle.rotate_cons line 24
3. lemma OAI.CubeShuffle.rotate_insert line 27
4. def OAI.CubeShuffle.insertionPerm line 32

   Source documentation

   Move the first coordinate to a specified slot, without changing the order of the others.

   def insertionPerm (d : ℕ) (i : Fin (d+1)) : Equiv.Perm (Card (d+1)) :=
   …

   Mentions: OAI.CubeShuffle.Card

5. lemma OAI.CubeShuffle.insertionPerm_apply line 36
6. lemma OAI.CubeShuffle.insertionPerm_zero line 39
7. lemma OAI.CubeShuffle.insertionPerm_last line 43
8. lemma OAI.CubeShuffle.physical_carry_step line 48
9. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_mul_const line 75
10. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_const_mul line 79
11. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_run line 83
12. def OAI.CubeShuffle.carryCoins line 103

    Source documentation

    Splitting a fair coin layer according to an inserted carried bit is a bijection.

    def carryCoins (d : ℕ) (i : Fin (d+1)) : (Bool → Coins (d+1)) ≃ Coins (d+2) where
    …

    Mentions: OAI.CubeShuffle.Coins

13. lemma OAI.CubeShuffle.physical_carry_average line 111
14. theorem OAI.CubeShuffle.physical_sweep_recursion line 132

    Source documentation

    Exact physical sweep recursion, with rotations telescoped rather than replacing physical time by an independent network time parameter.

    theorem physical_sweep_recursion (d : ℕ)
        (ρ : Representation ℂ (Equiv.Perm (Card (d+1))) V) :
        (sampleOperator ρ (step (d+1)))^(d+1)=
          (sampleOperator ρ (fun ξ : Bool → Coins d => childLift (fun b => step d (ξ b))))^d*
            sampleOperator ρ (pairSwitch (d := d)) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.step, OAI.CubeShuffle.Coins, OAI.CubeShuffle.childLift, OAI.CubeShuffle.pairSwitch

15. lemma OAI.CubeShuffle.childInjection_product line 165
16. lemma OAI.CubeShuffle.childInjection_commute line 173
17. lemma OAI.CubeShuffle.sampleOperator_child line 184
18. lemma OAI.CubeShuffle.sampleOperator_child_commute line 200
19. lemma OAI.CubeShuffle.inverse_butterfly_average_step line 207
20. theorem OAI.CubeShuffle.physical_sweep_inverse_butterfly line 232

    Source documentation

    A physical sweep of exactly d shuffles is the adjoint-oriented fair butterfly, on every representation and every labeled card.

    theorem physical_sweep_inverse_butterfly (d : ℕ)
        (ρ : Representation ℂ (Equiv.Perm (Card d)) V) :
        (sampleOperator ρ (step d))^d=
          sampleOperator ρ (fun ω => (butterflyPerm d (decodeButterfly d ω))⁻¹) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.step, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly

21. lemma OAI.CubeShuffle.physical_sweep_adjoint line 246