OAI/Geometry/ProjectionBodies/SphericalCore.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PettyProjection.Spherical.Space line 13
2. abbrev OAI.PettyProjection.Spherical.Sphere line 14
3. def OAI.PettyProjection.Spherical.surface line 16
4. def OAI.PettyProjection.Spherical.sigma line 19
5. instance OAI.PettyProjection.Spherical.surface_finite line 22
6. lemma OAI.PettyProjection.Spherical.surface_ne_zero line 26
7. instance OAI.PettyProjection.Spherical.sigma_probability line 29
8. instance OAI.PettyProjection.Spherical.surface_open_pos line 35
9. instance OAI.PettyProjection.Spherical.sigma_open_pos line 39
10. def OAI.PettyProjection.Spherical.mean line 43

    Source documentation

    Spherical means in the probability normalization.

    def mean {n : ℕ} (f : Sphere n → ℝ) : ℝ := ∫ u, f u ∂sigma n

    Mentions: OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.sigma

11. lemma OAI.PettyProjection.Spherical.mean_const line 45
12. instance OAI.PettyProjection.Spherical.sphere_compact line 48
13. lemma OAI.PettyProjection.Spherical.norm_coe line 51
14. abbrev OAI.PettyProjection.Spherical.H line 55

    Source documentation

    Continuous functions are put into the actual spherical L² space.

    abbrev H (n : ℕ) := Lp ℝ 2 (sigma n)

    Mentions: OAI.PettyProjection.Spherical.sigma

15. def OAI.PettyProjection.Spherical.toH line 57
16. def OAI.PettyProjection.Spherical.coordinateProduct line 62

    Source documentation

    Restrictions of ambient coordinate quadratics. Their span contains the constants on the unit sphere and all degree-two spherical harmonics.

    def coordinateProduct (n : ℕ) (i j : Fin n) : C(Sphere n, ℝ) where
    …

    Mentions: OAI.PettyProjection.Spherical.Sphere

17. def OAI.PettyProjection.Spherical.lowSpace line 66
18. instance OAI.PettyProjection.Spherical.lowSpace_finite line 70
19. def OAI.PettyProjection.Spherical.Q line 75

    Source documentation

    The complement of the constants and the quadratics. For even input this is exactly the even tail of degree at least four.

    def Q (n : ℕ) [NeZero n] : H n →L[ℝ] H n :=
    …

    Mentions: OAI.PettyProjection.Spherical.H

20. lemma OAI.PettyProjection.Spherical.sum_coordinateProduct line 78
21. lemma OAI.PettyProjection.Spherical.constant_mem_lowSpace line 85
22. lemma OAI.PettyProjection.Spherical.Q_eq_sub line 97
23. lemma OAI.PettyProjection.Spherical.Q_constant line 101
24. lemma OAI.PettyProjection.Spherical.norm_Q_le line 106
25. lemma OAI.PettyProjection.Spherical.inner_toH line 109
26. lemma OAI.PettyProjection.Spherical.norm_toH_sq line 113
27. lemma OAI.PettyProjection.Spherical.norm_Q_le_centered line 118
28. def OAI.PettyProjection.Spherical.sphereMap line 129

    Source documentation

    Orthogonal changes of variables on the actual unit sphere.

    def sphereMap {n : ℕ} (U : Space n ≃ₗᵢ[ℝ] Space n) : Sphere n ≃ₜ Sphere n where
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.Sphere

29. lemma OAI.PettyProjection.Spherical.cone_preimage line 137
30. lemma OAI.PettyProjection.Spherical.surface_preserving line 150
31. lemma OAI.PettyProjection.Spherical.sigma_preserving line 159
32. lemma OAI.PettyProjection.Spherical.mean_rotation line 163
33. def OAI.PettyProjection.Spherical.rotation line 174

    Source documentation

    Exponentiating an actual skew-adjoint operator produces rotations.

    def rotation {n : ℕ} (T : Space n →L[ℝ] Space n) (hT : star T = -T) (t : ℝ) :
        Space n ≃ₗᵢ[ℝ] Space n :=
    …

    Mentions: OAI.PettyProjection.Spherical.Space

