OAI/Geometry/HarmonicGrowth/Angular.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicCounterexample.Angular.PolynomialSpace line 10
2. def OAI.HarmonicCounterexample.Angular.polynomialLaplacian line 12
3. def OAI.HarmonicCounterexample.Angular.harmonicPolynomials line 15
4. lemma OAI.HarmonicCounterexample.Angular.pderiv_commute line 18
5. def OAI.HarmonicCounterexample.Angular.polynomialRotation line 32

   Source documentation

   Infinitesimal linear coordinate motion: (M x) · ∇.

   def polynomialRotation (M : Mat n) : PolynomialSpace n →ₗ[ℝ] PolynomialSpace n :=
   …

   Mentions: OAI.HarmonicCounterexample.Mat, OAI.HarmonicCounterexample.Angular.PolynomialSpace

6. lemma OAI.HarmonicCounterexample.Angular.polynomialRotation_apply line 36
7. lemma OAI.HarmonicCounterexample.Angular.polynomialRotation_homogeneous line 40
8. lemma OAI.HarmonicCounterexample.Angular.pderiv_rotation_term line 59
9. lemma OAI.HarmonicCounterexample.Angular.pderiv_rotation line 70
10. lemma OAI.HarmonicCounterexample.Angular.polynomialLaplacian_apply line 76
11. lemma OAI.HarmonicCounterexample.Angular.laplacian_rotation line 80
12. lemma OAI.HarmonicCounterexample.Angular.laplacian_rotation_skew line 96
13. instance OAI.HarmonicCounterexample.Angular.harmonicPolynomials_finite line 116
14. def OAI.HarmonicCounterexample.Angular.rotation line 122
15. def OAI.HarmonicCounterexample.Angular.factorialWeight line 146

    Source documentation

    Positive factorial monomial weights of the real Fischer form.

    def factorialWeight (d : Fin n →₀ ℕ) : ℝ := ∏ i : Fin n, (d i).factorial

16. lemma OAI.HarmonicCounterexample.Angular.factorialWeight_pos line 148
17. lemma OAI.HarmonicCounterexample.Angular.factorialWeight_add_single line 153
18. def OAI.HarmonicCounterexample.Angular.fischer line 169

    Source documentation

    Fischer bilinear form on the actual polynomial coefficient module.

    def fischer : MvPolynomial (Fin n) ℝ →ₗ[ℝ] MvPolynomial (Fin n) ℝ →ₗ[ℝ] ℝ :=
    …

19. lemma OAI.HarmonicCounterexample.Angular.fischer_monomial line 173
20. lemma OAI.HarmonicCounterexample.Angular.fischer_apply line 181
21. lemma OAI.HarmonicCounterexample.Angular.fischer_symm line 186
22. lemma OAI.HarmonicCounterexample.Angular.fischer_nonneg line 198
23. lemma OAI.HarmonicCounterexample.Angular.fischer_definite line 204
24. lemma OAI.HarmonicCounterexample.Angular.fischer_mul_X line 217
25. lemma OAI.HarmonicCounterexample.Angular.fischer_pderiv line 226
26. def OAI.HarmonicCounterexample.Angular.fischerCore line 236

    Source documentation

    The actual polynomial norm is positive definite, not a formal assumed round-space inner product. Its restriction is rotation invariant.

    def fischerCore (n : ℕ) : InnerProductSpace.Core ℝ (MvPolynomial (Fin n) ℝ) where
    …

27. instance OAI.HarmonicCounterexample.Angular.homogeneous_finite line 255
28. lemma OAI.HarmonicCounterexample.Angular.degree_eq_univ_sum line 258
29. lemma OAI.HarmonicCounterexample.Angular.homogeneous_finrank line 261
30. def OAI.HarmonicCounterexample.Angular.subFischer line 275

    Source documentation

    The Fischer duality on any actual polynomial subspace.

    def subFischer (U : Submodule ℝ (MvPolynomial (Fin n) ℝ)) : U →ₗ[ℝ] Module.Dual ℝ U :=
    …

