BianchiHessian.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The Hessian matrix on actual quaternionic Bianchi tensors

The energy pairing and the matrix-slot operator are transported through the proved bijective parametrization. Thus the squared-operator term uses the inverse energy metric automatically.

def OAI.PositiveEinsteinFour.Bianchi.Tensor.pairing line 20
Source documentation
The normalized Hilbert--Schmidt pairing.
```
def Tensor.pairing (T U : Tensor) : ℝ := (∑ i, ∑ j, inner ℝ (T.matrix i j) (U.matrix i j)) / 6
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_add_matrix line 22
theorem OAI.PositiveEinsteinFour.Bianchi.parameters_pairing line 29
Source documentation
The full inner product, not just the norm, is transported by the coordinate map with metric diag(5/3,5,1).
```
theorem parameters_pairing (S : Shape) (p k l p' k' l' : Vec) :
    (parameters S p k l).pairing (parameters S p' k' l') =
      (5 / 3) * inner ℝ p p' + 5 * inner ℝ k k' + inner ℝ l l' := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.parameters
def OAI.PositiveEinsteinFour.Bianchi.curvatureActionP line 46
def OAI.PositiveEinsteinFour.Bianchi.curvatureActionK line 49
def OAI.PositiveEinsteinFour.Bianchi.curvatureActionL line 52
def OAI.PositiveEinsteinFour.Bianchi.curvatureAction line 55
Source documentation
The matrix-slot curvature operator on the concrete Bianchi space.
```
def curvatureAction (S : Shape) (v : ℝ) (p k l : Vec) : Tensor :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureAction_pairing line 59
Source documentation
The transported operator is self-adjoint for the actual energy pairing.
```
theorem curvatureAction_pairing (S : Shape) (v : ℝ) (p k l p' k' l' : Vec) :
    (curvatureAction S v p k l).pairing (parameters S p' k' l') =
      v * ((4 / 3) * S.sigma * inner ℝ p p' -
        4 * S.skewMoment * (inner ℝ p k' + inner ℝ k p') -
        4 * S.sigma * inner ℝ k k' - inner ℝ k l' - inner ℝ l k') := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.curvatureAction, OAI.PositiveEinsteinFour.Bianchi.parameters
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureAction_quadratic line 72
Source documentation
The quadratic form of the transported operator is exactly contraction with the diagonal Weyl block, computed from matrix entries.
```
theorem curvatureAction_quadratic (S : Shape) (v : ℝ) (p k l : Vec) :
    (curvatureAction S v p k l).pairing (parameters S p k l) =
      curvatureContraction S v (parameters S p k l) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.curvatureAction, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureContraction
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureAction_energy line 85
Source documentation
The B H⁻¹ B term is the squared Hilbert--Schmidt norm of the actual transported operator, with all tangent correlations retained.
```
theorem curvatureAction_energy (S : Shape) (v : ℝ) (p k l : Vec) :
    (curvatureAction S v p k l).squaredNorm / 6 =
      v ^ 2 * ((16 / 15) * ‖p‖ ^ 2 + (21 / 5) * ‖k‖ ^ 2 + ‖l‖ ^ 2 / 5 +
        (8 / 5) * S.skewMoment * inner ℝ p l + (8 / 5) * S.sigma * inner ℝ k l) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.curvatureAction
def OAI.PositiveEinsteinFour.Bianchi.hessianTensorForm line 99
Source documentation
The first-derivative Hessian form expressed directly using concrete matrix contractions and the actual inverse-energy-metric operator.
```
def hessianTensorForm (S : Shape) (v b : ℝ) (p k l : Vec) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec

theorem OAI.PositiveEinsteinFour.Bianchi.hessianTensor_matrix line 107

Source documentation

Equation (12) on real tangent vectors, with the precise off-diagonal pairings and without assumptions about their signs.

theorem hessianTensor_matrix (S : Shape) (v b : ℝ) (p k l : Vec) :
    hessianTensorForm S v b p k l =
      (-70 - 5 * b ^ 2 + 100 * S.sigma * v - 25 * v ^ 2) * ‖p‖ ^ 2 +
      (-210 - 15 * b ^ 2 - 300 * S.sigma * v - 190 * v ^ 2) * ‖k‖ ^ 2 +
      (-42 - 3 * b ^ 2 - 10 * v ^ 2) * ‖l‖ ^ 2 -
      200 * Real.sqrt 3 * S.rho * v * inner ℝ p k -
      70 * S.rho * v ^ 2 / Real.sqrt 3 * inner ℝ p l -
      2 * (75 * v + 35 * S.sigma * v ^ 2) * inner ℝ k l := by
…

Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.hessianTensorForm

theorem OAI.PositiveEinsteinFour.Bianchi.projection_cost_coefficients line 128
Source documentation
The projected quadratic cost is bounded by the exact coefficients used in equation (19) for the concrete Bianchi tensor.
```
theorem projection_cost_coefficients (S : Shape) {v : ℝ} (hv : 0 ≤ v)
    (y : ℝ) (p k l : Vec) :
    (7 / 12) * (4 + y) * ((parameters S p k l).squaredNorm / 6) -
      (5 / 4) * curvatureContraction S v (parameters S p k l) ≤
    QuarticEnergy.projectionCoefficient v y S.sigma S.rho * ((5 / 3) * ‖p‖ ^ 2) +
      Energy.defectCoefficient v y * ((parameters S p k l).squaredNorm / 6 -
        (5 / 3) * ‖p‖ ^ 2) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.parameters, OAI.PositiveEinsteinFour.Bianchi.curvatureContraction, OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient, OAI.PositiveEinsteinFour.Energy.defectCoefficient
theorem OAI.PositiveEinsteinFour.Bianchi.binary_inner_nonneg line 139
theorem OAI.PositiveEinsteinFour.Bianchi.normalized_curvature_bound line 153
Source documentation
The unit normalized matrix-slot action is a contraction for the complete Bianchi energy metric.
```
theorem normalized_curvature_bound (S : Shape) (p k l : Vec) :
    |(4 / 3) * S.sigma * ‖p‖ ^ 2 - 8 * S.skewMoment * inner ℝ p k -
      4 * S.sigma * ‖k‖ ^ 2 - 2 * inner ℝ k l| ≤
      (5 / 3) * ‖p‖ ^ 2 + 5 * ‖k‖ ^ 2 + ‖l‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec
theorem OAI.PositiveEinsteinFour.Bianchi.curvatureContraction_abs_le line 172
Source documentation
Operator bound stated using the actual matrix contraction and energy.
```
theorem curvatureContraction_abs_le (S : Shape) {v : ℝ} (hv : 0 ≤ v) (p k l : Vec) :
    |curvatureContraction S v (parameters S p k l)| ≤
      v * ((parameters S p k l).squaredNorm / 6) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.curvatureContraction, OAI.PositiveEinsteinFour.Bianchi.parameters