OAI/RepresentationTheory/SignedTensor/Blocks.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoordinateSweeps.SignedTensor.finite_block_density_domination line 24

   Source comment

   Tensorization of finite density domination, preserving finite probability normalization and the exact product of local dimensions.

   theorem finite_block_density_domination (s p : ℕ) (hp : 0 < p) (hps : p ≤ s)
       (l : B → ℕ) (hl : ∀ i, l i ≤ s) (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (l i)))) :
       ∃ (K : Type) (_ : Fintype K) (_ : Nonempty K) (r : K → B → EvenDensity p),
         (((∏ i, ((ρ i).dimension : ℂ))*((s+1 : ℕ) : ℂ)^(Fintype.card B*(41*p^2))) •
           ((Fintype.card K : ℂ)⁻¹ • ∑ x, DependentTensor.tensor (fun i => densityPower (l i) (r x i).val))-
             DependentTensor.tensor (fun i => isotypic (p := p) (ρ i))).PosSemidef := by
   …

   Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.DependentTensor.tensor, OAI.CoordinateSweeps.SignedTensor.densityPower, OAI.CoordinateSweeps.SignedTensor.isotypic

2. def OAI.CoordinateSweeps.OrderedBlocks.offset line 63
3. lemma OAI.CoordinateSweeps.OrderedBlocks.offset_next_le line 65
4. lemma OAI.CoordinateSweeps.OrderedBlocks.offset_next_le_total line 72
5. def OAI.CoordinateSweeps.OrderedBlocks.encode line 78
6. lemma OAI.CoordinateSweeps.OrderedBlocks.encode_lt_of_block line 81
7. lemma OAI.CoordinateSweeps.OrderedBlocks.encode_lt_same line 88
8. lemma OAI.CoordinateSweeps.OrderedBlocks.encode_injective line 93
9. def OAI.CoordinateSweeps.OrderedBlocks.positions line 106

   Source comment

   Explicit contiguous coordinate chart, including zero-length blocks.

   def positions : ((i : Fin r) × Fin (n i)) ≃ Fin (∑ i, n i) :=
   …

10. lemma OAI.CoordinateSweeps.OrderedBlocks.positions_apply line 110
11. lemma OAI.CoordinateSweeps.OrderedBlocks.positions_lt_of_block line 112
12. lemma OAI.CoordinateSweeps.OrderedBlocks.positions_lt_same line 115
13. def OAI.CoordinateSweeps.OrderedBlocks.perm line 118
14. lemma OAI.CoordinateSweeps.OrderedBlocks.perm_apply line 121
15. lemma OAI.CoordinateSweeps.OrderedBlocks.perm_inv line 125
16. def OAI.CoordinateSweeps.OrderedBlocks.permHom line 133
17. lemma OAI.CoordinateSweeps.SignedTensor.phase_double_prod line 148
18. def OAI.CoordinateSweeps.SignedTensor.blockPerm line 161
19. lemma OAI.CoordinateSweeps.SignedTensor.blockPerm_left line 164
20. lemma OAI.CoordinateSweeps.SignedTensor.blockPerm_right line 168
21. lemma OAI.CoordinateSweeps.SignedTensor.blockPerm_inv line 172
22. lemma OAI.CoordinateSweeps.SignedTensor.phase_blockPerm line 179
23. def OAI.CoordinateSweeps.SignedTensor.splitWord line 197

    Source comment

    The explicit unitary reindexing between a concatenated tensor word and its two block words. The Koszul signs are retained in phase_blockPerm.

    def splitWord (p m n : ℕ) : Word p (m+n) ≃ Word p m × Word p n where
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

24. lemma OAI.CoordinateSweeps.SignedTensor.splitWord_wordPerm line 203
25. def OAI.CoordinateSweeps.SignedTensor.blockMatrix line 209
26. theorem OAI.CoordinateSweeps.SignedTensor.matrix_blockPerm line 215

    Source comment

    Exact block multiplicativity of the signed permutation action.

    theorem matrix_blockPerm {p m n : ℕ} (σ : Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin n)) :
        matrix (p := p) (blockPerm σ τ)=blockMatrix (matrix σ) (matrix τ) := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.matrix, OAI.CoordinateSweeps.SignedTensor.blockPerm, OAI.CoordinateSweeps.SignedTensor.blockMatrix

27. lemma OAI.CoordinateSweeps.SignedTensor.prod_positions line 231
28. lemma OAI.CoordinateSweeps.SignedTensor.phase_grouped line 235
29. def OAI.CoordinateSweeps.SignedTensor.groupWord line 259
30. lemma OAI.CoordinateSweeps.SignedTensor.groupWord_wordPerm line 268
31. theorem OAI.CoordinateSweeps.SignedTensor.matrix_grouped line 274

    Source comment

    Genuine product-subgroup action, with no suppressed Koszul signs.

    theorem matrix_grouped (σ : ∀ i, Equiv.Perm (Fin (n i))) :
        matrix (p := p) (perm n σ)=
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.matrix

