OAI/Probability/CubeShuffle/ExceptionalOperators.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeShuffle.ParallelBlocks.lift line 12
  2. lemma OAI.CubeShuffle.ParallelBlocks.lift_apply line 21
  3. def OAI.CubeShuffle.ParallelBlocks.injection line 23
  4. lemma OAI.CubeShuffle.ParallelBlocks.injection_apply line 29
  5. lemma OAI.CubeShuffle.ParallelBlocks.injection_commute line 34
  6. lemma OAI.CubeShuffle.ParallelBlocks.lift_product line 43
  7. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_uniform_absorb line 78
  8. lemma OAI.CubeShuffle.ParallelBlocks.local_average_commute line 91
  9. lemma OAI.CubeShuffle.ParallelBlocks.sampleOperator_parallel line 100
  10. def OAI.CubeShuffle.splitPerm line 125
  11. def OAI.CubeShuffle.outerPerm line 128
  12. lemma OAI.CubeShuffle.outerPerm_apply line 133
  13. lemma OAI.CubeShuffle.splitPerm_butterfly line 136
  14. lemma OAI.CubeShuffle.boundaryTree_node_raw line 148
  15. lemma OAI.CubeShuffle.boundaryOutput_node_raw line 157
  16. lemma OAI.CubeShuffle.boundaryTree_split line 163
  17. lemma OAI.CubeShuffle.splitPerm_boundaryTree line 190
  18. lemma OAI.CubeShuffle.boundaryOutput_split line 201
  19. abbrev OAI.CubeShuffle.OuterCoins line 220
  20. abbrev OAI.CubeShuffle.LocalCoins line 221
  21. def OAI.CubeShuffle.parallelSplitCoinEquiv line 223
  22. lemma OAI.CubeShuffle.parallelSplitCoinEquiv_apply line 228
  23. def OAI.CubeShuffle.pairAssembleEquiv line 232
  24. def OAI.CubeShuffle.palindromeStageEquiv line 239
  25. lemma OAI.CubeShuffle.palindromeStageEquiv_apply line 244
  26. def OAI.CubeShuffle.modifiedAssembleEquiv line 252
  27. def OAI.CubeShuffle.modifiedStageEquiv line 260
  28. lemma OAI.CubeShuffle.modifiedStageEquiv_apply line 266
  29. lemma OAI.CubeShuffle.palindrome_stage line 275
  30. def OAI.CubeShuffle.localModifiedPerm line 286
  31. lemma OAI.CubeShuffle.modified_stage line 290
  32. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_sandwich line 312
  33. lemma OAI.CubeShuffle.UnitaryFinite.localModified_average line 319
  34. lemma OAI.CubeShuffle.sampleOperator_palindrome_stage line 335
  35. lemma OAI.CubeShuffle.sampleOperator_modified_stage line 351
  36. def OAI.CubeShuffle.CommutingBlocks.retain line 376
  37. lemma OAI.CubeShuffle.CommutingBlocks.retain_commute line 380
  38. lemma OAI.CubeShuffle.CommutingBlocks.blocks_retain line 386
  39. def OAI.CubeShuffle.ParallelBlocks.centralProjection line 410
  40. lemma OAI.CubeShuffle.ParallelBlocks.centralProjection_commute line 414
  41. lemma OAI.CubeShuffle.ParallelBlocks.local_central_commute line 420
  42. lemma OAI.CubeShuffle.modified_central_average line 437
  43. lemma OAI.CubeShuffle.central_local_gap line 450
  44. lemma OAI.CubeShuffle.central_blocks_exception_bound line 457
  45. theorem OAI.CubeShuffle.palindrome_exception_bound line 479

    Source documentation

    The network comparison at a fixed central size is proved for the actual fair-coin operators. No spectral/PSD comparison hypothesis is inserted.

    theorem palindrome_exception_bound (r L : ℕ)
    (ρ : Representation ℂ (Equiv.Perm (Card r × Card L)) V) (hρ : IsUnitary ρ) (n : ℕ) :
    ‖sampleOperator (ρ.comp (splitPerm r L).toMonoidHom) (palindromePerm (L+r))‖ ≤
      (blockGap L)^n + ∑ E : Finset (Card r), if E.card<n then
        ‖sampleOperator (ρ.comp (splitPerm r L).toMonoidHom) (modifiedPerm L r E)‖ else 0 := by
…

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.splitPerm, OAI.CubeShuffle.palindromePerm, OAI.CubeShuffle.blockGap, OAI.CubeShuffle.modifiedPerm