34. lemma OAI.PettyProjection.Spherical.rotation_apply line 180
35. lemma OAI.PettyProjection.Spherical.rotation_zero line 183
36. lemma OAI.PettyProjection.Spherical.hasDerivAt_rotation line 190
37. lemma OAI.PettyProjection.Spherical.continuous_integrable line 196
38. lemma OAI.PettyProjection.Spherical.mean_fderiv_skew line 204

    Source documentation

    Infinitesimal rotation invariance, with differentiation justified using uniform derivative bounds on the compact sphere. This supplies spherical integration by parts without postulating it as an interface.

    lemma mean_fderiv_skew {n : ℕ} [NeZero n] (T : Space n →L[ℝ] Space n)
        (hT : star T = -T) (f : Space n → ℝ) (hf : ContDiff ℝ 1 f) :
        mean (fun u : Sphere n => fderiv ℝ f u (T u)) = 0 := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Sphere

39. def OAI.PettyProjection.Spherical.rotDeriv line 244

    Source documentation

    Derivative along an infinitesimal linear rotation.

    def rotDeriv {n : ℕ} (T : Space n →L[ℝ] Space n) (f : Space n → ℝ) : Space n → ℝ :=
    …

    Mentions: OAI.PettyProjection.Spherical.Space

40. lemma OAI.PettyProjection.Spherical.continuous_rotDeriv line 247
41. lemma OAI.PettyProjection.Spherical.contDiff_rotDeriv line 251
42. lemma OAI.PettyProjection.Spherical.rotDeriv_mul line 255
43. lemma OAI.PettyProjection.Spherical.mean_rotDeriv_mul line 263

    Source documentation

    Genuine spherical integration by parts for each rotation generator.

    lemma mean_rotDeriv_mul {n : ℕ} [NeZero n] (T : Space n →L[ℝ] Space n)
        (hT : star T = -T) {f g : Space n → ℝ}
        (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) :
        mean (fun u : Sphere n => f u * rotDeriv T g u) =
          - mean (fun u : Sphere n => g u * rotDeriv T f u) := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.rotDeriv

44. def OAI.PettyProjection.Spherical.generator line 284

    Source documentation

    The standard skew generator in the i,j plane.

    def generator (n : ℕ) (i j : Fin n) : Space n →L[ℝ] Space n :=
    …

    Mentions: OAI.PettyProjection.Spherical.Space

45. lemma OAI.PettyProjection.Spherical.generator_skew line 288
46. lemma OAI.PettyProjection.Spherical.generator_apply line 293
47. lemma OAI.PettyProjection.Spherical.generator_apply_coord line 297
48. lemma OAI.PettyProjection.Spherical.generator_self line 302
49. lemma OAI.PettyProjection.Spherical.generator_swap line 305
50. def OAI.PettyProjection.Spherical.energy line 309

    Source documentation

    The Dirichlet form, expressed without local coordinates by rotations.

    def energy {n : ℕ} (f g : Space n → ℝ) : ℝ :=
    …

    Mentions: OAI.PettyProjection.Spherical.Space

51. def OAI.PettyProjection.Spherical.casimir line 315

    Source documentation

    The spherical Laplacian expressed by its rotation generators.

    def casimir {n : ℕ} (f : Space n → ℝ) : Space n → ℝ := fun x =>
    …

    Mentions: OAI.PettyProjection.Spherical.Space

