OAI/Geometry/HarmonicGrowth/PolynomialControl.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.Control.derivative_mem_submodule line 15
2. lemma OAI.HarmonicCounterexample.Control.conjugation_derivative line 23
3. theorem OAI.HarmonicCounterexample.Control.bracket_mem_of_conjugation line 33

   Source documentation

   Differentiating a genuine conjugation orbit in a finite-dimensional Lie subalgebra proves its infinitesimal normalizer property. No Fourier integral or unproved representation-theoretic closure is substituted.

   theorem bracket_mem_of_conjugation [FiniteDimensional ℝ A]
       (L : Submodule ℝ A) {g h : ℝ → A} {z : A}
       (hg : HasDerivAt g z 0) (hh : HasDerivAt h (-z) 0)
       (hg0 : g 0 = 1) (hh0 : h 0 = 1)
       (hconj : ∀ t X,X ∈ L → g t*X*h t ∈ L) {X : A} (hX : X ∈ L) : (z*X-X*z) ∈ L :=
   …

4. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.exp_neg_mul_self line 48
5. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.exp_mul_neg_self line 51
6. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.exp_skew_transpose line 54
7. def OAI.HarmonicCounterexample.Berger.ComplexStructure.rotate line 59

   Source documentation

   An actual smooth orbit of orthogonal complex structures under any skew infinitesimal rotation; both orientation classes remain available.

   def rotate (J : ComplexStructure ι) (R : Matrix ι ι ℝ) (hR : Rᵀ = -R) (t : ℝ) :
       ComplexStructure ι where
   …

   Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

8. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.rotate_zero line 82
9. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.rotate_hasDerivAt_zero line 86
10. def OAI.HarmonicCounterexample.Control.traceFree line 107
11. lemma OAI.HarmonicCounterexample.Control.four_square_polarization line 113
12. lemma OAI.HarmonicCounterexample.Control.mixed_product_mem line 119

    Source documentation

    Four sign choices already extract each mixed plane product: no exponential Walsh sum needs to be computed inside the kernel. Trace subtraction is exact.

    lemma mixed_product_mem [CharZero 𝕜] (L : LieSubalgebra 𝕜 (Matrix ι ι 𝕜))
        (H X Y : Matrix ι ι 𝕜) (hXY : Commute X Y)
        (h0 : traceFree (H*H) ∈ L)
        (hi : traceFree ((H-2*X)*(H-2*X)) ∈ L)
        (hj : traceFree ((H-2*Y)*(H-2*Y)) ∈ L)
        (hij : traceFree ((H-2*X-2*Y)*(H-2*X-2*Y)) ∈ L) :
        traceFree (X*Y) ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.traceFree

13. lemma OAI.HarmonicCounterexample.Control.traceFree_commutator line 158
14. lemma OAI.HarmonicCounterexample.Control.commutator_traceFree line 163
15. lemma OAI.HarmonicCounterexample.Control.square_generator_normalizer line 173

    Source documentation

    The actual rotation curve makes every skew angular field an infinitesimal normalizer of the squared-complex-structure generators. The anti-representation hypothesis is an ordinary algebraic compatibility, proved for actual polynomial fields in linearField_bracket; no Lie-generation conclusion is assumed.

    lemma square_generator_normalizer
        (ρ : Matrix ι ι ℝ →ₗ[ℝ] Matrix κ κ ℝ)
        (hρ : ∀ M N,ρ (M*N-N*M) = ρ N*ρ M-ρ M*ρ N)
        (L : LieSubalgebra ℝ (Matrix κ κ ℝ))
        (hgen : ∀ J : ComplexStructure ι,traceFree (ρ J.matrix*ρ J.matrix) ∈ L)
        (R : Matrix ι ι ℝ) (hR : Rᵀ = -R) (J : ComplexStructure ι) :
        ⁅ρ R,traceFree (ρ J.matrix*ρ J.matrix)⁆ ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.traceFree

16. lemma OAI.HarmonicCounterexample.Control.normalizer_lieSpan line 215

    Source documentation

    Normalizer membership on generators propagates through the genuine Lie span by Jacobi. This is the closure step needed for torus weight filtering.

    lemma normalizer_lieSpan {𝕜 A : Type*} [Field 𝕜] [LieRing A] [LieAlgebra 𝕜 A]
        (s : Set A) (z : A)
        (hz : ∀ x ∈ s,⁅z,x⁆ ∈ LieSubalgebra.lieSpan 𝕜 A s) :
        ∀ x ∈ LieSubalgebra.lieSpan 𝕜 A s,⁅z,x⁆ ∈ LieSubalgebra.lieSpan 𝕜 A s := by
    …

