OAI/LinearAlgebra/MatrixState/Postselection.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RowColumn.WordOrbits.transporterEquiv line 15

   Source documentation

   All transporters between two words are exactly the independent bijections between corresponding color fibres.

   def transporterEquiv (a b : S → A) :
       {p : Equiv.Perm S // ∀ x, b (p x) = a x} ≃
         (∀ c : A, {x : S // a x = c} ≃ {x : S // b x = c}) where
   …

2. lemma OAI.RowColumn.WordOrbits.card_transporters line 37
3. lemma OAI.RowColumn.WordOrbits.type_card_factorial line 56

   Source documentation

   Orbit-stabilizer with all factors explicit. It is the exact multinomial cardinality needed for the finite postselection probability.

   lemma type_card_factorial (a : S → A) :
       Fintype.card {b : S → A // counts b = counts a} *
         (∏ c : A, (Fintype.card {x : S // a x = c})!) = (Fintype.card S)! := by
   …

   Mentions: OAI.RowColumn.WordOrbits.counts

4. lemma OAI.RowColumn.WordOrbits.factorial_le_factorial_mul_pow line 96
5. lemma OAI.RowColumn.WordOrbits.factorial_mode line 107
6. lemma OAI.RowColumn.WordOrbits.prod_by_counts line 127
7. lemma OAI.RowColumn.WordOrbits.sum_counts line 137
8. lemma OAI.RowColumn.WordOrbits.empirical_type_mode line 142

   Source documentation

   Under its own empirical product distribution, a type is a mode among all types. This gives a polynomial lower bound without Stirling or entropy.

   lemma empirical_type_mode (a b : S → A) :
       Fintype.card {w : S → A // counts w = counts b} *
         (∏ c : A, (counts a c).val ^ (counts b c).val) ≤
       Fintype.card {w : S → A // counts w = counts a} *
         (∏ c : A, (counts a c).val ^ (counts a c).val) := by
   …

   Mentions: OAI.RowColumn.WordOrbits.counts

9. def OAI.RowColumn.WordOrbits.typeMass line 171
10. lemma OAI.RowColumn.WordOrbits.typeMass_le_mode line 174
11. lemma OAI.RowColumn.WordOrbits.sum_typeMass line 183
12. lemma OAI.RowColumn.WordOrbits.empirical_mass_lower line 199

    Source documentation

    Elementary finite postselection mass bound: an empirical type has at least the inverse number of possible occupation tables.

    lemma empirical_mass_lower (a : S → A) :
        (Fintype.card S)^(Fintype.card S) ≤
          (Fintype.card S+1)^(Fintype.card A) * typeMass a (counts a) := by
    …

    Mentions: OAI.RowColumn.WordOrbits.typeMass, OAI.RowColumn.WordOrbits.counts

13. def OAI.RowColumn.Postselection.empiricalAmplitude line 213
14. def OAI.RowColumn.Postselection.tensorVector line 216
15. lemma OAI.RowColumn.Postselection.normSq_empiricalAmplitude line 219
16. lemma OAI.RowColumn.Postselection.empiricalAmplitude_normalized line 226
17. lemma OAI.RowColumn.Postselection.normSq_tensorVector line 233
18. lemma OAI.RowColumn.Postselection.normSq_empirical_tensor line 238
19. lemma OAI.RowColumn.Postselection.empirical_type_probability line 247
20. abbrev OAI.RowColumn.Postselection.CountIndex line 266
21. abbrev OAI.RowColumn.Postselection.Phases line 267
22. def OAI.RowColumn.Postselection.countCharacter line 269
23. lemma OAI.RowColumn.Postselection.countCharacter_single line 275
24. lemma OAI.RowColumn.Postselection.countCharacter_injective line 279
25. lemma OAI.RowColumn.Postselection.character_orthogonality line 290
26. lemma OAI.RowColumn.Postselection.phase_parseval line 303

    Source documentation

    Finite exact phase integration: order n+1 resolves every occupation vector with entries in 0,...,n, with no analytical Haar integral.

    lemma phase_parseval (f : CountIndex A n → ℂ) :
        (∑ θ : Phases A n, Complex.normSq (∑ q, countCharacter q θ * f q)) =
          (Fintype.card (Phases A n) : ℝ) * ∑ q, Complex.normSq (f q) := by
    …

    Mentions: OAI.RowColumn.Postselection.CountIndex, OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.countCharacter

27. lemma OAI.RowColumn.Postselection.phase_single_bound line 321
28. lemma OAI.RowColumn.Postselection.normSq_sum_mul_le line 333
29. abbrev OAI.RowColumn.Postselection.Types line 346
30. def OAI.RowColumn.Postselection.typeSize line 347
31. def OAI.RowColumn.Postselection.typeSum line 348
32. def OAI.RowColumn.Postselection.typeAverage line 351
33. def OAI.RowColumn.Postselection.typeRepresentative line 354
34. lemma OAI.RowColumn.Postselection.representative_counts line 358
35. lemma OAI.RowColumn.Postselection.typeAverage_pair line 364
36. lemma OAI.RowColumn.Postselection.typeAverage_normSq line 385
37. lemma OAI.RowColumn.Postselection.invariant_vector_bound line 403
38. lemma OAI.RowColumn.Postselection.char_sum line 417
39. def OAI.RowColumn.Postselection.typeAmplitude line 425
40. lemma OAI.RowColumn.Postselection.tensorVector_by_counts line 429
41. def OAI.RowColumn.Postselection.twistedAmplitude line 432
42. lemma OAI.RowColumn.Postselection.twistedAmplitude_normalized line 436
43. lemma OAI.RowColumn.Postselection.countCharacter_eq_prod line 445
44. lemma OAI.RowColumn.Postselection.tensorVector_twisted line 454
45. lemma OAI.RowColumn.Postselection.twisted_pair line 462
46. lemma OAI.RowColumn.Postselection.type_phase_bound line 475
47. lemma OAI.RowColumn.Postselection.type_representative_bound line 486
48. theorem OAI.RowColumn.Postselection.symmetric_postselection line 522

    Source documentation

    Exact finite symmetric-vector postselection, with a polynomial cost in the slot number and alphabet size. Every mixture vector is a normalized identical-slot tensor power; the construction is explicit and finite.

    theorem symmetric_postselection (a₀ : S → A) (hn : 0 < Fintype.card S)
        (v x : (S → A) → ℂ) (hv : ∀ a b, counts a = counts b → v a = v b) :
        Complex.normSq (∑ w, v w * x w) ≤
          (∑ w, Complex.normSq (v w)) *
          (((Fintype.card S+1)^(Fintype.card A) : ℕ) /
            (Fintype.card (Phases A (Fintype.card S)) : ℝ) *
          ∑ q : Types (S := S) (A := A),
    …

    Mentions: OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.Types

49. def OAI.RowColumn.Postselection.truncateAmplitude line 545

    Source documentation

    Truncating purification letters preserves positivity after partial trace. It is how the postselection mixture is constrained to even one-slot states.

    def truncateAmplitude (good : A → Prop) [DecidablePred good] (z : A → ℂ) : A → ℂ :=
    …

50. lemma OAI.RowColumn.Postselection.tensorVector_truncate line 549
51. lemma OAI.RowColumn.Postselection.truncated_twisted_subnormalized line 560
52. theorem OAI.RowColumn.Postselection.supported_symmetric_postselection line 573

    Source documentation

    Symmetric postselection retaining a prescribed alphabet support. In the application good(c,e) means that the physical and auxiliary parities agree, so the resulting Gram states are block diagonal.

    theorem supported_symmetric_postselection (a₀ : S → A) (hn : 0 < Fintype.card S)
        (good : A → Prop) [DecidablePred good] (v x : (S → A) → ℂ)
        (hv : ∀ a b, counts a = counts b → v a = v b)
        (hsupp : ∀ w, ¬ (∀ i, good (w i)) → v w = 0) :
        Complex.normSq (∑ w, v w * x w) ≤
          (∑ w, Complex.normSq (v w)) *
          (((Fintype.card S+1)^(Fintype.card A) : ℕ) /
            (Fintype.card (Phases A (Fintype.card S)) : ℝ) *
          ∑ q : Types (S := S) (A := A),
    …

    Mentions: OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.Types

53. def OAI.RowColumn.Postselection.pairWordsEquiv line 603
54. def OAI.RowColumn.Postselection.purificationVector line 609
55. def OAI.RowColumn.Postselection.purificationTest line 612
56. def OAI.RowColumn.Postselection.productPurifier line 615
57. def OAI.RowColumn.Postselection.purifierQuadratic line 617
58. def OAI.RowColumn.Postselection.purifierTrace line 620
59. lemma OAI.RowColumn.Postselection.purification_pair line 623
60. lemma OAI.RowColumn.Postselection.purification_normSq line 632
61. lemma OAI.RowColumn.Postselection.productPurifier_pair line 639
62. lemma OAI.RowColumn.Postselection.purification_invariant line 645
63. theorem OAI.RowColumn.Postselection.matrix_postselection line 663

    Source documentation

    Explicit positive identical-slot domination at the purification level. The matrix factor is symmetric under actual slot permutations and has the specified letter support. This is the quantitative local-state dependency of the occupied-board main, not an assumed main overlap estimate.

    theorem matrix_postselection (a₀ : S → C × C) (hn : 0 < Fintype.card S)
        (good : C × C → Prop) [DecidablePred good]
        (B : (S → C) → (S → C) → ℂ)
        (hB : ∀ (p : Equiv.Perm S) (w v : S → C),
          B (fun i => w (p i)) (fun i => v (p i)) = B w v)
        (hsupp : ∀ w v, ¬ (∀ i, good (w i,v i)) → B w v = 0)
        (x : (S → C) → ℂ) :
        purifierQuadratic B x ≤ purifierTrace B *
          (((Fintype.card S+1)^(Fintype.card (C × C)) : ℕ) /
            (Fintype.card (Phases (C × C) (Fintype.card S)) : ℝ) *
          ∑ q : Types (S := S) (A := C × C),
    …

    Mentions: OAI.RowColumn.Postselection.purifierQuadratic, OAI.RowColumn.Postselection.purifierTrace, OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.Types

64. lemma OAI.RowColumn.MatrixState.sqrt_commute line 699
65. lemma OAI.RowColumn.MatrixState.commute_perm_iff line 704
66. lemma OAI.RowColumn.MatrixState.sqrt_permutation_invariant line 716
67. lemma OAI.RowColumn.MatrixState.commute_diagonal_iff line 721
68. lemma OAI.RowColumn.MatrixState.sqrt_block_supported line 730
69. def OAI.RowColumn.MatrixState.quadratic line 746

    Source documentation

    Bilinear-coordinate quadratic form. Complex conjugation is placed in the second coordinate, matching the purification formulas used below.

    def quadratic (A : Matrix I I ℂ) (x : I → ℂ) : ℝ :=
    …

70. def OAI.RowColumn.MatrixState.factorQuadratic line 749
71. lemma OAI.RowColumn.MatrixState.normSq_eq_re line 752
72. lemma OAI.RowColumn.MatrixState.factorQuadratic_eq line 757
73. lemma OAI.RowColumn.MatrixState.sqrt_factorQuadratic line 774
74. lemma OAI.RowColumn.MatrixState.sqrt_trace line 779
75. def OAI.RowColumn.MatrixState.tensorMatrix line 801
76. lemma OAI.RowColumn.MatrixState.tensorMatrix_mul line 805
77. lemma OAI.RowColumn.MatrixState.tensorMatrix_star line 812
78. lemma OAI.RowColumn.MatrixState.tensorMatrix_trace line 818
79. lemma OAI.RowColumn.MatrixState.tensorMatrix_one line 824
80. lemma OAI.RowColumn.MatrixState.tensorMatrix_posSemidef line 833
81. def OAI.RowColumn.MatrixState.letterMatrix line 845
82. def OAI.RowColumn.MatrixState.gramState line 848

    Source documentation

    A purification letter z is an actual one-slot substate after partial trace.

    def gramState (z : C × C → ℂ) : Matrix C C ℂ :=
    …

83. lemma OAI.RowColumn.MatrixState.gramState_posSemidef line 852
84. lemma OAI.RowColumn.MatrixState.gramState_trace line 858
85. lemma OAI.RowColumn.MatrixState.gramState_parity_supported line 871
86. def OAI.RowColumn.Postselection.reindexWord line 889
87. lemma OAI.RowColumn.Postselection.productPurifier_quadratic line 896
88. def OAI.RowColumn.Postselection.localAmplitude line 903
89. def OAI.RowColumn.Postselection.localState line 908
90. lemma OAI.RowColumn.Postselection.localState_positive line 913
91. lemma OAI.RowColumn.Postselection.localState_trace_le_one line 918
92. lemma OAI.RowColumn.Postselection.localState_even line 926
93. theorem OAI.RowColumn.Postselection.positive_state_postselection line 937

    Source documentation

    Quantitative positive mixture of genuine even identical-slot states for a PSD matrix invariant under unsigned slot permutations and supported on physical parity blocks. The polynomial includes only the explicitly finite type count; no structural duality or postselection axiom is assumed.

    theorem positive_state_postselection (a₀ : S → C × C) (hn : 0 < Fintype.card S)
        (odd : C → Prop) [DecidablePred odd] (A : Matrix (S → C) (S → C) ℂ)
        (hA : A.PosSemidef)
        (hinv : ∀ (p : Equiv.Perm S) (w v : S → C),
          A (fun i => w (p i)) (fun i => v (p i)) = A w v)
        (hsupp : ∀ w v, ¬ (∀ i, odd (w i) ↔ odd (v i)) → A w v = 0)
        (x : (S → C) → ℂ) :
        quadratic A x ≤ A.trace.re *
          (((Fintype.card S+1)^(Fintype.card (C × C)) : ℕ) /
            (Fintype.card (Phases (C × C) (Fintype.card S)) : ℝ) *
          ∑ q : Types (S := S) (A := C × C),
    …

    Mentions: OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.Types