BianchiCurvature.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Curvature contractions of the concrete Bianchi tensor

The normalized spectral moments and the matrix-slot contraction are computed from the actual symmetric matrix of Euclidean four-vectors in Bianchi.

def OAI.PositiveEinsteinFour.Bianchi.Shape.sigma line 20
Source documentation
Normalized cubic spectral moment.
```
def Shape.sigma (S : Shape) : ℝ := (∑ i, S.s i ^ 3) / 6
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape
def OAI.PositiveEinsteinFour.Bianchi.Shape.skewMoment line 23
Source documentation
Rational form of ρ / √3.
```
def Shape.skewMoment (S : Shape) : ℝ := (∑ i, S.s i ^ 2 * difference S.s i) / 18
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.difference
def OAI.PositiveEinsteinFour.Bianchi.Shape.rho line 26
Source documentation
The oriented companion spectral moment.
```
def Shape.rho (S : Shape) : ℝ := Real.sqrt 3 * S.skewMoment
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape
def OAI.PositiveEinsteinFour.Bianchi.Shape.tilde line 29
Source documentation
The normalized quarter-turn spectral vector.
```
def Shape.tilde (S : Shape) (i : Fin 3) : ℝ := difference S.s i / Real.sqrt 3
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.difference
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.trace_coordinates line 31
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.norm_coordinates line 36
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.sigma_skew_circle line 42
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.sigma_rho_circle line 53
Source documentation
The exact normalized identity used by every spectral matrix estimate.
```
theorem Shape.sigma_rho_circle (S : Shape) : S.rho ^ 2 = 1 - S.sigma ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.rho_div_sqrt_three line 58
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.rho_eq_source line 63
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.square_decomposition line 76
Source documentation
The normalized trace-free square is expanded in the two spectral vectors.
```
theorem Shape.square_decomposition (S : Shape) (i : Fin 3) :
    S.s i ^ 2 - 2 = S.sigma * S.s i + S.rho * S.tilde i := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.mixed_cubic line 99
Source documentation
Cubic moment in the unnormalized quarter-turn vector.
```
theorem Shape.mixed_cubic (S : Shape) :
    (∑ i, S.s i * difference S.s i ^ 2) = -18 * S.sigma := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.difference
def OAI.PositiveEinsteinFour.Bianchi.curvatureContraction line 109
Source documentation
Direct matrix-slot quadratic contraction with diagonal Weyl block v*s. The second sum is the off-diagonal contribution, because the spectral trace vanishes.
```
def curvatureContraction (S : Shape) (v : ℝ) (T : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureContraction_eq_matrix line 114
Source documentation
This is the contraction of the actual three-by-three matrix, not an independent scalar surrogate.
```
theorem curvatureContraction_eq_matrix (S : Shape) (v : ℝ) (T : Tensor) :
    curvatureContraction S v T = (v / 6) * ∑ i, ∑ j, S.s i * ‖T.matrix i j‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.curvatureContraction
theorem OAI.PositiveEinsteinFour.Bianchi.diagonal_contraction line 124
theorem OAI.PositiveEinsteinFour.Bianchi.off_contraction line 134
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureContraction_parameters line 149
Source documentation
The B/v matrix in Section 5 follows from the concrete parameter tensor. All three variables remain real tangent four-vectors.
```
theorem curvatureContraction_parameters (S : Shape) (v : ℝ) (p k l : Vec) :
    curvatureContraction S v (parameters S p k l) =
      v * ((4 / 3) * S.sigma * ‖p‖ ^ 2 -
        8 * S.rho / Real.sqrt 3 * inner ℝ p k -
        4 * S.sigma * ‖k‖ ^ 2 - 2 * inner ℝ k l) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.curvatureContraction, OAI.PositiveEinsteinFour.Bianchi.parameters
theorem OAI.PositiveEinsteinFour.Bianchi.Shape.squareWeight_eq line 167
Source documentation
Rational form of the same trace-free square decomposition.
```
theorem Shape.squareWeight_eq (S : Shape) (i : Fin 3) :
    S.s i ^ 2 - 2 = S.sigma * S.s i + S.skewMoment * difference S.s i := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.difference
def OAI.PositiveEinsteinFour.Bianchi.Shape.squareWeight line 177
Source documentation
The normalized eigenvalues of the trace-free square of the Weyl block.
```
def Shape.squareWeight (S : Shape) (i : Fin 3) : ℝ := S.s i ^ 2 - 2
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape
theorem OAI.PositiveEinsteinFour.Bianchi.cube_sum line 179
theorem OAI.PositiveEinsteinFour.Bianchi.mixed_cube_sum line 183
theorem OAI.PositiveEinsteinFour.Bianchi.difference_cube_sum line 188
theorem OAI.PositiveEinsteinFour.Bianchi.squareWeight_moments line 196
def OAI.PositiveEinsteinFour.Bianchi.squareCurvatureContraction line 246
Source documentation
The actual matrix-slot contraction with N = (T²)₀.
```
def squareCurvatureContraction (S : Shape) (v : ℝ) (T : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_diagonal_contraction line 250
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_off_contraction line 261
theorem OAI.PositiveEinsteinFour.Bianchi.squareCurvatureContraction_parameters line 276
Source documentation
The C_N/v² matrix in Section 5 from the concrete four-vector tensor.
```
theorem squareCurvatureContraction_parameters (S : Shape) (v : ℝ) (p k l : Vec) :
    squareCurvatureContraction S v (parameters S p k l) =
      v ^ 2 * ((4 / 3) * ‖p‖ ^ 2 - 2 * S.rho / Real.sqrt 3 * inner ℝ p l -
        4 * ‖k‖ ^ 2 - 2 * S.sigma * inner ℝ k l) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.squareCurvatureContraction, OAI.PositiveEinsteinFour.Bianchi.parameters