OAI/Probability/CoordinateSweeps/Decomposition.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoordinateSweeps.schattenMoment_unitary_left line 31
2. def OAI.CoordinateSweeps.Grid.Holes.residualWithReference line 44
3. lemma OAI.CoordinateSweeps.Grid.Holes.residualWithReference_eq line 52
4. def OAI.CoordinateSweeps.Grid.Holes.averageWithReference line 62
5. theorem OAI.CoordinateSweeps.Grid.Holes.averageWithReference_moment line 68

   Source comment

   Arbitrary feasible reference choices preserve the literal, unnormalized moment.

   theorem averageWithReference_moment (hf : H.Feasible)
       (ω0 : {ω : G.Choices // H.Compatible ω}) (z : ℝ) (ρ : UnitaryIrrep H.stabilizer) (q : ℕ) :
       schattenMoment q (H.averageWithReference ω0 z ρ)=schattenMoment q (H.conditionalAverage hf z ρ) := by
   …

   Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.schattenMoment

6. def OAI.CoordinateSweeps.Grid.Holes.junctionIrrep line 88
7. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_eq_junction line 92

   Source comment

   Attachment of the checked law-level factorization to the exact main target.

   theorem conditionalAverage_eq_junction (hf : H.Feasible) (z : ℝ)
       (ρ : UnitaryIrrep H.stabilizer) :
       H.conditionalAverage hf z ρ=H.columnAverage hf z (H.junctionIrrep hf ρ).matrix*
         H.rowAverage hf z (H.junctionIrrep hf ρ).matrix := by
   …

   Mentions: OAI.CoordinateSweeps.UnitaryIrrep

8. abbrev OAI.CoordinateSweeps.Grid.Holes.JunctionFree line 111
9. def OAI.CoordinateSweeps.Grid.Holes.rowLabel line 112
10. def OAI.CoordinateSweeps.Grid.Holes.columnLabel line 113
11. lemma OAI.CoordinateSweeps.Grid.Holes.junctionTime line 115
12. def OAI.CoordinateSweeps.Grid.Holes.freeRow line 118

    Source comment

    The actual free row at the split layer is the child's terminal free set.

    def freeRow (y : B.Slot) : {x : H.JunctionFree // H.rowLabel x=y} ≃
        (H.rowHoles y).FreeAt (Fin.last A.b) where
    …

    Mentions: OAI.CoordinateSweeps.Grid.Holes.FreeAt

13. def OAI.CoordinateSweeps.Grid.Holes.freeColumn line 149

    Source comment

    The actual free column at the split layer is the child's initial free set.

    def freeColumn (x : A.Slot) : {y : H.JunctionFree // H.columnLabel y=x} ≃
        (H.columnHoles x).FreeAt 0 where
    …

    Mentions: OAI.CoordinateSweeps.Grid.Holes.FreeAt

14. lemma OAI.CoordinateSweeps.Grid.Holes.card_freeRow line 178
15. lemma OAI.CoordinateSweeps.Grid.Holes.card_freeColumn line 181
16. lemma OAI.CoordinateSweeps.Grid.rowSweep_inv_apply line 188
17. lemma OAI.CoordinateSweeps.Grid.columnSweep_inv_apply line 195
18. def OAI.CoordinateSweeps.Grid.Holes.outputStabilizerEquiv line 207
19. lemma OAI.CoordinateSweeps.Grid.Holes.outputStabilizer_residual line 211
20. def OAI.CoordinateSweeps.Grid.Holes.junctionFreeEquiv line 220
21. lemma OAI.CoordinateSweeps.Grid.Holes.rowResidual_split line 223
22. lemma OAI.CoordinateSweeps.Grid.Holes.columnResidual_split line 232
23. lemma OAI.CoordinateSweeps.Grid.Holes.rowResidual_label line 239
24. lemma OAI.CoordinateSweeps.Grid.Holes.columnResidual_label line 243
25. theorem OAI.CoordinateSweeps.Grid.Holes.rowResidual_fiber line 250

    Source comment

    Literal row-fiber permutation and the child's compatible residual agree in its output frame.

    theorem rowResidual_fiber (hf : H.Feasible) (ω : H.RowChoices) (y : B.Slot)
        (x : {x : H.JunctionFree // H.rowLabel x=y}) :
        H.freeRow y ⟨H.junctionFreeEquiv (H.rowResidual hf ω) x.val,
          (H.rowResidual_label hf ω x.val).trans x.property⟩=
        (H.rowHoles y).outputStabilizerEquiv ((H.refPair hf).1 y)
          ((H.rowHoles y).residualWithReference ((H.refPair hf).1 y) (ω y)) (H.freeRow y x) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid.Holes.outputStabilizerEquiv, OAI.CoordinateSweeps.Grid.Holes.residualWithReference

26. theorem OAI.CoordinateSweeps.Grid.Holes.columnResidual_fiber line 267

    Source comment

    Literal column-fiber permutation and the child's residual agree in its input frame; this is where the row/column orientations differ.

    theorem columnResidual_fiber (hf : H.Feasible) (ω : H.ColumnChoices) (y : A.Slot)
        (x : {x : H.JunctionFree // H.columnLabel x=y}) :
        H.freeColumn y ⟨H.junctionFreeEquiv (H.columnResidual hf ω) x.val,
          (H.columnResidual_label hf ω x.val).trans x.property⟩=
        (H.columnHoles y).stabilizerFreeEquiv
          ((H.columnHoles y).residualWithReference ((H.refPair hf).2 y) (ω y)) (H.freeColumn y x) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid.Holes.stabilizerFreeEquiv, OAI.CoordinateSweeps.Grid.Holes.residualWithReference

27. def OAI.CoordinateSweeps.Grid.Holes.rowIndex line 285
28. def OAI.CoordinateSweeps.Grid.Holes.columnIndex line 286
29. def OAI.CoordinateSweeps.Grid.Holes.rowSite line 287
30. def OAI.CoordinateSweeps.Grid.Holes.columnSite line 288
31. def OAI.CoordinateSweeps.Grid.Holes.rowLocalChart line 290
32. def OAI.CoordinateSweeps.Grid.Holes.columnLocalChart line 294
33. def OAI.CoordinateSweeps.Grid.Holes.rowChildEquiv line 299
34. def OAI.CoordinateSweeps.Grid.Holes.columnChildEquiv line 304
35. lemma OAI.CoordinateSweeps.Grid.Holes.rowResidual_index line 308
36. lemma OAI.CoordinateSweeps.Grid.Holes.columnResidual_index line 311
37. theorem OAI.CoordinateSweeps.Grid.Holes.row_restrict_eq line 315
38. theorem OAI.CoordinateSweeps.Grid.Holes.column_restrict_eq line 336
39. lemma OAI.CoordinateSweeps.Grid.Holes.rowResidual_as_fibers line 357
40. lemma OAI.CoordinateSweeps.Grid.Holes.columnResidual_as_fibers line 365
41. abbrev OAI.CoordinateSweeps.Grid.Holes.RowLocalChoices line 379
42. abbrev OAI.CoordinateSweeps.Grid.Holes.ColumnLocalChoices line 381
43. instance OAI.CoordinateSweeps.Grid.Holes.(instance at line 383) line 383
44. instance OAI.CoordinateSweeps.Grid.Holes.(instance at line 384) line 384
45. def OAI.CoordinateSweeps.Grid.Holes.rowChoiceFinEquiv line 386
46. def OAI.CoordinateSweeps.Grid.Holes.columnChoiceFinEquiv line 389
47. def OAI.CoordinateSweeps.Grid.Holes.rowLocalWeight line 393
48. def OAI.CoordinateSweeps.Grid.Holes.columnLocalWeight line 395
49. def OAI.CoordinateSweeps.Grid.Holes.rowLocalPerm line 397
50. def OAI.CoordinateSweeps.Grid.Holes.columnLocalPerm line 399
51. def OAI.CoordinateSweeps.Grid.Holes.junctionTensorAction line 402
52. theorem OAI.CoordinateSweeps.Grid.Holes.rowAverage_eq_ambient line 406
53. theorem OAI.CoordinateSweeps.Grid.Holes.columnAverage_eq_ambient line 422
54. theorem OAI.CoordinateSweeps.Grid.Holes.rowLocalMoment line 438
55. theorem OAI.CoordinateSweeps.Grid.Holes.columnLocalMoment line 447
56. lemma OAI.CoordinateSweeps.evenTrace_real line 460
57. theorem OAI.CoordinateSweeps.Grid.Holes.row_projected_moment line 473
58. theorem OAI.CoordinateSweeps.Grid.Holes.column_projected_moment line 493
59. lemma OAI.CoordinateSweeps.Grid.Holes.row_size_le line 518
60. lemma OAI.CoordinateSweeps.Grid.Holes.column_size_le line 523
61. theorem OAI.CoordinateSweeps.Grid.Holes.row_moment_bound line 529
62. theorem OAI.CoordinateSweeps.Grid.Holes.column_moment_bound line 544