OAI/Probability/CubeShuffle/Generation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_palindrome line 10
2. def OAI.CubeShuffle.butterflyIdentity line 23
3. lemma OAI.CubeShuffle.pairSwitch_false line 27
4. lemma OAI.CubeShuffle.childLift_one line 33
5. lemma OAI.CubeShuffle.butterflyIdentity_perm line 37
6. def OAI.CubeShuffle.childInjection line 42
7. lemma OAI.CubeShuffle.childInjection_swap line 51
8. lemma OAI.CubeShuffle.pairSwitch_single line 71
9. theorem OAI.CubeShuffle.butterfly_generates line 85

   Source documentation

   Every genuine butterfly outcome generates the full symmetric group.

   theorem butterfly_generates (d : ℕ) (H : Subgroup (Equiv.Perm (Card d)))
       (hH : ∀ ω : Butterfly d, butterflyPerm d ω∈H) : H=⊤ := by
   …

   Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.butterflyPerm

10. lemma OAI.CubeShuffle.butterfly_closure line 125
11. lemma OAI.CubeShuffle.palindrome_identity line 133
12. lemma OAI.CubeShuffle.palindrome_range_contains_butterfly line 138
13. lemma OAI.CubeShuffle.palindrome_support_generates line 146
14. def OAI.CubeShuffle.palindromeMinorant line 153
15. def OAI.CubeShuffle.blockGap line 158
16. lemma OAI.CubeShuffle.blockGap_pos line 160
17. lemma OAI.CubeShuffle.blockGap_lt_one line 161
18. theorem OAI.CubeShuffle.palindrome_off_invariants_gap line 165

    Source documentation

    Strict fixed-size palindrome contraction is derived from its actual coins, not assumed, and is uniform in the represented space.

    theorem palindrome_off_invariants_gap (d : ℕ) {V : Type*}
        [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]
        (ρ : Representation ℂ (Equiv.Perm (Card d)) V) (hρ : UnitaryFinite.IsUnitary ρ) :
        ‖UnitaryFinite.weightedOperator ρ (sampleLaw (palindromePerm d))-
          UnitaryFinite.uniformOperator ρ‖≤blockGap d := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.UnitaryFinite.weightedOperator, OAI.CubeShuffle.sampleLaw, OAI.CubeShuffle.palindromePerm, OAI.CubeShuffle.UnitaryFinite.uniformOperator, OAI.CubeShuffle.blockGap