OAI/Geometry/HarmonicGrowth/PolarGeometry.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Construction.horizontalScale line 13
2. def OAI.HarmonicCounterexample.Construction.horizontalSlope line 16
3. lemma OAI.HarmonicCounterexample.Construction.horizontalScale_smooth line 19
4. lemma OAI.HarmonicCounterexample.Construction.horizontalScale_pos line 23
5. lemma OAI.HarmonicCounterexample.Construction.horizontalSlope_smooth line 27
6. lemma OAI.HarmonicCounterexample.Construction.logSlope_hasDeriv line 31
7. lemma OAI.HarmonicCounterexample.Construction.horizontalScale_hasDeriv line 37
8. lemma OAI.HarmonicCounterexample.Construction.horizontalSlope_deriv line 49
9. lemma OAI.HarmonicCounterexample.Construction.scalar_initial_local line 56
10. lemma OAI.HarmonicCounterexample.Construction.logSlope_initial_local line 63
11. lemma OAI.HarmonicCounterexample.Construction.horizontalScale_initial line 72
12. theorem OAI.HarmonicCounterexample.Construction.scalar_all_curvatures line 79

    Source documentation

    The early round region is handled by exact radial concavity; the late threshold controls all periods, for the same q and c used to tune the equation.

    theorem scalar_all_curvatures {κ : Type*} (w : LinearODE.PhysicalWord κ)
        {μ : ℝ} (hμ : 0<μ) (hμ1 : μ≤1/4) (ha : Tendsto (Scale.profile μ) atTop (𝓝 a)) :
        ∃ J : ℕ,∀ j0,J≤j0 → ∀ s : ℕ → Fin w.n → ℝ,(∀ j,s j ∈ w.admissible) →
          (∀ t,1/2 ≤ scalar s qstar j0 t ∧ scalar s qstar j0 t ≤ qstar+1/2) ∧
          ∀ t,let q:=scalar s qstar j0
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.PhysicalWord, OAI.HarmonicCounterexample.Scale.profile, OAI.HarmonicCounterexample.Construction.a, OAI.HarmonicCounterexample.Construction.qstar

13. def OAI.HarmonicCounterexample.Construction.mu line 122
14. lemma OAI.HarmonicCounterexample.Construction.mu_pos line 123
15. lemma OAI.HarmonicCounterexample.Construction.mu_le line 124
16. lemma OAI.HarmonicCounterexample.Construction.profile_limit line 125
17. lemma OAI.HarmonicCounterexample.Construction.scale_match line 126
18. lemma OAI.HarmonicCounterexample.Construction.profile_lower line 127
19. def OAI.HarmonicCounterexample.Construction.alpha line 130
20. def OAI.HarmonicCounterexample.Construction.drift line 131
21. lemma OAI.HarmonicCounterexample.Construction.alpha_smooth line 133
22. lemma OAI.HarmonicCounterexample.Construction.alpha_pos line 135
23. lemma OAI.HarmonicCounterexample.Construction.alpha_bound line 136
24. lemma OAI.HarmonicCounterexample.Construction.drift_smooth line 144
25. lemma OAI.HarmonicCounterexample.Construction.drift_bounds line 146
26. lemma OAI.HarmonicCounterexample.Construction.alpha_center line 153
27. lemma OAI.HarmonicCounterexample.Construction.drift_center line 155
28. lemma OAI.HarmonicCounterexample.Construction.alpha_limit line 157
29. lemma OAI.HarmonicCounterexample.Construction.drift_limit line 159
30. def OAI.HarmonicCounterexample.Construction.geometry line 164
31. def OAI.HarmonicCounterexample.Berger.tensorContract line 203
32. lemma OAI.HarmonicCounterexample.Berger.contract_add line 205
33. lemma OAI.HarmonicCounterexample.Berger.contract_smul line 209
34. lemma OAI.HarmonicCounterexample.Berger.contract_rank line 218
35. lemma OAI.HarmonicCounterexample.Berger.contract_identity line 227
36. lemma OAI.HarmonicCounterexample.Berger.symmetric_pairing line 230
37. lemma OAI.HarmonicCounterexample.Berger.connection_lower_matrix line 234
38. lemma OAI.HarmonicCounterexample.Berger.contract_connection line 248
39. lemma OAI.HarmonicCounterexample.Berger.polarTensor_symmetric line 266
40. lemma OAI.HarmonicCounterexample.Berger.polarTensor_trace line 272
41. lemma OAI.HarmonicCounterexample.Berger.polarTensor_radial line 280
42. lemma OAI.HarmonicCounterexample.Berger.polarTensor_hopf line 288
43. lemma OAI.HarmonicCounterexample.Berger.contract_normalizedConnection line 297

    Source documentation

    The full contracted connection, derived algebraically from the actual six Christoffel coefficients; no polar Laplacian formula is assumed.

    lemma contract_normalizedConnection (J : ComplexStructure (Fin n)) {x : Space n}
        (hS : x ⬝ᵥ x ≠ 0) {A q : ℝ} (hA : A ≠ 0) (hq : q ≠ 0)
        (u v : ℝ) (k : Fin n) :
        tensorContract (polarTensor J x A⁻¹ (A*q)⁻¹)
          (fun i j => normalizedConnectionCoeff J x A q u v k i j) =
          (((n:ℝ)-2)/A+1/(A*q)-((n:ℝ)-1)*(1+u)-v)/(x ⬝ᵥ x)*x k := by
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Berger.tensorContract, OAI.HarmonicCounterexample.Berger.polarTensor, OAI.HarmonicCounterexample.Berger.normalizedConnectionCoeff