31. lemma OAI.HarmonicCounterexample.Angular.subFischer_apply line 278
32. lemma OAI.HarmonicCounterexample.Angular.subFischer_injective line 281
33. lemma OAI.HarmonicCounterexample.Angular.subFischer_surjective line 290
34. def OAI.HarmonicCounterexample.Angular.quadraticRadius line 296

    Source documentation

    Squared Euclidean radius as an actual polynomial.

    def quadraticRadius (n : ℕ) : MvPolynomial (Fin n) ℝ := ∑ i : Fin n,X i^2

35. lemma OAI.HarmonicCounterexample.Angular.quadraticRadius_homogeneous line 298
36. lemma OAI.HarmonicCounterexample.Angular.quadraticRadius_ne_zero line 303
37. lemma OAI.HarmonicCounterexample.Angular.fischer_radius_laplacian line 309
38. def OAI.HarmonicCounterexample.Angular.radiusMultiply line 318

    Source documentation

    Radius multiplication between actual homogeneous parts.

    def radiusMultiply (n l : ℕ) : homogeneousSubmodule (Fin n) ℝ l →ₗ[ℝ]
        homogeneousSubmodule (Fin n) ℝ (l+2) where
    …

39. lemma OAI.HarmonicCounterexample.Angular.radiusMultiply_injective line 327
40. def OAI.HarmonicCounterexample.Angular.homogeneousLaplacian line 334

    Source documentation

    Restricted polynomial Laplacian, between the correct degree spaces.

    def homogeneousLaplacian (n l : ℕ) : homogeneousSubmodule (Fin n) ℝ (l+2) →ₗ[ℝ]
        homogeneousSubmodule (Fin n) ℝ l where
    …

41. lemma OAI.HarmonicCounterexample.Angular.homogeneousLaplacian_surjective line 348

    Source documentation

    The Laplacian is actually onto: the proof constructs its dual preimage from injective radius multiplication and positive Fischer duality.

    lemma homogeneousLaplacian_surjective (hn : 0 < n) (l : ℕ) :
        Function.Surjective (homogeneousLaplacian n l) := by
    …

    Mentions: OAI.HarmonicCounterexample.Angular.homogeneousLaplacian

42. def OAI.HarmonicCounterexample.Angular.harmonicKernelEquiv line 375

    Source documentation

    The kernel uses the actual polynomial Laplacian, not an abstract dimension count.

    def harmonicKernelEquiv (n l : ℕ) : LinearMap.ker (homogeneousLaplacian n l) ≃ₗ[ℝ]
        harmonicPolynomials n (l+2) where
    …

    Mentions: OAI.HarmonicCounterexample.Angular.homogeneousLaplacian, OAI.HarmonicCounterexample.Angular.harmonicPolynomials

43. lemma OAI.HarmonicCounterexample.Angular.harmonic_finrank_add line 392
44. lemma OAI.HarmonicCounterexample.Angular.harmonic_finrank_succ_succ line 401
45. lemma OAI.HarmonicCounterexample.Angular.harmonic_radius_multiple_zero line 409

    Source documentation

    Fischer decomposition obstruction: no nonzero harmonic polynomial is itself a multiple of the squared radius.

    lemma harmonic_radius_multiple_zero (P Q : PolynomialSpace n)
        (hP : polynomialLaplacian P = 0) (hQ : P = quadraticRadius n*Q) : P = 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.Angular.PolynomialSpace, OAI.HarmonicCounterexample.Angular.polynomialLaplacian, OAI.HarmonicCounterexample.Angular.quadraticRadius

