OAI/RepresentationTheory/Tensor/Postselection.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.OrdinaryTensor.count line 17

   Source comment

   Occupancies of single alphabet symbols in an ordinary tensor word.

   def count (w : I → A) (a : A) : ℕ := Fintype.card {i : I // w i = a}

   Mentions: OAI.CoordinateSweeps.a

2. def OAI.CoordinateSweeps.OrdinaryTensor.permute line 20

   Source comment

   Ordinary tensor permutation, with the manuscript's product convention.

   def permute (σ : Equiv.Perm I) : Equiv.Perm (I → A) where
   …

3. lemma OAI.CoordinateSweeps.OrdinaryTensor.permute_mul line 27
4. lemma OAI.CoordinateSweeps.OrdinaryTensor.count_le line 32
5. lemma OAI.CoordinateSweeps.OrdinaryTensor.sum_count line 35
6. lemma OAI.CoordinateSweeps.OrdinaryTensor.counts_eq_exists_perm line 40
7. def OAI.CoordinateSweeps.OrdinaryTensor.fiberPermEquiv line 53

   Source comment

   Word-preserving permutations and independent permutations of its fibers are literally equivalent finite sets. This yields the factorial frame moments.

   def fiberPermEquiv (w : I → A) :
       {σ : Equiv.Perm I // ∀ i, w (σ i) = w i} ≃ (∀ a : A, Equiv.Perm {i : I // w i = a}) where
   …

   Mentions: OAI.CoordinateSweeps.a

8. lemma OAI.CoordinateSweeps.OrdinaryTensor.card_wordStabilizer line 69
9. def OAI.CoordinateSweeps.OrdinaryTensor.transporterEquiv line 76

   Source comment

   A transporter fiber is a coset of the literal word stabilizer.

   def transporterEquiv (u w : I → A) (σ : Equiv.Perm I) (hσ : permute σ u = w) :
       {g : Equiv.Perm I // permute g u = w} ≃
         {g : Equiv.Perm I // ∀ i, u (g i) = u i} where
   …

   Mentions: OAI.CoordinateSweeps.OrdinaryTensor.permute

10. lemma OAI.CoordinateSweeps.OrdinaryTensor.permute_count line 95
11. lemma OAI.CoordinateSweeps.OrdinaryTensor.card_transporter line 104
12. def OAI.CoordinateSweeps.OrdinaryTensor.momentFrame line 116

    Source comment

    The finite moment matrix which will be realized by actual radial Gamma variables and root phases rather than an assumed de Finetti density.

    def momentFrame : Matrix (I → A) (I → A) ℂ := fun u w =>
    …

13. lemma OAI.CoordinateSweeps.OrdinaryTensor.momentFrame_eq_perm_sum line 119
14. lemma OAI.CoordinateSweeps.OrdinaryTensor.factorial_step_upper line 135

    Source comment

    A factorial ratio is bounded by the largest factor; used to avoid any assumed entropy/Stirling estimate in the empirical postselection measure.

    lemma factorial_step_upper (t k : ℕ) : (t+k).factorial ≤ t.factorial * (t+k)^k := by
    …

15. lemma OAI.CoordinateSweeps.OrdinaryTensor.factorial_mode line 148

    Source comment

    For any integral Poisson mean n, n is a mode. This elementary exact inequality is the only numerical ingredient for the finite tensor mixture.

    lemma factorial_mode (n t : ℕ) : n^t * n.factorial ≤ n^n * t.factorial := by
    …

16. lemma OAI.CoordinateSweeps.OrdinaryTensor.prod_word_eq_counts line 164
17. def OAI.CoordinateSweeps.OrdinaryTensor.orbitFiberEquiv line 170

    Source comment

    Exact sigma decomposition of a word orbit and its transporter fibers.

    def orbitFiberEquiv (u : I → A) :
        (Σ w : {w : I → A // count w = count u}, {σ : Equiv.Perm I // permute σ u = w.val}) ≃
          Equiv.Perm I where
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.count, OAI.CoordinateSweeps.OrdinaryTensor.permute

18. lemma OAI.CoordinateSweeps.OrdinaryTensor.orbit_card_mul_factorials line 182
19. abbrev OAI.CoordinateSweeps.OrdinaryTensor.Histogram line 198

    Source comment

    Histogram space is an actual finite set of attained occupancies.

    abbrev Histogram (I A : Type*) [Fintype I] [Fintype A] [DecidableEq A] :=
    …

20. instance OAI.CoordinateSweeps.OrdinaryTensor.(instance at line 201) line 201
21. instance OAI.CoordinateSweeps.OrdinaryTensor.(instance at line 202) line 202
22. def OAI.CoordinateSweeps.OrdinaryTensor.histogram line 204
23. lemma OAI.CoordinateSweeps.OrdinaryTensor.histogram_surjective line 207
24. lemma OAI.CoordinateSweeps.OrdinaryTensor.histogram_card_le line 212
25. def OAI.CoordinateSweeps.OrdinaryTensor.typeWeight line 223

    Source comment

    The individual multinomial type of a word, evaluated at any integer weights.

    def typeWeight (r : A → ℕ) (u : I → A) : ℕ :=
    …

26. lemma OAI.CoordinateSweeps.OrdinaryTensor.typeWeight_mul_factorials line 226
27. lemma OAI.CoordinateSweeps.OrdinaryTensor.typeWeight_empirical_max line 232

    Source comment

    Empirical occupancies maximize their own exact multinomial type weight.

    lemma typeWeight_empirical_max (u w : I → A) : typeWeight (count u) w ≤ typeWeight (count u) u := by
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.typeWeight, OAI.CoordinateSweeps.OrdinaryTensor.count

28. def OAI.CoordinateSweeps.OrdinaryTensor.histogramWeight line 251

    Source comment

    Type weight on the finite, attained histogram space.

    def histogramWeight (r : A → ℕ) (h : Histogram I A) : ℕ :=
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.Histogram

29. lemma OAI.CoordinateSweeps.OrdinaryTensor.histogramWeight_mk line 254
30. lemma OAI.CoordinateSweeps.OrdinaryTensor.sum_histogramWeight line 264
31. theorem OAI.CoordinateSweeps.OrdinaryTensor.empirical_type_mass line 281

    Source comment

    Exact polynomial empirical multinomial lower bound. It includes zero occupancies and avoids Stirling errors and asymptotic hypotheses.

    theorem empirical_type_mass (u : I → A) :
        (Fintype.card I)^Fintype.card I ≤
          (Fintype.card I+1)^Fintype.card A * typeWeight (count u) u := by
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.typeWeight, OAI.CoordinateSweeps.OrdinaryTensor.count

32. abbrev OAI.CoordinateSweeps.OrdinaryTensor.PhaseSpace line 305

    Source comment

    Finite independent root phases. The modulus is strictly larger than any occupancy, so it distinguishes every histogram without an analytic limit.

    abbrev PhaseSpace (I A : Type*) [Fintype I] := A → ZMod (Fintype.card I+1)

33. def OAI.CoordinateSweeps.OrdinaryTensor.wordPhase line 307
34. lemma OAI.CoordinateSweeps.OrdinaryTensor.wordPhase_eq_prod line 311
35. lemma OAI.CoordinateSweeps.OrdinaryTensor.phase_conjugate_sum line 321
36. lemma OAI.CoordinateSweeps.OrdinaryTensor.wordPhase_orthogonality line 347
37. lemma OAI.CoordinateSweeps.OrdinaryTensor.wordPhase_star_mul line 354
38. def OAI.CoordinateSweeps.OrdinaryTensor.tensorVector line 368
39. def OAI.CoordinateSweeps.OrdinaryTensor.outer line 369
40. lemma OAI.CoordinateSweeps.OrdinaryTensor.outer_posSemidef line 371
41. lemma OAI.CoordinateSweeps.OrdinaryTensor.outer_apply line 374
42. def OAI.CoordinateSweeps.OrdinaryTensor.empiricalVector line 378

    Source comment

    Empirical-site amplitudes. Their exact squared norm is one when there is at least one slot. Zero-count letters are allowed and have zero amplitude.

    def empiricalVector (h : Histogram I A) (t : PhaseSpace I A) (a : A) : ℂ :=
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.Histogram, OAI.CoordinateSweeps.OrdinaryTensor.PhaseSpace, OAI.CoordinateSweeps.a

43. def OAI.CoordinateSweeps.OrdinaryTensor.amplitude line 381
44. lemma OAI.CoordinateSweeps.OrdinaryTensor.char_star_mul line 385
45. lemma OAI.CoordinateSweeps.OrdinaryTensor.empiricalVector_square line 391
46. lemma OAI.CoordinateSweeps.OrdinaryTensor.empiricalVector_unit line 404
47. lemma OAI.CoordinateSweeps.OrdinaryTensor.amplitude_eq_counts line 413
48. lemma OAI.CoordinateSweeps.OrdinaryTensor.amplitude_congr line 420
49. lemma OAI.CoordinateSweeps.OrdinaryTensor.tensorVector_empirical line 424
50. lemma OAI.CoordinateSweeps.OrdinaryTensor.amplitude_square line 430
51. def OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame line 439

    Source comment

    Finite phase average of actual pure product states.

    def phaseFrame (h : Histogram I A) : Matrix (I → A) (I → A) ℂ :=
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.Histogram

52. lemma OAI.CoordinateSweeps.OrdinaryTensor.phaseSpace_card_pos line 444
53. lemma OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame_posSemidef line 449
54. lemma OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame_entry line 455
55. def OAI.CoordinateSweeps.OrdinaryTensor.orbitSize line 477
56. def OAI.CoordinateSweeps.OrdinaryTensor.representative line 478
57. lemma OAI.CoordinateSweeps.OrdinaryTensor.count_representative line 481
58. lemma OAI.CoordinateSweeps.OrdinaryTensor.histogram_representative line 484
59. lemma OAI.CoordinateSweeps.OrdinaryTensor.orbitSize_pos line 487
60. lemma OAI.CoordinateSweeps.OrdinaryTensor.orbitSize_mk line 491
61. def OAI.CoordinateSweeps.OrdinaryTensor.block line 496
62. lemma OAI.CoordinateSweeps.OrdinaryTensor.block_posSemidef line 500
63. lemma OAI.CoordinateSweeps.OrdinaryTensor.block_entry line 503
64. def OAI.CoordinateSweeps.OrdinaryTensor.symProjector line 510

    Source comment

    Orthogonal projection onto vectors invariant under ordinary slot permutations, implemented by their exact histogram blocks.

    def symProjector : Matrix (I → A) (I → A) ℂ :=
    …

65. lemma OAI.CoordinateSweeps.OrdinaryTensor.symProjector_posSemidef line 513
66. lemma OAI.CoordinateSweeps.OrdinaryTensor.symProjector_entry line 518
67. lemma OAI.CoordinateSweeps.OrdinaryTensor.symProjector_mulVec_of_constant line 528
68. lemma OAI.CoordinateSweeps.OrdinaryTensor.symProjector_idempotent line 549
69. def OAI.CoordinateSweeps.OrdinaryTensor.histogramAmplitude line 556
70. lemma OAI.CoordinateSweeps.OrdinaryTensor.histogramAmplitude_mk line 559
71. lemma OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame_blocks line 565
72. lemma OAI.CoordinateSweeps.OrdinaryTensor.inverse_orbit_le_empirical line 582

    Source comment

    Polynomial inverse-orbit bound for the **actual** empirical phase frame.

    lemma inverse_orbit_le_empirical (hn : 0 < Fintype.card I) (h : Histogram I A) :
        (orbitSize h : ℝ)⁻¹ ≤ ((Fintype.card I+1)^Fintype.card A : ℕ) * histogramAmplitude h h ^ 2 := by
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.Histogram, OAI.CoordinateSweeps.OrdinaryTensor.orbitSize, OAI.CoordinateSweeps.OrdinaryTensor.histogramAmplitude

73. lemma OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame_sum_blocks line 606
74. theorem OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame_sum_domination line 616

    Source comment

    Constructive finite postselection before normalizing the histogram sum.

    theorem phaseFrame_sum_domination (hn : 0 < Fintype.card I) :
        ((((Fintype.card I+1)^Fintype.card A : ℕ) : ℂ) •
          (∑ h : Histogram I A, phaseFrame h) - symProjector).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.Histogram, OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame, OAI.CoordinateSweeps.OrdinaryTensor.symProjector

75. instance OAI.CoordinateSweeps.OrdinaryTensor.(instance at line 643) line 643
76. def OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture line 647

    Source comment

    Literal finite average of empirical pure product tensors, grouped first by histogram and then by independent roots.

    def finiteMixture : Matrix (I → A) (I → A) ℂ :=
    …

77. lemma OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture_posSemidef line 651
78. theorem OAI.CoordinateSweeps.OrdinaryTensor.finite_postselection line 658

    Source comment

    Finite, normalized tensor postselection with explicit polynomial overhead. Every product in finiteMixture comes from squared-norm-one empirical vectors; there is no de Finetti theorem or independent density assumption.

    theorem finite_postselection [Nonempty A] (hn : 0 < Fintype.card I) :
        ((((Fintype.card I+1)^(2*Fintype.card A) : ℕ) : ℂ) •
          (finiteMixture (I := I) (A := A)) - symProjector).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture, OAI.CoordinateSweeps.OrdinaryTensor.symProjector

79. lemma OAI.CoordinateSweeps.OrdinaryTensor.outer_tensorVector_trace line 684
80. lemma OAI.CoordinateSweeps.OrdinaryTensor.phaseFrame_trace line 694
81. lemma OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture_trace line 701
82. lemma OAI.CoordinateSweeps.OrdinaryTensor.outer_trace_nonneg line 718
83. theorem OAI.CoordinateSweeps.OrdinaryTensor.invariant_vector_postselection line 723

    Source comment

    The ordinary finite postselection theorem applied to an actual invariant purification vector, rather than an assumed projection inequality.

    theorem invariant_vector_postselection [Nonempty A] (hn : 0 < Fintype.card I)
        (v : (I → A) → ℂ) (hv : ∀ σ : Equiv.Perm I, ∀ w, v (permute σ w) = v w) :
        ((Matrix.trace (outer v) * ((Fintype.card I+1 : ℕ) : ℂ)^(2*Fintype.card A)) •
          finiteMixture - outer v).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.OrdinaryTensor.permute, OAI.CoordinateSweeps.OrdinaryTensor.outer, OAI.CoordinateSweeps.OrdinaryTensor.finiteMixture

84. def OAI.CoordinateSweeps.OrdinaryTensor.rawMixture line 748
85. lemma OAI.CoordinateSweeps.OrdinaryTensor.rawMixture_posSemidef line 751
86. lemma OAI.CoordinateSweeps.OrdinaryTensor.rawMixture_eq line 754
87. lemma OAI.CoordinateSweeps.OrdinaryTensor.rawMixture_domination line 767