44. lemma OAI.HarmonicCounterexample.Berger.contract_comm line 323
45. lemma OAI.HarmonicCounterexample.Berger.contract_polarTensor line 326
46. def OAI.HarmonicCounterexample.Berger.gradient line 336

    Source documentation

    Cartesian gradient and Hessian, with the same coordinate order as the frozen definition of the Laplace--Beltrami operator.

    def gradient (f : Space n → ℝ) (x : Space n) : Space n := fun i => coordDeriv i f x

    Mentions: OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.coordDeriv

47. def OAI.HarmonicCounterexample.Berger.hessian line 337
48. def OAI.HarmonicCounterexample.Berger.euler line 338
49. def OAI.HarmonicCounterexample.Berger.hopfDerivative line 339
50. def OAI.HarmonicCounterexample.Berger.euclideanLaplacian line 342
51. lemma OAI.HarmonicCounterexample.Berger.laplace_contract line 344
52. lemma OAI.HarmonicCounterexample.Berger.euler_expansion line 359
53. lemma OAI.HarmonicCounterexample.Berger.euler_twice line 370
54. lemma OAI.HarmonicCounterexample.Berger.hopf_expansion line 382
55. lemma OAI.HarmonicCounterexample.Berger.hopf_twice line 396
56. theorem OAI.HarmonicCounterexample.Berger.laplace_polar line 428

    Source documentation

    The complete polar Laplacian identity, derived from the actual Cartesian Hessian and Christoffels. This isolates the analytic bridge independently of any spectral or harmonic-polynomial assumptions.

    theorem laplace_polar (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        (f : Space n → ℝ) {x : Space n} (hS : x ⬝ᵥ x ≠ 0)
        {A q : ℝ} (hA : A ≠ 0) (hq : q ≠ 0) (u v : ℝ)
        (hg : (g.coeff x)⁻¹ = polarTensor J x A⁻¹ (A*q)⁻¹)
        (hΓ : ∀ k i j, christoffel g x k i j = normalizedConnectionCoeff J x A q u v k i j)
        (hf : ∀ j, DifferentiableAt ℝ (coordDeriv j f) x) :
        (x ⬝ᵥ x)*laplaceBeltrami g f x =
          euler (euler f) x + ((n:ℝ)-2+((n:ℝ)-1)*u+v)*euler f x +
          A⁻¹*((x ⬝ᵥ x)*euclideanLaplacian f x-euler (euler f) x-((n:ℝ)-2)*euler f x)+
          ((A*q)⁻¹-A⁻¹)*hopfDerivative J (hopfDerivative J f) x := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Berger.polarTensor, OAI.HarmonicCounterexample.christoffel, OAI.HarmonicCounterexample.Berger.normalizedConnectionCoeff, OAI.HarmonicCounterexample.coordDeriv, OAI.HarmonicCounterexample.laplaceBeltrami, OAI.HarmonicCounterexample.Berger.euler, OAI.HarmonicCounterexample.Berger.euclideanLaplacian, OAI.HarmonicCounterexample.Berger.hopfDerivative

57. lemma OAI.HarmonicCounterexample.Berger.coordDeriv_smooth line 465
58. lemma OAI.HarmonicCounterexample.Berger.euler_congr line 469
59. lemma OAI.HarmonicCounterexample.Berger.hopf_congr line 473
60. lemma OAI.HarmonicCounterexample.Berger.euler_mul line 477
61. lemma OAI.HarmonicCounterexample.Berger.hopf_mul line 484
62. lemma OAI.HarmonicCounterexample.Berger.coordDeriv_product_second line 492
63. lemma OAI.HarmonicCounterexample.Berger.euclideanLaplacian_mul line 509
64. lemma OAI.HarmonicCounterexample.Berger.euler_add line 523
65. lemma OAI.HarmonicCounterexample.Berger.euler_smooth line 528
66. lemma OAI.HarmonicCounterexample.Berger.hopf_smooth line 532
67. lemma OAI.HarmonicCounterexample.Cartesian.logProfile_differentiableAt line 551
68. lemma OAI.HarmonicCounterexample.Cartesian.logProfile_coord_differentiableAt line 556
69. lemma OAI.HarmonicCounterexample.Cartesian.logProfile_second line 570
70. lemma OAI.HarmonicCounterexample.Cartesian.euler_logProfile line 589
71. lemma OAI.HarmonicCounterexample.Cartesian.hopf_logProfile line 599
72. lemma OAI.HarmonicCounterexample.Cartesian.laplacian_logProfile line 610
73. lemma OAI.HarmonicCounterexample.Cartesian.euler_logProfile_mul line 642
74. lemma OAI.HarmonicCounterexample.Cartesian.euler_twice_logProfile_mul line 650
75. lemma OAI.HarmonicCounterexample.Cartesian.hopf_logProfile_mul line 665
76. lemma OAI.HarmonicCounterexample.Cartesian.hopf_twice_logProfile_mul line 672
77. lemma OAI.HarmonicCounterexample.Cartesian.gradient_logProfile_dot line 682
78. lemma OAI.HarmonicCounterexample.Cartesian.euclideanLaplacian_logProfile_mul line 691
79. lemma OAI.HarmonicCounterexample.Cartesian.coordDeriv_product_differentiableAt line 709
80. theorem OAI.HarmonicCounterexample.Cartesian.laplace_homogeneous_profile line 724

    Source documentation

    The actual Cartesian Laplace--Beltrami operator on a radial coefficient times a homogeneous harmonic polynomial. Every derivative in this statement is the genuine Fréchet/coordinate derivative, not a spectral placeholder.

    theorem laplace_homogeneous_profile (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {f f1 f2 : ℝ → ℝ} {P : Space n → ℝ} {l : ℝ}
        (hf : ∀ t, HasDerivAt f (f1 t) t) (hf1 : ∀ t, HasDerivAt f1 (f2 t) t)
        (hP : ContDiff ℝ ∞ P) (hE : ∀ x, euler P x = l*P x)
        (hH : ∀ x, euclideanLaplacian P x = 0) {x : Space n} (hx : x ≠ 0)
        {A q : ℝ} (hA : A ≠ 0) (hq : q ≠ 0) (u v : ℝ)
        (hg : (g.coeff x)⁻¹ = polarTensor J x A⁻¹ (A*q)⁻¹)
        (hΓ : ∀ k i j, christoffel g x k i j = normalizedConnectionCoeff J x A q u v k i j) :
        (x ⬝ᵥ x)*laplaceBeltrami g (fun y => f (logRadius y)*P y) x =
          (f2 (logRadius x)+(2*l+(n:ℝ)-2+((n:ℝ)-1)*u+v)*f1 (logRadius x)+
            (l^2+((n:ℝ)-2+((n:ℝ)-1)*u+v)*l-A⁻¹*l*(l+(n:ℝ)-2))*f (logRadius x))*P x+
            ((A*q)⁻¹-A⁻¹)*f (logRadius x)*hopfDerivative J (hopfDerivative J P) x := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.christoffel, OAI.HarmonicCounterexample.laplaceBeltrami, OAI.HarmonicCounterexample.Cartesian.logRadius

81. def OAI.HarmonicCounterexample.Cartesian.regularCoefficient line 761

    Source documentation

    Polynomial-normalized coefficient. This is constant in the Euclidean core.

    def regularCoefficient (l : ℝ) (Y : ℝ → ι → ℝ) (i : ι) (t : ℝ) : ℝ :=
    …

82. def OAI.HarmonicCounterexample.Cartesian.synthesized line 764
83. lemma OAI.HarmonicCounterexample.Cartesian.regularCoefficient_deriv line 768
84. lemma OAI.HarmonicCounterexample.Cartesian.regularCoefficient_second line 777
85. lemma OAI.HarmonicCounterexample.Cartesian.regularCoefficient_core line 789
86. lemma OAI.HarmonicCounterexample.Cartesian.synthesized_smooth line 795
87. lemma OAI.HarmonicCounterexample.Cartesian.laplace_sum line 818
88. lemma OAI.HarmonicCounterexample.Cartesian.laplace_regular_term line 846