46. lemma OAI.HarmonicCounterexample.Angular.pderiv_homogeneous_zero line 429
47. lemma OAI.HarmonicCounterexample.Angular.polynomialLaplacian_low line 434
48. lemma OAI.HarmonicCounterexample.Angular.harmonicPolynomials_low line 441
49. lemma OAI.HarmonicCounterexample.Angular.harmonic_finrank_zero line 448
50. lemma OAI.HarmonicCounterexample.Angular.harmonic_finrank_one line 452
51. lemma OAI.HarmonicCounterexample.Angular.homogeneous_components_independent line 457

    Source documentation

    A finite mixture of distinct homogeneous degrees has unique coefficients.

    lemma homogeneous_components_independent {ι : Type*} [Fintype ι] (d : ι → ℕ)
        (hd : Function.Injective d) (P : ι → PolynomialSpace n)
        (hP : ∀ i,(P i).IsHomogeneous (d i)) (hz : ∑ i,P i = 0) : ∀ i,P i = 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.Angular.PolynomialSpace

52. lemma OAI.HarmonicCounterexample.Angular.sum_harmonic_finrank line 481
53. lemma OAI.HarmonicCounterexample.Angular.fischer_rotation line 513

    Source documentation

    The infinitesimal rotation has its genuine Fischer adjoint.

    lemma fischer_rotation (M : Mat n) (P Q : PolynomialSpace n) :
        fischer (polynomialRotation M P) Q = fischer P (polynomialRotation M.transpose Q) := by
    …

    Mentions: OAI.HarmonicCounterexample.Mat, OAI.HarmonicCounterexample.Angular.PolynomialSpace, OAI.HarmonicCounterexample.Angular.fischer, OAI.HarmonicCounterexample.Angular.polynomialRotation

54. lemma OAI.HarmonicCounterexample.Angular.polynomialRotation_transpose_skew line 525
55. lemma OAI.HarmonicCounterexample.Angular.fischer_rotation_skew line 534
56. lemma OAI.HarmonicCounterexample.Angular.fischer_family_cauchy line 541

    Source documentation

    A sum of Fischer pairings satisfies Cauchy--Schwarz; this avoids introducing any assumed angular norm or a topological completion of the polynomial module.

    lemma fischer_family_cauchy {ι : Type*} [Fintype ι]
        (P Q : ι → PolynomialSpace n) :
        (∑ i,fischer (P i) (Q i))^2 ≤
          (∑ i,fischer (P i) (P i))*(∑ i,fischer (Q i) (Q i)) := by
    …

    Mentions: OAI.HarmonicCounterexample.Angular.PolynomialSpace, OAI.HarmonicCounterexample.Angular.fischer

57. lemma OAI.HarmonicCounterexample.Angular.fischer_gradient_energy line 560
58. lemma OAI.HarmonicCounterexample.Angular.fischer_gradient_orthogonal line 574

    Source documentation

    Orthogonal change of the gradient preserves its Fischer energy.

    lemma fischer_gradient_orthogonal (M : Mat n)
        (hM : ∀ i k, (∑ j : Fin n,M i j*M k j) = if i = k then 1 else 0)
        (P : PolynomialSpace n) :
        (∑ j : Fin n,fischer (∑ i : Fin n,M i j • pderiv i P)
          (∑ k : Fin n,M k j • pderiv k P)) =
          ∑ i : Fin n,fischer (pderiv i P) (pderiv i P) := by
    …

    Mentions: OAI.HarmonicCounterexample.Mat, OAI.HarmonicCounterexample.Angular.PolynomialSpace, OAI.HarmonicCounterexample.Angular.fischer

59. lemma OAI.HarmonicCounterexample.Angular.polynomialRotation_gradient line 606
60. lemma OAI.HarmonicCounterexample.Angular.fischer_rotation_bound line 615

    Source documentation

    The sharp degree-l rotation bound, proved on genuine polynomials by Fischer duality, Euler's identity, and Cauchy--Schwarz.

    lemma fischer_rotation_bound (M : Mat n)
        (hM : ∀ i k, (∑ j : Fin n,M i j*M k j) = if i = k then 1 else 0)
        {P : PolynomialSpace n} {l : ℕ} (hP : P.IsHomogeneous l) :
        fischer (polynomialRotation M P) (polynomialRotation M P) ≤
          (l:ℝ)^2*fischer P P := by
    …

    Mentions: OAI.HarmonicCounterexample.Mat, OAI.HarmonicCounterexample.Angular.PolynomialSpace, OAI.HarmonicCounterexample.Angular.fischer, OAI.HarmonicCounterexample.Angular.polynomialRotation