17. lemma OAI.HarmonicCounterexample.Control.traceFree_commutator_complex line 239
18. lemma OAI.HarmonicCounterexample.Control.commutator_traceFree_complex line 244
19. lemma OAI.HarmonicCounterexample.Control.square_generator_normalizer_complex line 254

    Source documentation

    The actual rotation curve makes every skew angular field an infinitesimal normalizer of the squared-complex-structure generators. The anti-representation hypothesis is an ordinary algebraic compatibility, proved for actual polynomial fields in linearField_bracket; no Lie-generation conclusion is assumed.

    lemma square_generator_normalizer_complex
        (ρ : Matrix ι ι ℝ →ₗ[ℝ] Matrix κ κ ℂ)
        (hρ : ∀ M N,ρ (M*N-N*M) = ρ N*ρ M-ρ M*ρ N)
        (L : LieSubalgebra ℂ (Matrix κ κ ℂ))
        (hgen : ∀ J : ComplexStructure ι,traceFree (ρ J.matrix*ρ J.matrix) ∈ L)
        (R : Matrix ι ι ℝ) (hR : Rᵀ = -R) (J : ComplexStructure ι) :
        ⁅ρ R,traceFree (ρ J.matrix*ρ J.matrix)⁆ ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.traceFree

20. def OAI.HarmonicCounterexample.Berger.ComplexStructure.triple line 304

    Source documentation

    The manuscript's explicit three-plane complex structure: the disjoint coordinate swaps turn the standard pairs into (X_i,X_j), (Y_i,X_k), (Y_j,Y_k). It is an ACTUAL orthogonal complex structure, with no matrix equations assumed.

    def triple (i j k : Fin s) : ComplexStructure (Fin s ⊕ Fin s) :=
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

21. def OAI.HarmonicCounterexample.Berger.ComplexStructure.coordinateSign line 308
22. def OAI.HarmonicCounterexample.Berger.ComplexStructure.coordinatePlane line 309
23. def OAI.HarmonicCounterexample.Berger.ComplexStructure.signedIndex line 311
24. def OAI.HarmonicCounterexample.Berger.ComplexStructure.splitMatrix line 316

    Source documentation

    Pullback matrix in the independent complex coordinates x_i ± i y_i. This is the exact substitution x=(z+zbar)/2, y=(z-zbar)/(2i), not a spectral model replacing the real vector field.

    def splitMatrix (J : ComplexStructure (Fin s ⊕ Fin s)) :
        Matrix (Fin s ⊕ Fin s) (Fin s ⊕ Fin s) ℂ := fun a b =>
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

25. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.triple_split_ij line 323
26. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.triple_split_ik line 331
27. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.triple_split_ji line 340
28. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.triple_split_ki line 348
29. def OAI.HarmonicCounterexample.Berger.ComplexStructure.complexMatrix line 358

    Source documentation

    Complexification of the actual real coordinate matrix.

    def complexMatrix (J : ComplexStructure (Fin s ⊕ Fin s)) :
        Matrix (Fin s ⊕ Fin s) (Fin s ⊕ Fin s) ℂ := J.matrix.map Complex.ofReal

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

30. def OAI.HarmonicCounterexample.Berger.ComplexStructure.splitChange line 361
31. def OAI.HarmonicCounterexample.Berger.ComplexStructure.unsplitChange line 364
32. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.split_unsplit line 367
33. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.unsplit_split line 374
34. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitMatrix_eq line 381
35. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitMatrix_square line 390
36. def OAI.HarmonicCounterexample.Berger.ComplexStructure.torusMatrix line 405
37. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.torusMatrix_skew line 408
38. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.torusMatrix_square line 413
39. def OAI.HarmonicCounterexample.Berger.ComplexStructure.signedStructure line 423
40. def OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix line 431

    Source documentation

    Real-linear transformation of any actual coordinate field into the source's independent complex z/bar-z coordinates.

    def splitFieldMatrix : Matrix (Fin s ⊕ Fin s) (Fin s ⊕ Fin s) ℝ →ₗ[ℝ]
        Matrix (Fin s ⊕ Fin s) (Fin s ⊕ Fin s) ℂ where
    …

41. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_complex line 441
42. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_mul line 444
43. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_torus line 455
44. def OAI.HarmonicCounterexample.Control.linearField line 481

    Source documentation

    The actual infinitesimal linear coordinate motion, specified on generators.

    def linearField (M : Matrix ι ι 𝕜) : Derivation 𝕜 (MvPolynomial ι 𝕜) (MvPolynomial ι 𝕜) :=
    …

45. lemma OAI.HarmonicCounterexample.Control.linearField_X line 485
46. lemma OAI.HarmonicCounterexample.Control.linearField_add line 489
47. lemma OAI.HarmonicCounterexample.Control.linearField_smul line 495
48. lemma OAI.HarmonicCounterexample.Control.linearField_bracket line 503

    Source documentation

    Exact anti-representation identity for coordinate vector fields. The sign is important: fields act on functions by pullback.

    lemma linearField_bracket (M N : Matrix ι ι 𝕜) :
        ⁅linearField M,linearField N⁆ = linearField (N*M-M*N) := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.linearField

