OAI/Geometry/HarmonicGrowth/Curvature.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.square_mulVec line 18
2. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.trace_zero line 22
3. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.dot_skew line 27
4. lemma OAI.HarmonicCounterexample.Berger.trace_rank_mul line 35
5. lemma OAI.HarmonicCounterexample.Berger.trace_mul_rank line 41
6. lemma OAI.HarmonicCounterexample.Berger.trace_rank_rank line 46
7. def OAI.HarmonicCounterexample.Berger.connectionMatrix line 55

   Source documentation

   The endomorphism v ↦ Γ(u,v), after raising the first-kind connection. This nine-low-rank decomposition permits exact finite-dimensional traces.

   def connectionMatrix (J : ComplexStructure ι) (x : ι → ℝ)
       (a b c d e f : ℝ) (u : ι → ℝ) : Matrix ι ι ℝ :=
   …

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

8. lemma OAI.HarmonicCounterexample.Berger.connectionMatrix_trace line 65
9. lemma OAI.HarmonicCounterexample.Berger.connectionMatrix_trace_product line 77

   Source documentation

   Exact quadratic connection trace, the difficult algebraic part of Ricci. No dimension-specific computation or assumed Gauss/Codazzi formula is used.

   lemma connectionMatrix_trace_product (J : ComplexStructure ι) (x u v : ι → ℝ)
       (a b c d e f : ℝ) :
       (connectionMatrix J x a b c d e f u *
         connectionMatrix J x a b c d e f v).trace =
       2*a*b*(x ⬝ᵥ x)*(u ⬝ᵥ v) +
       ((2*a+b+c*(x ⬝ᵥ x))^2 + (a+d*(x ⬝ᵥ x)+f)^2 +
         ((Fintype.card ι:ℝ)-2)*a^2-2*a*b)*(x ⬝ᵥ u)*(x ⬝ᵥ v) +
       (2*(a+d*(x ⬝ᵥ x)+f)*(b+e*(x ⬝ᵥ x)-2*f) -
         ((Fintype.card ι:ℝ)-2)*f^2-2*a*b)*
           ((J.matrix *ᵥ x) ⬝ᵥ u)*((J.matrix *ᵥ x) ⬝ᵥ v) := by
   …

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

10. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.diagonal_zero line 120
11. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.entry_skew line 126
12. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.sum_x_entry line 129
13. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.sum_w_entry line 134
14. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.sum_entries line 139
15. def OAI.HarmonicCounterexample.Berger.connectionCoeff line 144

    Source documentation

    Cartesian Christoffel coefficients written in their invariant six-term form.

    def connectionCoeff (J : ComplexStructure (Fin n)) (x : Space n)
        (a b c d e f : ℝ) (k i j : Fin n) : ℝ :=
    …

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

16. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_eq_matrix line 152
17. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_symmetric line 166
18. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_trace line 174
19. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_inner_trace line 183
20. lemma OAI.HarmonicCounterexample.Berger.coordDeriv_radialSquare line 199
21. lemma OAI.HarmonicCounterexample.Berger.differentiableAt_linear_entry line 210
22. lemma OAI.HarmonicCounterexample.Berger.divergence_delta_radial line 233
23. lemma OAI.HarmonicCounterexample.Berger.divergence_radial_delta line 244
24. lemma OAI.HarmonicCounterexample.Berger.divergence_radial_cubic line 262
25. lemma OAI.HarmonicCounterexample.Berger.divergence_hopf_mixed line 283
26. lemma OAI.HarmonicCounterexample.Berger.divergence_hopf_cubic line 313
27. lemma OAI.HarmonicCounterexample.Berger.divergence_hopf_linear line 337
28. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_radial_contraction line 379
29. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_outer_trace line 403
30. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_differentiableAt line 421
31. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_divergence line 432
32. lemma OAI.HarmonicCounterexample.Berger.connectionCoeff_trace_derivative line 453
33. theorem OAI.HarmonicCounterexample.Berger.ricci_of_connectionCoeff line 481

    Source documentation

    Ricci computed from the exact Christoffel ansatz on a neighbourhood. This theorem uses the frozen coordinate definition of ricci verbatim.

    theorem ricci_of_connectionCoeff (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {a b c d e f : Space n → ℝ} {x : Space n} {ad bd cd dd ed fd : ℝ}
        (hΓ : ∀ᶠ y in 𝓝 x, ∀ k i j, christoffel g y k i j =
          connectionCoeff J y (a y) (b y) (c y) (d y) (e y) (f y) k i j)
        (ha : DifferentiableAt ℝ a x) (hb : DifferentiableAt ℝ b x)
        (hc : DifferentiableAt ℝ c x) (hd : DifferentiableAt ℝ d x)
        (he : DifferentiableAt ℝ e x) (hf : DifferentiableAt ℝ f x)
        (had : ∀ i, coordDeriv i a x = ad*x i) (hbd : ∀ i, coordDeriv i b x = bd*x i)
        (hcd : ∀ i, coordDeriv i c x = cd*x i) (hdd : ∀ i, coordDeriv i d x = dd*x i)
        (hed : ∀ i, coordDeriv i e x = ed*x i) (hfd : ∀ i, coordDeriv i f x = fd*x i)
        (i j : Fin n) :
        let S := x ⬝ᵥ x
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.christoffel, OAI.HarmonicCounterexample.Berger.connectionCoeff, OAI.HarmonicCounterexample.coordDeriv

34. def OAI.HarmonicCounterexample.Berger.polarTensor line 533

    Source documentation

    Polar tensor in unnormalized Cartesian coordinates. Its radial/Hopf/ horizontal eigenvalues are respectively 1,D,A.

    def polarTensor (J : ComplexStructure ι) (x : ι → ℝ) (A D : ℝ) : Matrix ι ι ℝ :=
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

35. lemma OAI.HarmonicCounterexample.Berger.polarTensor_inverse line 537
36. lemma OAI.HarmonicCounterexample.Berger.polarTensor_mulVec line 553
37. def OAI.HarmonicCounterexample.Berger.rawPolarEntry line 582
38. def OAI.HarmonicCounterexample.Berger.lowerConnectionCoeff line 586
39. lemma OAI.HarmonicCounterexample.Berger.firstKind_rawPolar line 595

    Source documentation

    First-kind Levi-Civita calculation, directly from coordinate derivatives.

    lemma firstKind_rawPolar (J : ComplexStructure (Fin n))
        {A B C : Space n → ℝ} {x : Space n} {Ad Bd Cd : ℝ}
        (hA : DifferentiableAt ℝ A x) (hB : DifferentiableAt ℝ B x)
        (hC : DifferentiableAt ℝ C x)
        (hAd : ∀ i, coordDeriv i A x = Ad*x i)
        (hBd : ∀ i, coordDeriv i B x = Bd*x i)
        (hCd : ∀ i, coordDeriv i C x = Cd*x i)
        (l i j : Fin n) :
        (1/2:ℝ)*(coordDeriv i (fun y => rawPolarEntry J A B C y j l) x+
          coordDeriv j (fun y => rawPolarEntry J A B C y i l) x-
          coordDeriv l (fun y => rawPolarEntry J A B C y i j) x) =
          lowerConnectionCoeff J x (B x) (C x) Ad Bd Cd l i j := by
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.coordDeriv, OAI.HarmonicCounterexample.Berger.rawPolarEntry, OAI.HarmonicCounterexample.Berger.lowerConnectionCoeff

40. lemma OAI.HarmonicCounterexample.Berger.lowerConnection_radial line 640
41. lemma OAI.HarmonicCounterexample.Berger.lowerConnection_hopf line 665
42. lemma OAI.HarmonicCounterexample.Berger.raise_lowerConnection line 695

    Source documentation

    Raising the first-kind expression gives exactly the six invariant scalar coefficients; this is an algebra theorem, not a curvature assumption.

    lemma raise_lowerConnection (J : ComplexStructure (Fin n)) (x : Space n)
        (hx : x ⬝ᵥ x ≠ 0) (A D B C Ad Bd Cd : ℝ) (k i j : Fin n) :
        (∑ l, polarTensor J x A⁻¹ D⁻¹ k l*lowerConnectionCoeff J x B C Ad Bd Cd l i j) =
        connectionCoeff J x (Ad/(2*A)) (B-Ad/2)
          (Ad*(1-A⁻¹)/(x ⬝ᵥ x)+Bd/2)
          (Ad*(D⁻¹-A⁻¹)/(2*(x ⬝ᵥ x))+Cd/(2*D)+C*(D⁻¹-A⁻¹)/(x ⬝ᵥ x))
          (-Cd/2-2*C*(1-A⁻¹)/(x ⬝ᵥ x)) (C/A) k i j := by
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Berger.polarTensor, OAI.HarmonicCounterexample.Berger.lowerConnectionCoeff, OAI.HarmonicCounterexample.Berger.connectionCoeff

43. theorem OAI.HarmonicCounterexample.Berger.christoffel_of_rawPolar line 736

    Source documentation

    The actual Levi-Civita connection is computed from locally given Cartesian metric entries. The only assumptions are differentiability and the polar tensor identities, not any curvature or connection formula.

    theorem christoffel_of_rawPolar (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {A B C : Space n → ℝ} {x : Space n} {D Ad Bd Cd : ℝ}
        (hcoeff : ∀ᶠ y in 𝓝 x, ∀ i j, g.coeff y i j = rawPolarEntry J A B C y i j)
        (hx : x ⬝ᵥ x ≠ 0) (hA0 : A x ≠ 0) (hD0 : D ≠ 0)
        (hBval : B x = (1-A x)/(x ⬝ᵥ x)) (hCval : C x = (D-A x)/(x ⬝ᵥ x))
        (hA : DifferentiableAt ℝ A x) (hB : DifferentiableAt ℝ B x)
        (hC : DifferentiableAt ℝ C x)
        (hAd : ∀ i, coordDeriv i A x = Ad*x i)
        (hBd : ∀ i, coordDeriv i B x = Bd*x i)
        (hCd : ∀ i, coordDeriv i C x = Cd*x i)
        (k i j : Fin n) :
        christoffel g x k i j =
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Berger.rawPolarEntry, OAI.HarmonicCounterexample.coordDeriv, OAI.HarmonicCounterexample.christoffel

44. def OAI.HarmonicCounterexample.Berger.normalAlpha line 797
45. def OAI.HarmonicCounterexample.Berger.normalBeta line 798
46. def OAI.HarmonicCounterexample.Berger.normalGamma line 799
47. def OAI.HarmonicCounterexample.Berger.normalDelta line 800
48. def OAI.HarmonicCounterexample.Berger.normalEpsilon line 801
49. def OAI.HarmonicCounterexample.Berger.normalZeta line 802
50. def OAI.HarmonicCounterexample.Berger.normalizedConnectionCoeff line 804
51. lemma OAI.HarmonicCounterexample.Berger.normalize_connection line 810
52. lemma OAI.HarmonicCounterexample.Berger.differentiableAt_radialSquare line 825
53. theorem OAI.HarmonicCounterexample.Berger.christoffel_normalized line 832

    Source documentation

    Actual normalized Christoffel producer from first derivatives of the metric profiles. Here h=(log A)'/2 and p=(log q)'/2 in logarithmic radius.

    theorem christoffel_normalized (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {A q : Space n → ℝ} {x : Space n} {h p : ℝ}
        (hmetric : ∀ᶠ y in 𝓝 x, ∀ i j, g.coeff y i j =
          rawPolarEntry J A (fun z => (1-A z)/(z ⬝ᵥ z))
            (fun z => A z*(q z-1)/(z ⬝ᵥ z)) y i j)
        (hS : x ⬝ᵥ x ≠ 0) (hA0 : A x ≠ 0) (hq0 : q x ≠ 0)
        (hA : DifferentiableAt ℝ A x) (hq : DifferentiableAt ℝ q x)
        (hAd : ∀ i, coordDeriv i A x = (2*A x*h/(x ⬝ᵥ x))*x i)
        (hqd : ∀ i, coordDeriv i q x = (2*q x*p/(x ⬝ᵥ x))*x i)
        (k i j : Fin n) :
        christoffel g x k i j = normalizedConnectionCoeff J x (A x) (q x) h p k i j := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Berger.rawPolarEntry, OAI.HarmonicCounterexample.coordDeriv, OAI.HarmonicCounterexample.christoffel, OAI.HarmonicCounterexample.Berger.normalizedConnectionCoeff

54. def OAI.HarmonicCounterexample.Berger.normalAlphaD line 883
55. def OAI.HarmonicCounterexample.Berger.normalBetaD line 884
56. def OAI.HarmonicCounterexample.Berger.normalGammaD line 885
57. def OAI.HarmonicCounterexample.Berger.normalDeltaD line 886
58. def OAI.HarmonicCounterexample.Berger.normalEpsilonD line 887
59. def OAI.HarmonicCounterexample.Berger.normalZetaD line 888
60. lemma OAI.HarmonicCounterexample.Berger.gradient_normalAlpha line 890
61. lemma OAI.HarmonicCounterexample.Berger.gradient_normalBeta line 903
62. lemma OAI.HarmonicCounterexample.Berger.gradient_normalGamma line 919
63. lemma OAI.HarmonicCounterexample.Berger.gradient_normalDelta line 935
64. lemma OAI.HarmonicCounterexample.Berger.gradient_normalEpsilon line 951
65. lemma OAI.HarmonicCounterexample.Berger.gradient_normalZeta line 971
66. def OAI.HarmonicCounterexample.Berger.normalTrace line 1001
67. def OAI.HarmonicCounterexample.Berger.normalTraceD line 1002
68. def OAI.HarmonicCounterexample.Berger.horizontalRicciNumerator line 1004
69. def OAI.HarmonicCounterexample.Berger.verticalRicciNumerator line 1006
70. def OAI.HarmonicCounterexample.Berger.radialRicciNumerator line 1008
71. lemma OAI.HarmonicCounterexample.Berger.normalTrace_identity line 1011
72. lemma OAI.HarmonicCounterexample.Berger.normalTraceD_identity line 1019
73. lemma OAI.HarmonicCounterexample.Berger.normalized_ricci_zero line 1029
74. lemma OAI.HarmonicCounterexample.Berger.normalized_ricci_one line 1042
75. lemma OAI.HarmonicCounterexample.Berger.normalized_ricci_two line 1061
76. theorem OAI.HarmonicCounterexample.Berger.ricci_normalized line 1099

    Source documentation

    Exact Cartesian Ricci coefficients for the Berger metric, in logarithmic radial variables. All curvature operations use the frozen coordinate formula.

    theorem ricci_normalized (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {A q u v : Space n → ℝ} {x : Space n} {ud vd : ℝ}
        (hΓ : ∀ᶠ y in 𝓝 x, ∀ k i j, christoffel g y k i j =
          normalizedConnectionCoeff J y (A y) (q y) (u y) (v y) k i j)
        (hS : x ⬝ᵥ x ≠ 0)
        (hA : DifferentiableAt ℝ A x) (hq : DifferentiableAt ℝ q x)
        (hu : DifferentiableAt ℝ u x) (hv : DifferentiableAt ℝ v x)
        (hdA : ∀ i, coordDeriv i A x = (2*A x*u x)/(x ⬝ᵥ x)*x i)
        (hdq : ∀ i, coordDeriv i q x = (2*q x*v x)/(x ⬝ᵥ x)*x i)
        (hdu : ∀ i, coordDeriv i u x = ud/(x ⬝ᵥ x)*x i)
        (hdv : ∀ i, coordDeriv i v x = vd/(x ⬝ᵥ x)*x i)
        (i j : Fin n) :
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Berger.ComplexStructure, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.christoffel, OAI.HarmonicCounterexample.Berger.normalizedConnectionCoeff, OAI.HarmonicCounterexample.coordDeriv

77. lemma OAI.HarmonicCounterexample.Cartesian.coordDeriv_logRadius line 1167
78. lemma OAI.HarmonicCounterexample.Cartesian.coordDeriv_logProfile line 1177
79. lemma OAI.HarmonicCounterexample.Cartesian.tensor_eq_rawPolar line 1184
80. theorem OAI.HarmonicCounterexample.Cartesian.christoffel_logProfiles line 1197

    Source documentation

    Produces the actual Levi-Civita connection for logarithmic profiles, locally in a fixed complex label (round gaps can use any label).

    theorem christoffel_logProfiles (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {A q u v : ℝ → ℝ} {x : Space n} (hx : x ≠ 0)
        (hg : ∀ᶠ y in 𝓝 x, g.coeff y =
          tensor (radialUnit y) (hopfUnit J y) (A (logRadius y)) (q (logRadius y)))
        (hA : HasDerivAt A (2*A (logRadius x)*u (logRadius x)) (logRadius x))
        (hq : HasDerivAt q (2*q (logRadius x)*v (logRadius x)) (logRadius x))
        (hA0 : A (logRadius x) ≠ 0) (hq0 : q (logRadius x) ≠ 0)
        (k i j : Fin n) :
        christoffel g x k i j = normalizedConnectionCoeff J x
          (A (logRadius x)) (q (logRadius x)) (u (logRadius x)) (v (logRadius x)) k i j := by
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Cartesian.radialUnit, OAI.HarmonicCounterexample.Cartesian.hopfUnit, OAI.HarmonicCounterexample.Cartesian.logRadius, OAI.HarmonicCounterexample.christoffel

81. theorem OAI.HarmonicCounterexample.Cartesian.ricci_logProfiles line 1224

    Source documentation

    Full Ricci formula from the Cartesian definition for a locally fixed Berger label. It includes radial, Hopf and horizontal curvature with mixed terms zero.

    theorem ricci_logProfiles (g : SmoothMetric n) (J : ComplexStructure (Fin n))
        {A q u v : ℝ → ℝ} {x : Space n} {ud vd : ℝ} (hx : x ≠ 0)
        (hg : ∀ᶠ y in 𝓝 x, g.coeff y =
          tensor (radialUnit y) (hopfUnit J y) (A (logRadius y)) (q (logRadius y)))
        (hA : ∀ t, HasDerivAt A (2*A t*u t) t)
        (hq : ∀ t, HasDerivAt q (2*q t*v t) t)
        (hA0 : ∀ t, A t ≠ 0) (hq0 : ∀ t, q t ≠ 0)
        (hu : HasDerivAt u ud (logRadius x)) (hv : HasDerivAt v vd (logRadius x))
        (i j : Fin n) :
        let t := logRadius x
    …

    Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Cartesian.radialUnit, OAI.HarmonicCounterexample.Cartesian.hopfUnit, OAI.HarmonicCounterexample.Cartesian.logRadius

82. lemma OAI.HarmonicCounterexample.Berger.polar_quadratic line 1277
83. lemma OAI.HarmonicCounterexample.Berger.radialRicci_shape line 1296
84. lemma OAI.HarmonicCounterexample.Berger.horizontalRicci_round line 1303
85. lemma OAI.HarmonicCounterexample.Berger.verticalRicci_round line 1309
86. lemma OAI.HarmonicCounterexample.Berger.roundRicci_nonnegative line 1315
87. lemma OAI.HarmonicCounterexample.Cartesian.polarCoefficients_nonnegative line 1353

    Source documentation

    Eigenvalue positivity implies nonnegative Ricci as the frozen bilinear form, including all directions, not only radial or eigenvector test directions.

    lemma polarCoefficients_nonnegative (J : ComplexStructure (Fin n))
        {x : Space n} (hx : x ≠ 0) {H R V : ℝ}
        (hH : 0 ≤ H) (hR : 0 ≤ R) (hV : 0 ≤ V) (w : Space n) :
        0 ≤ ∑ i, ∑ j, (H/(x ⬝ᵥ x)*(1:Mat n) i j+
          (R-H)/(x ⬝ᵥ x)^2*x i*x j+
          (V-H)/(x ⬝ᵥ x)^2*(J.matrix *ᵥ x) i*(J.matrix *ᵥ x) j)*w i*w j := by
    …

    Mentions: OAI.HarmonicCounterexample.Space, OAI.HarmonicCounterexample.Mat

88. lemma OAI.HarmonicCounterexample.Berger.radial_scalar_budget line 1393