61. lemma OAI.HarmonicCounterexample.Angular.fischer_square_rotation_nonpos line 641
62. lemma OAI.HarmonicCounterexample.Angular.fischer_square_rotation_lower line 648
63. instance OAI.HarmonicCounterexample.Angular.polynomialNormedAddCommGroup line 667
64. instance OAI.HarmonicCounterexample.Angular.polynomialUniformSpace line 672

    Source documentation

    Override the unrelated power-series coefficient topology with the topology of the Fischer norm; the underlying polynomial algebra is unchanged.

    @[reducible] instance polynomialUniformSpace (n : ℕ) : UniformSpace (PolynomialSpace n) :=
    …

    Mentions: OAI.HarmonicCounterexample.Angular.PolynomialSpace

65. instance OAI.HarmonicCounterexample.Angular.polynomialTopologicalSpace line 675
66. instance OAI.HarmonicCounterexample.Angular.polynomialInnerProductSpace line 678
67. instance OAI.HarmonicCounterexample.Angular.harmonicNormedAddCommGroup line 681
68. instance OAI.HarmonicCounterexample.Angular.harmonicSeminormedAddCommGroup line 683
69. instance OAI.HarmonicCounterexample.Angular.harmonicTopologicalSpace line 685
70. instance OAI.HarmonicCounterexample.Angular.harmonicUniformSpace line 687
71. instance OAI.HarmonicCounterexample.Angular.harmonicInnerProductSpace line 689
72. instance OAI.HarmonicCounterexample.Angular.harmonicOperatorNormSMulClass line 692
73. lemma OAI.HarmonicCounterexample.Angular.polynomial_inner line 697
74. lemma OAI.HarmonicCounterexample.Angular.harmonic_inner line 699
75. def OAI.HarmonicCounterexample.Angular.rotationCLM line 703

    Source documentation

    The genuine infinitesimal Hopf operator as a bounded operator on V_l.

    def rotationCLM (J : ComplexStructure (Fin n)) (l : ℕ) :
        harmonicPolynomials n l →L[ℝ] harmonicPolynomials n l :=
    …

    Mentions: OAI.HarmonicCounterexample.Angular.harmonicPolynomials

76. lemma OAI.HarmonicCounterexample.Angular.rotationCLM_inner_skew line 707
77. lemma OAI.HarmonicCounterexample.Angular.complexStructure_rows line 712
78. lemma OAI.HarmonicCounterexample.Angular.rotationCLM_norm_le line 719
79. lemma OAI.HarmonicCounterexample.Angular.rotationCLM_opNorm_le line 727
80. lemma OAI.HarmonicCounterexample.Angular.rotationCLM_square_symmetric line 731
81. lemma OAI.HarmonicCounterexample.Angular.rotationCLM_square_nonpos line 738
82. lemma OAI.HarmonicCounterexample.Angular.rotationCLM_square_lower line 743
83. def OAI.HarmonicCounterexample.Control.directionalPolynomial line 762
84. lemma OAI.HarmonicCounterexample.Control.directionalPolynomial_apply line 767
85. lemma OAI.HarmonicCounterexample.Control.directionalPolynomial_mul line 772
86. lemma OAI.HarmonicCounterexample.Control.pderiv_linearChange line 778
87. def OAI.HarmonicCounterexample.Control.ordinaryLaplacian line 790
88. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_apply line 794
89. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_linearChange line 797
90. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_rename line 816
91. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_map line 827
92. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitChange_gram line 841
93. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_split line 859
94. lemma OAI.HarmonicCounterexample.Control.linearChange_injective line 876
95. def OAI.HarmonicCounterexample.Control.realCoefficients line 895
96. lemma OAI.HarmonicCounterexample.Control.coeff_realCoefficients line 900
97. lemma OAI.HarmonicCounterexample.Control.realCoefficients_ofReal line 903
98. lemma OAI.HarmonicCounterexample.Control.ofReal_realCoefficients line 908
99. lemma OAI.HarmonicCounterexample.Control.realCoefficients_homogeneous line 922
100. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_realCoefficients line 932
101. lemma OAI.HarmonicCounterexample.Control.linearChange_split_inl line 951
102. lemma OAI.HarmonicCounterexample.Control.linearChange_split_inr line 956
103. lemma OAI.HarmonicCounterexample.Control.conjugate_split_X line 961
104. lemma OAI.HarmonicCounterexample.Control.conjugate_split line 970
105. def OAI.HarmonicCounterexample.Control.cartesianChange line 982

     Source documentation

     The literal Cartesian coefficient substitution z=x+iy,w=x-iy, including the index identification with the ambient Euclidean R^16.

     def cartesianChange : SplitPolynomial (Fin 8) →ₐ[ℂ] MvPolynomial (Fin 16) ℂ :=
     …