32. def OAI.CoordinateSweeps.SignedTensor.groupedAverage line 305

    Source comment

    The subgroup operator is an actual group-algebra average on the full set of slots, not an operator posited to factor.

    def groupedAverage {Ω : Fin r → Type*} [∀ i, Fintype (Ω i)]
        (w : ∀ i, Ω i → ℂ) (g : ∀ i, Ω i → Equiv.Perm (Fin (n i))) :
        Matrix (Word p (∑ i, n i)) (Word p (∑ i, n i)) ℂ :=
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

33. lemma OAI.CoordinateSweeps.SignedTensor.groupedAverage_factor line 311
34. def OAI.CoordinateSweeps.SignedTensor.groupedProjector line 334
35. lemma OAI.CoordinateSweeps.SignedTensor.groupedProjector_factor line 338
36. lemma OAI.CoordinateSweeps.SignedTensor.matrix_trace_reindex line 344
37. lemma OAI.CoordinateSweeps.SignedTensor.reindex_moment line 348
38. theorem OAI.CoordinateSweeps.SignedTensor.grouped_projected_moment line 359

    Source comment

    Exact isotypic child moment factorization, including the true Hom multiplicities and all zero-length blocks.

    theorem grouped_projected_moment {Ω : Fin r → Type*} [∀ i, Fintype (Ω i)]
        (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (n i))))
        (w : ∀ i, Ω i → ℂ) (g : ∀ i, Ω i → Equiv.Perm (Fin (n i)))
        {q : ℕ} (hq : q ≠ 0) :
        Matrix.trace (((groupedProjector (p := p) n ρ*groupedAverage n w g).conjTranspose*
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.groupedProjector, OAI.CoordinateSweeps.SignedTensor.groupedAverage

39. def OAI.CoordinateSweeps.SignedTensor.IsEven line 383
40. def OAI.CoordinateSweeps.SignedTensor.grading line 386
41. lemma OAI.CoordinateSweeps.SignedTensor.isEven_iff_commute line 389
42. lemma OAI.CoordinateSweeps.SignedTensor.isEven_add line 412
43. lemma OAI.CoordinateSweeps.SignedTensor.isEven_smul line 415
44. lemma OAI.CoordinateSweeps.SignedTensor.isEven_sum line 418
45. lemma OAI.CoordinateSweeps.SignedTensor.isEven_one line 424
46. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_commute_of_even line 431
47. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_commute_lift line 459
48. theorem OAI.CoordinateSweeps.SignedTensor.exists_even_whitening line 469

    Source comment

    Constructed even whitening of the regularized empirical row density.

    theorem exists_even_whitening {R : Type*} [Fintype R] [Nonempty R]
        (r : R → EvenDensity p) {ε : ℝ} (hε : 0 < ε) :
        let B := (Fintype.card R : ℂ)⁻¹ • ∑ i, (r i).val + (ε : ℂ) • (1 : Matrix (Letter p) (Letter p) ℂ)
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.SignedTensor.Letter

49. lemma OAI.CoordinateSweeps.SignedTensor.tensor_covariance line 496

    Source comment

    Even inhomogeneous site tensors transform by the *signed* permutation matrix with no residual phase. This is what permits regrouping deleted rows and columns without identifying the two Koszul charts by an unsigned map.

    lemma tensor_covariance (A : Fin l → Matrix (Letter p) (Letter p) ℂ)
        (hA : ∀ i, IsEven (A i)) (σ : Equiv.Perm (Fin l)) :
        matrix σ*TensorBoard.tensor A=
          TensorBoard.tensor (fun i => A (σ⁻¹ i))*matrix σ := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Letter, OAI.CoordinateSweeps.SignedTensor.IsEven, OAI.CoordinateSweeps.SignedTensor.matrix, OAI.CoordinateSweeps.TensorBoard.tensor

50. lemma OAI.CoordinateSweeps.SignedTensor.tensor_signed_conjugate line 527
51. def OAI.CoordinateSweeps.SignedTensor.groupedSite line 539
52. lemma OAI.CoordinateSweeps.SignedTensor.grouped_densityPower line 542
53. theorem OAI.CoordinateSweeps.SignedTensor.finite_grouped_density_domination line 557

    Source comment

    Literal contiguous-block projectors are dominated by independent finite mixtures of even site densities, with all local dimension factors.

    theorem finite_grouped_density_domination (s : ℕ) (hp : 0 < p) (hps : p ≤ s)
        (hn : ∀ i, n i ≤ s) (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (n i)))) :
        ∃ (K : Type) (_ : Fintype K) (_ : Nonempty K) (a : K → Fin r → EvenDensity p),
          (((∏ i, ((ρ i).dimension : ℂ))*((s+1 : ℕ) : ℂ)^(r*(41*p^2))) •
            ((Fintype.card K : ℂ)⁻¹ • ∑ x,
              TensorBoard.tensor (fun k => (groupedSite n (a x) k).val))-
              groupedProjector (p := p) n ρ).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.TensorBoard.tensor, OAI.CoordinateSweeps.SignedTensor.groupedSite, OAI.CoordinateSweeps.SignedTensor.groupedProjector