52. lemma OAI.PettyProjection.Spherical.energy_symm line 319
53. lemma OAI.PettyProjection.Spherical.energy_nonneg line 322
54. lemma OAI.PettyProjection.Spherical.mean_sum line 330
55. lemma OAI.PettyProjection.Spherical.mean_casimir line 335
56. def OAI.PettyProjection.Spherical.polynomialFunction line 365

    Source documentation

    Ambient evaluation of a polynomial, using the Euclidean coordinates.

    def polynomialFunction {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : Space n → ℝ :=
    …

    Mentions: OAI.PettyProjection.Spherical.Space

57. lemma OAI.PettyProjection.Spherical.polynomialFunction_contDiff line 368
58. def OAI.PettyProjection.Spherical.polynomialRotation line 379

    Source documentation

    Polynomial rotation differentiation, a derivation preserving degree.

    def polynomialRotation {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℝ) :
        MvPolynomial (Fin n) ℝ :=
    …

59. lemma OAI.PettyProjection.Spherical.rotDeriv_add line 383
60. lemma OAI.PettyProjection.Spherical.rotDeriv_const line 388
61. lemma OAI.PettyProjection.Spherical.rotDeriv_coordinate line 392
62. lemma OAI.PettyProjection.Spherical.polynomialRotation_add line 399
63. lemma OAI.PettyProjection.Spherical.polynomialRotation_mul line 404
64. lemma OAI.PettyProjection.Spherical.polynomialRotation_C line 410
65. lemma OAI.PettyProjection.Spherical.polynomialFunction_add line 414
66. lemma OAI.PettyProjection.Spherical.polynomialFunction_mul line 419
67. lemma OAI.PettyProjection.Spherical.polynomialFunction_X line 424
68. lemma OAI.PettyProjection.Spherical.polynomialFunction_C line 429
69. lemma OAI.PettyProjection.Spherical.rotDeriv_polynomialFunction line 435

    Source documentation

    The formal polynomial generator agrees with actual differentiation.

    lemma rotDeriv_polynomialFunction {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℝ) :
        rotDeriv (generator n i j) (polynomialFunction p) =
          polynomialFunction (polynomialRotation i j p) := by
    …

    Mentions: OAI.PettyProjection.Spherical.rotDeriv, OAI.PettyProjection.Spherical.generator, OAI.PettyProjection.Spherical.polynomialFunction, OAI.PettyProjection.Spherical.polynomialRotation

70. def OAI.PettyProjection.Spherical.radiusPolynomial line 462

    Source documentation

    Radius squared as an ambient polynomial.

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

71. def OAI.PettyProjection.Spherical.eulerPolynomial line 464
72. def OAI.PettyProjection.Spherical.laplacePolynomial line 467
73. lemma OAI.PettyProjection.Spherical.polynomialRotation_twice line 470
74. lemma OAI.PettyProjection.Spherical.eulerPolynomial_twice line 484
75. lemma OAI.PettyProjection.Spherical.sum_polynomialRotation_twice line 496
76. def OAI.PettyProjection.Spherical.eigenvalue line 532

    Source documentation

    The spherical Laplace eigenvalues.

    def eigenvalue (n d : ℕ) : ℝ := (d : ℝ) * ((d : ℝ) + n - 2)

77. lemma OAI.PettyProjection.Spherical.eulerPolynomial_nsmul line 534
78. lemma OAI.PettyProjection.Spherical.eulerPolynomial_homogeneous line 541
79. lemma OAI.PettyProjection.Spherical.sum_polynomialRotation_homogeneous line 545
80. lemma OAI.PettyProjection.Spherical.polynomialFunction_radius line 556
81. lemma OAI.PettyProjection.Spherical.casimir_polynomialFunction line 564

    Source documentation

    Polar Laplacian identity, derived from finite rotation sums and Euler's identity rather than assumed as a spherical calculus interface.

    lemma casimir_polynomialFunction {n d : ℕ} {p : MvPolynomial (Fin n) ℝ}
        (hp : p.IsHomogeneous d) (x : Space n) :
        casimir (polynomialFunction p) x =
          ‖x‖ ^ 2 * polynomialFunction (laplacePolynomial p) x -
            eigenvalue n d * polynomialFunction p x := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.casimir, OAI.PettyProjection.Spherical.polynomialFunction, OAI.PettyProjection.Spherical.laplacePolynomial, OAI.PettyProjection.Spherical.eigenvalue

82. lemma OAI.PettyProjection.Spherical.casimir_harmonic line 579
83. lemma OAI.PettyProjection.Spherical.eigenvalue_strictMono line 585
84. lemma OAI.PettyProjection.Spherical.harmonic_orthogonal line 596

    Source documentation

    Distinct homogeneous harmonic degrees are orthogonal under actual normalized surface measure.

    lemma harmonic_orthogonal {n d e : ℕ} (hn : 2 ≤ n)
        {p q : MvPolynomial (Fin n) ℝ} (hp : p.IsHomogeneous d) (hq : q.IsHomogeneous e)
        (hΔp : laplacePolynomial p = 0) (hΔq : laplacePolynomial q = 0) (hde : d ≠ e) :
        mean (fun u : Sphere n => polynomialFunction p u * polynomialFunction q u) = 0 := by
    …

    Mentions: OAI.PettyProjection.Spherical.laplacePolynomial, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.polynomialFunction

85. lemma OAI.PettyProjection.Spherical.laplacePolynomial_add line 617
86. lemma OAI.PettyProjection.Spherical.laplacePolynomial_sub line 621
87. lemma OAI.PettyProjection.Spherical.laplacePolynomial_C_mul line 625
88. lemma OAI.PettyProjection.Spherical.laplacePolynomial_homogeneous line 629
89. lemma OAI.PettyProjection.Spherical.pderiv_radiusPolynomial line 635
90. lemma OAI.PettyProjection.Spherical.radiusPolynomial_homogeneous line 639
91. lemma OAI.PettyProjection.Spherical.laplacePolynomial_radius_mul line 644
92. lemma OAI.PettyProjection.Spherical.laplacePolynomial_radius_mul_homogeneous line 657
93. def OAI.PettyProjection.Spherical.radialCoefficient line 666

    Source documentation

    The nonzero radial coefficient in the finite Fischer decomposition.

    def radialCoefficient (n l j : ℕ) : ℝ := 2 * (j + 1 : ℕ) * (2 * l + 2 * (j + 1 : ℕ) + n - 2)

94. lemma OAI.PettyProjection.Spherical.radialCoefficient_pos line 668
95. lemma OAI.PettyProjection.Spherical.radius_pow_mul_homogeneous line 678
96. lemma OAI.PettyProjection.Spherical.laplacePolynomial_radial_harmonic line 683
97. lemma OAI.PettyProjection.Spherical.laplacePolynomial_smul line 703
98. lemma OAI.PettyProjection.Spherical.laplacePolynomial_eq_zero_small line 707
99. def OAI.PettyProjection.Spherical.fischerSpan line 718

    Source documentation

    Algebraic span of radius powers times homogeneous harmonics of fixed total degree.

    def fischerSpan (n d : ℕ) : Submodule ℝ (MvPolynomial (Fin n) ℝ) :=
    …

100. lemma OAI.PettyProjection.Spherical.fischerSpan_le_homogeneous line 722
101. lemma OAI.PettyProjection.Spherical.harmonic_mem_fischerSpan line 728
102. lemma OAI.PettyProjection.Spherical.fischerSpan_laplace_preimage line 732
103. lemma OAI.PettyProjection.Spherical.homogeneous_mem_fischerSpan line 753

     Source documentation

     Finite Fischer decomposition: the induction on the degree.

     lemma homogeneous_mem_fischerSpan {n : ℕ} (hn : 2 ≤ n) (d : ℕ)
         {p : MvPolynomial (Fin n) ℝ} (hp : p.IsHomogeneous d) : p ∈ fischerSpan n d := by
     …

     Mentions: OAI.PettyProjection.Spherical.fischerSpan

104. def OAI.PettyProjection.Spherical.polynomialRestriction line 769

     Source documentation

     Actual polynomial restrictions, as continuous functions on the sphere.

     def polynomialRestriction (n : ℕ) : MvPolynomial (Fin n) ℝ →ₐ[ℝ] C(Sphere n, ℝ) where
     …

     Mentions: OAI.PettyProjection.Spherical.Sphere

105. lemma OAI.PettyProjection.Spherical.polynomialRestriction_apply line 784
106. lemma OAI.PettyProjection.Spherical.polynomialRestriction_radius line 787
107. lemma OAI.PettyProjection.Spherical.polynomialRestriction_separates line 792
108. lemma OAI.PettyProjection.Spherical.polynomialRestriction_dense line 803
109. def OAI.PettyProjection.Spherical.polynomialL2 line 811
110. lemma OAI.PettyProjection.Spherical.polynomialL2_dense line 814
111. def OAI.PettyProjection.Spherical.laplaceLinear line 818
112. def OAI.PettyProjection.Spherical.harmonicPolynomials line 823
113. instance OAI.PettyProjection.Spherical.harmonicPolynomials_finite line 826
114. def OAI.PettyProjection.Spherical.harmonicSpace line 833

     Source documentation

     The genuine homogeneous harmonic subspaces of spherical L².

     def harmonicSpace (n d : ℕ) [NeZero n] : Submodule ℝ (H n) :=
     …

     Mentions: OAI.PettyProjection.Spherical.H

115. instance OAI.PettyProjection.Spherical.harmonicSpace_finite line 836
116. lemma OAI.PettyProjection.Spherical.harmonicSpace_orthogonal line 840
117. lemma OAI.PettyProjection.Spherical.polynomialL2_mem_iSup_of_fischer line 851
118. lemma OAI.PettyProjection.Spherical.polynomialL2_mem_iSup line 865
119. lemma OAI.PettyProjection.Spherical.harmonicSpace_total line 875

     Source documentation

     Completeness under the actual measure, using Stone--Weierstrass and finite Fischer decomposition, with no assumed spectral interface.

     lemma harmonicSpace_total {n : ℕ} (hn : 2 ≤ n) [NeZero n] :
         (⨆ l, harmonicSpace n l).topologicalClosure = ⊤ := by
     …

     Mentions: OAI.PettyProjection.Spherical.harmonicSpace

120. lemma OAI.PettyProjection.Spherical.energy_add_right line 882
121. lemma OAI.PettyProjection.Spherical.energy_add_left line 901
122. lemma OAI.PettyProjection.Spherical.rotDeriv_const_mul line 906
123. lemma OAI.PettyProjection.Spherical.energy_const_mul_right line 913
124. lemma OAI.PettyProjection.Spherical.energy_const_mul_left line 919
125. lemma OAI.PettyProjection.Spherical.energy_sub_self line 924
126. lemma OAI.PettyProjection.Spherical.energy_zero_right line 937
127. lemma OAI.PettyProjection.Spherical.energy_finset_sum_right line 940
128. lemma OAI.PettyProjection.Spherical.energy_harmonic_right line 952

     Source documentation

     Integration by parts against each genuine harmonic eigenfunction.

     lemma energy_harmonic_right {n d : ℕ} [NeZero n] {f : Space n → ℝ}
         {p : MvPolynomial (Fin n) ℝ} (hf : ContDiff ℝ 1 f) (hp : p.IsHomogeneous d)
         (hΔp : laplacePolynomial p = 0) :
         energy f (polynomialFunction p) = eigenvalue n d *
           mean (fun u : Sphere n => f u * polynomialFunction p u) := by
     …

     Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.laplacePolynomial, OAI.PettyProjection.Spherical.energy, OAI.PettyProjection.Spherical.polynomialFunction, OAI.PettyProjection.Spherical.eigenvalue, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Sphere

129. lemma OAI.PettyProjection.Spherical.polynomialFunction_smul_argument line 963
130. lemma OAI.PettyProjection.Spherical.harmonicSpace_zero_constant line 974
131. lemma OAI.PettyProjection.Spherical.constant_mem_harmonicSpace_zero line 988
132. lemma OAI.PettyProjection.Spherical.harmonicSpace_zero_projection line 997