106. def OAI.HarmonicCounterexample.Control.inverseCartesianChange line 985
107. lemma OAI.HarmonicCounterexample.Control.inverse_cartesianChange line 989
108. lemma OAI.HarmonicCounterexample.Control.cartesianChange_inverse line 996
109. lemma OAI.HarmonicCounterexample.Control.cartesianChange_injective line 1011
110. lemma OAI.HarmonicCounterexample.Control.cartesianChange_homogeneous line 1014
111. lemma OAI.HarmonicCounterexample.Control.inverseCartesianChange_homogeneous line 1018
112. lemma OAI.HarmonicCounterexample.Control.conjugate_cartesianChange line 1022
113. lemma OAI.HarmonicCounterexample.Control.ordinaryLaplacian_cartesianChange line 1030
114. lemma OAI.HarmonicCounterexample.Control.conjugate_ofReal line 1047
115. lemma OAI.HarmonicCounterexample.Control.cartesianChange_fixed line 1052
116. lemma OAI.HarmonicCounterexample.Control.cartesianChange_harmonic line 1058
117. lemma OAI.HarmonicCounterexample.Control.realCartesian_mem line 1062
118. lemma OAI.HarmonicCounterexample.Control.inverseCartesian_mem line 1068
119. lemma OAI.HarmonicCounterexample.Control.inverseCartesian_fixed line 1082
120. def OAI.HarmonicCounterexample.Control.realCartesianHarmonic line 1090

     Source documentation

     Literal real polynomial equivalence: the split-coordinate real form is exactly the Cartesian harmonic space, not merely an abstract dimension copy.

     def realCartesianHarmonic (l : ℕ) : realHarmonicSpace l ≃ₗ[ℝ] Angular.harmonicPolynomials 16 l where
     …

     Mentions: OAI.HarmonicCounterexample.Angular.harmonicPolynomials

121. lemma OAI.HarmonicCounterexample.Control.realCartesianHarmonic_apply line 1115
122. lemma OAI.HarmonicCounterexample.Control.ofReal_realCartesianHarmonic line 1118
123. lemma OAI.HarmonicCounterexample.Control.linearField_map line 1132
124. lemma OAI.HarmonicCounterexample.Control.linearField_rename line 1138
125. lemma OAI.HarmonicCounterexample.Control.linearChange_splitField line 1151
126. lemma OAI.HarmonicCounterexample.Control.cartesianChange_field line 1160
127. lemma OAI.HarmonicCounterexample.Control.rotation_eq_field line 1168
128. lemma OAI.HarmonicCounterexample.Control.harmonicField_star line 1172
129. lemma OAI.HarmonicCounterexample.Control.restrictReal_harmonicField_val line 1178
130. lemma OAI.HarmonicCounterexample.Control.realCartesian_rotation line 1187