54. theorem OAI.CoordinateSweeps.SignedTensor.finite_regrouped_density_domination line 585

    Source comment

    The same domination after an arbitrary *signed* change of slot chart.

    theorem finite_regrouped_density_domination (s : ℕ) (hp : 0 < p) (hps : p ≤ s)
        (hn : ∀ i, n i ≤ s) (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (n i))))
        (σ : Equiv.Perm (Fin (∑ i, n i))) :
        ∃ (K : Type) (_ : Fintype K) (_ : Nonempty K) (a : K → Fin r → EvenDensity p),
          (((∏ i, ((ρ i).dimension : ℂ))*((s+1 : ℕ) : ℂ)^(r*(41*p^2))) •
            ((Fintype.card K : ℂ)⁻¹ • ∑ x,
              TensorBoard.tensor (fun k => (groupedSite n (a x) (σ⁻¹ k)).val))-
              matrix σ*groupedProjector (p := p) n ρ*(matrix σ).conjTranspose).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.TensorBoard.tensor, OAI.CoordinateSweeps.SignedTensor.groupedSite, OAI.CoordinateSweeps.SignedTensor.matrix, OAI.CoordinateSweeps.SignedTensor.groupedProjector

55. lemma OAI.CoordinateSweeps.SignedTensor.groupedProjector_posSemidef line 609
56. lemma OAI.CoordinateSweeps.SignedTensor.groupedProjector_idempotent line 615
57. def OAI.CoordinateSweeps.SignedTensor.lengthMatrix line 629
58. def OAI.CoordinateSweeps.SignedTensor.ambientProjector line 632
59. def OAI.CoordinateSweeps.SignedTensor.ambientProjectorAlgebra line 636
60. lemma OAI.CoordinateSweeps.SignedTensor.ambientProjectorAlgebra_lift line 641
61. lemma OAI.CoordinateSweeps.SignedTensor.ambientProjector_posSemidef line 655
62. lemma OAI.CoordinateSweeps.SignedTensor.ambientProjector_idempotent line 661
63. theorem OAI.CoordinateSweeps.SignedTensor.finite_ambient_density_domination line 672

    Source comment

    Actual ambient projectors, not hypothesized density mixtures.

    theorem finite_ambient_density_domination (s : ℕ) (hp : 0 < p) (hps : p ≤ s)
        (hn : ∀ i, n i ≤ s) (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (n i))))
        (h : (∑ i, n i)=l) (σ : Equiv.Perm (Fin l)) :
        ∃ (K : Type) (_ : Fintype K) (_ : Nonempty K) (a : K → Fin r → EvenDensity p),
          (((∏ i, ((ρ i).dimension : ℂ))*((s+1 : ℕ) : ℂ)^(r*(41*p^2))) •
            ((Fintype.card K : ℂ)⁻¹ • ∑ x,
              TensorBoard.tensor (fun k => (groupedSite n (a x) ((finCongr h).symm (σ⁻¹ k))).val))-
              ambientProjector (p := p) n h σ ρ).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.TensorBoard.tensor, OAI.CoordinateSweeps.SignedTensor.groupedSite, OAI.CoordinateSweeps.SignedTensor.ambientProjector