49. lemma OAI.HarmonicCounterexample.Control.derivation_sum_apply line 513
50. lemma OAI.HarmonicCounterexample.Control.linearField_apply line 521
51. def OAI.HarmonicCounterexample.Control.linearFieldMap line 530
52. lemma OAI.HarmonicCounterexample.Control.linearField_diagonal_monomial line 555
53. lemma OAI.HarmonicCounterexample.Control.linearField_square_first line 561
54. lemma OAI.HarmonicCounterexample.Control.linearField_square line 572

    Source documentation

    Exact second-order formula: there is no implicit harmonic projection and no omitted first-order term.

    lemma linearField_square (M : Matrix ι ι 𝕜) (P : MvPolynomial ι 𝕜) :
        linearField M (linearField M P) = linearField (M*M) P+
          ∑ i : ι,∑ j : ι,M i j • (X j*linearField M (pderiv i P)) := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.linearField

55. lemma OAI.HarmonicCounterexample.Control.linearField_neg_one line 582
56. lemma OAI.HarmonicCounterexample.Control.linearField_square_complex line 591
57. abbrev OAI.HarmonicCounterexample.Control.MonomialIndex line 597
58. instance OAI.HarmonicCounterexample.Control.monomialIndexFintype line 599
59. def OAI.HarmonicCounterexample.Control.homogeneousCoords line 612

    Source documentation

    Actual coefficient coordinates on homogeneous polynomials.

    def homogeneousCoords (l : ℕ) :
        homogeneousSubmodule ι 𝕜 l ≃ₗ[𝕜] MonomialIndex ι l →₀ 𝕜 :=
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex

60. def OAI.HarmonicCounterexample.Control.homogeneousBasis line 617
61. lemma OAI.HarmonicCounterexample.Control.homogeneousCoords_apply line 621
62. lemma OAI.HarmonicCounterexample.Control.homogeneousBasis_repr line 625
63. lemma OAI.HarmonicCounterexample.Control.homogeneousBasis_val line 629
64. lemma OAI.HarmonicCounterexample.Control.linearField_homogeneous line 643
65. def OAI.HarmonicCounterexample.Control.homogeneousField line 662
66. lemma OAI.HarmonicCounterexample.Control.homogeneousField_bracket line 668
67. def OAI.HarmonicCounterexample.Control.homogeneousFieldMap line 678

    Source documentation

    An actual finite-dimensional representation, in the actual monomial basis.

    def homogeneousFieldMap (l : ℕ) :
        Matrix ι ι 𝕜 →ₗ[𝕜] Module.End 𝕜 (homogeneousSubmodule ι 𝕜 l) where
    …

68. def OAI.HarmonicCounterexample.Control.homogeneousMatrix line 692
69. lemma OAI.HarmonicCounterexample.Control.homogeneousMatrix_apply line 697
70. lemma OAI.HarmonicCounterexample.Control.homogeneousMatrix_square_apply line 705
71. lemma OAI.HarmonicCounterexample.Control.homogeneousMatrix_bracket line 714
72. lemma OAI.HarmonicCounterexample.Control.homogeneousMatrix_diagonal line 728
73. def OAI.HarmonicCounterexample.Control.angularRepresentation line 744
74. lemma OAI.HarmonicCounterexample.Control.angularRepresentation_bracket line 749
75. def OAI.HarmonicCounterexample.Control.monomialWeight line 758
76. lemma OAI.HarmonicCounterexample.Control.angularRepresentation_torus line 761
77. lemma OAI.HarmonicCounterexample.Control.angularRepresentation_plane line 776
78. def OAI.HarmonicCounterexample.Control.angularLie line 810

    Source documentation

    The actual squared-complex-structure Lie algebra on homogeneous polynomials; the restriction to harmonic polynomials is taken later.

    def angularLie (l : ℕ) : LieSubalgebra ℂ
        (Matrix (MonomialIndex (Fin s ⊕ Fin s) l) (MonomialIndex (Fin s ⊕ Fin s) l) ℂ) :=
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex

79. lemma OAI.HarmonicCounterexample.Control.angularLie_generator line 815
80. lemma OAI.HarmonicCounterexample.Control.angularLie_normalizer line 819
81. lemma OAI.HarmonicCounterexample.Control.angularLie_weight_normalizer line 828
82. def OAI.HarmonicCounterexample.Control.torusRepresentation line 844

    Source documentation

    The torus field is real-linear in its plane velocities.

    def torusRepresentation (l : ℕ) : (Fin s → ℝ) →ₗ[ℝ]
        Matrix (MonomialIndex (Fin s ⊕ Fin s) l) (MonomialIndex (Fin s ⊕ Fin s) l) ℂ where
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex

83. lemma OAI.HarmonicCounterexample.Control.torusRepresentation_flip line 861
84. lemma OAI.HarmonicCounterexample.Control.angularLie_mixed_torus line 865
85. lemma OAI.HarmonicCounterexample.Control.angularLie_pair_weight line 900
86. lemma OAI.HarmonicCounterexample.Control.angularLie_pair_normalizer line 921