64. def OAI.CoordinateSweeps.SignedTensor.ambientAverage line 690
65. lemma OAI.CoordinateSweeps.SignedTensor.ambientAverage_factor line 697
66. lemma OAI.CoordinateSweeps.SignedTensor.matrix_unitary_reverse line 712
67. lemma OAI.CoordinateSweeps.SignedTensor.conjugate_mul line 716
68. lemma OAI.CoordinateSweeps.SignedTensor.conjugate_pow line 723
69. lemma OAI.CoordinateSweeps.SignedTensor.conjugate_moment line 730
70. theorem OAI.CoordinateSweeps.SignedTensor.ambient_projected_moment line 741

    Source comment

    The child moment formula survives the literal slot chart, with actual Hom multiplicities.

    theorem ambient_projected_moment (h : (∑ i, n i)=l) (σ : Equiv.Perm (Fin l))
        {Ω : Fin r → Type*} [∀ i, Fintype (Ω i)]
        (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (n i))))
        (w : ∀ i, Ω i → ℂ) (g : ∀ i, Ω i → Equiv.Perm (Fin (n i)))
        {q : ℕ} (hq : q ≠ 0) :
        Matrix.trace (((ambientProjector (p := p) n h σ ρ*ambientAverage n h σ w g).conjTranspose*
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.ambientProjector, OAI.CoordinateSweeps.SignedTensor.ambientAverage

71. def OAI.CoordinateSweeps.FiberBlocks.size line 775
72. def OAI.CoordinateSweeps.FiberBlocks.cards line 776
73. def OAI.CoordinateSweeps.FiberBlocks.slots line 779

    Source comment

    Contiguous finite label fibers give a genuine ordered slot chart.

    def slots : Fin (∑ i, size f i) ≃ L :=
    …

    Mentions: OAI.CoordinateSweeps.FiberBlocks.size

74. lemma OAI.CoordinateSweeps.FiberBlocks.total line 783
75. lemma OAI.CoordinateSweeps.FiberBlocks.label_slots line 786
76. def OAI.CoordinateSweeps.FiberBlocks.chart line 791

    Source comment

    The same chart with the literal cardinal as ambient length.

    def chart : Fin (Fintype.card L) ≃ L :=
    …

77. def OAI.CoordinateSweeps.FiberBlocks.regroup line 795

    Source comment

    Permutation changing the contiguous fiber chart to any given ambient chart.

    def regroup (e : Fin (Fintype.card L) ≃ L) : Equiv.Perm (Fin (Fintype.card L)) :=
    …

    Mentions: OAI.CoordinateSweeps.e

78. lemma OAI.CoordinateSweeps.FiberBlocks.label_regroup line 798
79. lemma OAI.CoordinateSweeps.FiberBlocks.slots_positions line 811
80. def OAI.CoordinateSweeps.FiberBlocks.action line 816

    Source comment

    Independent permutations of the actual fibers, on the literal ambient set.

    def action : (∀ i, Equiv.Perm (Fin (size f i))) →* Equiv.Perm L :=
    …

    Mentions: OAI.CoordinateSweeps.FiberBlocks.size

81. lemma OAI.CoordinateSweeps.FiberBlocks.action_apply line 819
82. lemma OAI.CoordinateSweeps.FiberBlocks.ambient_action line 825
83. def OAI.CoordinateSweeps.FiberBlocks.restrict line 837

    Source comment

    A label-preserving permutation has genuine induced local permutations.

    def restrict (σ : Equiv.Perm L) (hσ : ∀ x, f (σ x)=f x) (i : Fin r) : Equiv.Perm (Fin (size f i)) :=
    …

    Mentions: OAI.CoordinateSweeps.FiberBlocks.size

84. lemma OAI.CoordinateSweeps.FiberBlocks.restrict_apply line 843
85. lemma OAI.CoordinateSweeps.FiberBlocks.action_restrict line 848
86. lemma OAI.CoordinateSweeps.SignedTensor.groupedProjector_commute_average line 861
87. lemma OAI.CoordinateSweeps.SignedTensor.ambientProjector_commute_average line 879
88. lemma OAI.CoordinateSweeps.SignedTensor.child_product_bound line 895
89. def OAI.CoordinateSweeps.SignedTensor.fiberProjector line 918
90. def OAI.CoordinateSweeps.SignedTensor.fiberProjectorAlgebra line 922
91. lemma OAI.CoordinateSweeps.SignedTensor.fiberProjectorAlgebra_lift line 926
92. lemma OAI.CoordinateSweeps.SignedTensor.fiberProjector_posSemidef line 931
93. lemma OAI.CoordinateSweeps.SignedTensor.fiberProjector_idempotent line 935
94. theorem OAI.CoordinateSweeps.SignedTensor.finite_fiber_density_domination line 941

    Source comment

    Exact regrouping connects local isotypic products to the literal site labels.

    theorem finite_fiber_density_domination (e : Fin (Fintype.card L) ≃ L)
        (s : ℕ) (hp : 0 < p) (hps : p ≤ s) (hn : ∀ i, FiberBlocks.size f i ≤ s)
        (ρ : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (FiberBlocks.size f i)))) :
        ∃ (K : Type) (_ : Fintype K) (_ : Nonempty K) (a : K → Fin r → EvenDensity p),
          (((∏ i, ((ρ i).dimension : ℂ))*((s+1 : ℕ) : ℂ)^(r*(41*p^2))) •
            ((Fintype.card K : ℂ)⁻¹ • ∑ x,
              TensorBoard.tensor (fun k => (a x (f (e k))).val))-fiberProjector (p := p) f e ρ).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.FiberBlocks.size, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.TensorBoard.tensor, OAI.CoordinateSweeps.SignedTensor.fiberProjector