WeylEstimates01.lean`

952 declarations, 0 contain sorry, 0 declared as axioms

Differentiate the invariant matrix Weyl equation before choosing a diagonal frame. The derivative of its quadratic term is exactly twice the concrete matrix-slot operator.

def OAI.PositiveEinsteinFour.TraceHessian.matrixTraceMap line 61
theorem OAI.PositiveEinsteinFour.TraceHessian.hasDerivAt_matrixTrace line 64
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixSlotAction_derivative line 69
theorem OAI.PositiveEinsteinFour.TraceHessian.hasDerivAt_traceFreeSquare line 77
theorem OAI.PositiveEinsteinFour.TraceHessian.hasDerivAt_weylLaplacian line 89
Source documentation
The differentiated weak Weyl equation is 6Z - 12 B_F(T)Z in a parallel frame, without differentiating eigenvectors or eigenvalues.
```
theorem hasDerivAt_weylLaplacian {T : ℝ → Mat} {Z : Mat} {t : ℝ}
    (hT : HasDerivAt T Z t) :
    HasDerivAt (fun r => weylLaplacian (T r))
      ((6 : ℝ) • Z - (12 : ℝ) • matrixSlotAction (T t) Z) t := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.weylLaplacian
theorem OAI.PositiveEinsteinFour.TraceHessian.third_trace_eq_of_bianchi_commutator line 100
Source documentation
Along a parallel frame, differentiate the Weyl equation derived from Bianchi and the raw curvature commutator. The trace of the third derivative is therefore a conclusion rather than another geometric input.
```
theorem third_trace_eq_of_bianchi_commutator
    (T : ℝ → Mat) (X : ℝ → Hessian) (D : Fin 4 → Mat) (Z : Mat) (r : ℝ)
    (hs : ∀ t, symmetric (T t)) (ht : ∀ t, traceFree (T t))
    (hm : ∀ t i j, symmetric (X t i j) ∧ traceFree (X t i j))
    (hb : ∀ t i s, HighestHessian.divergence (X t) i s = 0)
    (hc : ∀ t i j a b, X t i j a b - X t j i a b =
      bundleCurvatureAction (T t) i j (T t) a b)
    (hT : HasDerivAt T Z r)
    (hX : ∀ i, HasDerivAt (fun t => X t i i) (D i) r) :
    (∑ i, D i) = (6 : ℝ) • Z - (12 : ℝ) • matrixSlotAction (T r) Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.Hessian, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.TraceHessian.bundleCurvatureAction
def OAI.PositiveEinsteinFour.Geometry.matrixSlotAt line 135
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotAt_weylLaplacian line 142
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotAt_sum_trace line 151

theorem OAI.PositiveEinsteinFour.Geometry.matrix_green_main_terms line 158

Source documentation

The Laplacian correction contributes 3B - 3C; together with the Ricci term -13B + 20E this gives the matrix-slot polynomial.

theorem matrix_green_main_terms (T : Mat) (hT : symmetric T)
    (Z L : GradientVector) (E : ℝ)
    (hL : inner ℝ (matrixSlotOperator T Z) L =
      13 * inner ℝ (matrixSlotOperator T Z) Z - 20 * E) :
    -inner ℝ Z (matrixSlotOperator T L) +
        (1 / 2 : ℝ) * inner ℝ Z (matrixSlotOperator (weylLaplacian T) Z) =
      -10 * inner ℝ (matrixSlotOperator T Z) Z -
        3 * inner ℝ (matrixSlotOperator (traceFreeSquare T) Z) Z + 20 * E := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.GradientVector, OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator

theorem OAI.PositiveEinsteinFour.Geometry.curvatureBilinear_self line 172
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_diagonal_raw line 176
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_diagonal_self line 192
theorem OAI.PositiveEinsteinFour.Geometry.diagonalGradientForm_eq_entries line 200
theorem OAI.PositiveEinsteinFour.Geometry.traceFreeSquare_diagonal_shape line 209
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_square_self line 234

theorem OAI.PositiveEinsteinFour.Geometry.matrix_green_main_parameters line 249

Source documentation

This specialization supplies the exact normalized matrix-slot main term in the Hessian assembly from the raw Ricci equation.

theorem matrix_green_main_parameters (S : Shape) (v : ℝ) (p k l : Vec)
    (L : Tensor) (hLz : L.traceFree) (hLb : L.bianchi)
    (hL : L.matrix = ricciGradient (fun s => v * S.s s) (parameters S p k l)) :
    let T := Matrix.diagonal (fun s => v * S.s s)
…

theorem OAI.PositiveEinsteinFour.Geometry.matrix_green_main_scalar line 273
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_weight_cubic line 289
Source documentation
The derivative of the matrix coefficient is the actual cubic trace, with no eigenframe or parallel-coefficient premise.
```
theorem matrixSlot_weight_cubic (a : Fin 4 → ℝ) (Z : Angular.Gradient)
    (hs : ∀ j, symmetric (Z j)) (ht : ∀ j, traceFree (Z j)) :
    (∑ i, a i * inner ℝ (gradientVector Z)
      (matrixSlotOperator (Z i) (gradientVector Z))) =
      ∑ i, a i * Matrix.trace (Z i * (∑ j, Z j * Z j)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Geometry.gradientVector, OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator
structure OAI.PositiveEinsteinFour.Geometry.WeylCovariantIdentities line 327
Source documentation
The precise algebraic and covariant identities used from the classical Einstein/Weyl calculus, specialized to the plus block and Ricci 3g. All fields refer to the metric's actual tensors.
```
structure WeylCovariantIdentities (g : SmoothMetric M) : Prop where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.metric_weyl_trace line 341

theorem OAI.PositiveEinsteinFour.Geometry.metric_weyl_third_trace line 351

Source documentation

Differentiate on parallel frames and then evaluate at any requested frame. Surjectivity of the flow equivalence suffices; no chosen eigenframe is differentiated.

theorem metric_weyl_third_trace (g : SmoothMetric M)
    (h : WeylCovariantIdentities g) {μ : Measure (FrameBundle g)}
    (φ : Fin 4 → FrameFlow g μ)
    (hT : ∀ k t e, HasDerivAt
      (fun s => plusWeyl g ((φ k).map s e).base ((φ k).map s e).frame)
      (plusWeylGradient g ((φ k).map t e).base ((φ k).map t e).frame k) t)
    (hX : ∀ k i t e, HasDerivAt
      (fun s => plusWeylHessian g ((φ k).map s e).base ((φ k).map s e).frame i i)
      (plusWeylThirdDerivative g ((φ k).map t e).base ((φ k).map t e).frame k i i) t)
    (k : Fin 4) (e : FrameBundle g) :
    (∑ i, plusWeylThirdDerivative g e.base e.frame k i i) =
      (6 : ℝ) • plusWeylGradient g e.base e.frame k -
…

Mentions: OAI.PositiveEinsteinFour.Geometry.WeylCovariantIdentities, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative

def OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice line 400
theorem OAI.PositiveEinsteinFour.Geometry.matrixRotation_slice line 402
theorem OAI.PositiveEinsteinFour.Geometry.bundleCurvatureAction_diagonal line 407
theorem OAI.PositiveEinsteinFour.Geometry.bundleCurvatureAction_sum line 416
Source documentation
The factor two from Ricci commutation cancels the half in the bundle curvature. Its sign comes from the covector quaternion's skew symmetry.
```
theorem bundleCurvatureAction_sum (t : Fin 3 → ℝ) (Z : Tensor)
    (j : Fin 4) (a b : Fin 3) :
    2 * (∑ i, bundleCurvatureAction (Matrix.diagonal t) i j
      (rawMatrixSlice Z.matrix i) a b) =
        -(∑ s, (1 + t s) * mixedGradient s Z a b j) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice
def OAI.PositiveEinsteinFour.Geometry.rawThirdLaplacian line 443

theorem OAI.PositiveEinsteinFour.Geometry.rawThirdLaplacian_eq_ricciGradient line 449

Source documentation

The raw gradient equation follows from the two tensor-slot Ricci identities, divergence freedom, and the differentiated invariant matrix equation. The conclusion still retains the uncompressed bundle action.

theorem rawThirdLaplacian_eq_ricciGradient (t : Fin 3 → ℝ) (Z : Tensor)
    (D V : Fin 4 → Fin 4 → Fin 4 → Mat)
    (R : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ)
    (hinner : ∀ i k j, D i k j - D i j k = V i k j +
      bundleCurvatureAction (Matrix.diagonal t) k j (rawMatrixSlice Z.matrix i))
    (houter : ∀ i k j, D i k j - D k i j =
      bundleCurvatureAction (Matrix.diagonal t) i k (rawMatrixSlice Z.matrix j) +
        ∑ h, R i k j h • rawMatrixSlice Z.matrix h)
    (hdiv : ∀ j, (∑ i, V i i j) = 0)
    (hRic : ∀ j h, (∑ i, R i j i h) = if j = h then 3 else 0)
    (htrace : ∀ j, (∑ i, D j i i) = (6 : ℝ) • rawMatrixSlice Z.matrix j -
      (12 : ℝ) • matrixSlotAction (Matrix.diagonal t) (rawMatrixSlice Z.matrix j)) :
…

Mentions: OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice, OAI.PositiveEinsteinFour.Geometry.matrixSlotAction

def OAI.PositiveEinsteinFour.Geometry.bundleCurvatureDerivative line 517
Source documentation
Differentiate the matrix coefficient in the bundle curvature action, keeping the tensor acted on fixed in a parallel frame.
```
def bundleCurvatureDerivative (A : Mat) (i j : Fin 4) (N : Mat) : Mat :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.bundleCurvatureDerivative_divergence line 520
theorem OAI.PositiveEinsteinFour.HighestHessian.rawSlice_weightTensor line 568
theorem OAI.PositiveEinsteinFour.HighestHessian.gradientVector_rawSlice line 574
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianPairing_weightTensor line 577
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_identity_green line 590
Source documentation
The identity-operator term of the local weighted square is precisely one sixth of the actual rough-Laplacian Green integrand.
```
theorem weightedQuadratic_identity_green (X : Hessian) (a : Vec) (Z : Tensor) (m : ℝ) :
    weightedQuadratic hessianNormSq m X (weightTensor a Z) =
      (m * hessianNormSq X +
        ∑ i, a i * inner ℝ (tensorGradientVector Z) (gradientVector (X i))) / 6 := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.weightTensor
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixPairing_weight_trace line 596
theorem OAI.PositiveEinsteinFour.HighestHessian.traceCorrection_green line 621
Source documentation
Both trace subtractions are the single trace Green integrand with coefficient −5/12. The equality traceCurvatureBlock t M = 6 • N is the finite-dimensional curvature identity for the prescribed trace.
```
theorem traceCorrection_green (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M N : Mat) (hsM : symmetric M) (htM : traceFree M)
    (hN : traceCurvatureBlock t M = (6 : ℝ) • N)
    (a : Vec) (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) (m : ℝ) :
    traceCorrection t u M m (weightTensor a Z) =
      -(5 / 12 : ℝ) * (m * matrixPairing N M +
        ∑ i, a i * matrixPairing N (rawMatrixSlice Z.matrix i)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.traceCurvatureBlock, OAI.PositiveEinsteinFour.HighestHessian.traceCorrection, OAI.PositiveEinsteinFour.HighestHessian.weightTensor
def OAI.PositiveEinsteinFour.CurvatureContraction.matrixPairingLinear line 664
theorem OAI.PositiveEinsteinFour.CurvatureContraction.bundleCurvatureAction_diagonal_matrix line 672
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixPairing_bundle_diagonal line 680

theorem OAI.PositiveEinsteinFour.CurvatureContraction.weighted_bundle_pairing line 692

Source documentation

Pairing with a curvature coefficient uses just its three two-form contractions. This isolates the normalization before the Bianchi step.

theorem weighted_bundle_pairing (A : Fin 4 → Fin 4 → ℝ) (b t : Fin 3 → ℝ)
    (hA : ∀ s, (∑ i, ∑ k, A i k * quaternionMatrix s i k) = b s)
    (N P : Mat) :
    (∑ i, ∑ k, A i k *
      matrixPairing (bundleCurvatureAction (Matrix.diagonal t) i k N) P) =
      (1 / 2 : ℝ) * ∑ s, b s * (1 + t s) *
        matrixPairing (matrixAction s N) P := by
…

theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_bundle_pairing line 725
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_bundle_pairing line 737
theorem OAI.PositiveEinsteinFour.CurvatureContraction.sum_pair_blocks line 744
theorem OAI.PositiveEinsteinFour.CurvatureContraction.quaternion_pairing_sum line 752

theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixAction_slices_pairing line 768

Source documentation

The derivative index of the matrix-bundle curvature gives the mixed Bianchi form with its covector sign.

theorem matrixAction_slices_pairing (s : Fin 3) (Z : Tensor) :
    (∑ j, ∑ l, quaternionMatrix s j l *
      matrixPairing (matrixAction s (rawMatrixSlice Z.matrix j))
        (rawMatrixSlice Z.matrix l)) = -mixedCouplingForm s Z := by
…

def OAI.PositiveEinsteinFour.CurvatureContraction.bundleGreenContraction line 777
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_bundleGreenContraction line 783
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_bundleGreenContraction line 808
def OAI.PositiveEinsteinFour.CurvatureContraction.covectorGreenContraction line 812
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixSlice_self_sum line 817
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_covectorGreenContraction line 827
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_covectorGreenContraction line 836
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_green_polynomial line 847
Source documentation
Both parts of the raw Ricci commutator give the polynomial in the self-dual derivative-slot Green term.
```
theorem plus_green_polynomial (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    bundleGreenContraction (plusCoefficient t) t Z +
      covectorGreenContraction (plusCoefficient t) (einsteinCoefficient t u) Z =
        (7 / 6 : ℝ) * (∑ s, t s ^ 2) * Z.squaredNorm -
          4 * diagonalGradientForm t Z -
          4 * diagonalGradientForm (fun s => t s ^ 2 - (∑ r, t r ^ 2) / 3) Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.bundleGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.covectorGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_green_polynomial line 859
Source documentation
The opposite block contributes only the covector Ricci contraction.
```
theorem minus_green_polynomial (t u : Fin 3 → ℝ) (hu : ∑ s, u s = 0)
    (Z : Tensor) :
    bundleGreenContraction (minusCoefficient u) t Z +
      covectorGreenContraction (minusCoefficient u) (einsteinCoefficient t u) Z =
        ((∑ s, u s ^ 2) / 2) * Z.squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.bundleGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.minusCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.covectorGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixPairing_add_left line 883
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixPairing_sub_left line 887
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixPairing_sum_smul_left line 891
theorem OAI.PositiveEinsteinFour.CurvatureContraction.sum_pair_swap line 899
theorem OAI.PositiveEinsteinFour.CurvatureContraction.sum_last_first line 907
def OAI.PositiveEinsteinFour.CurvatureContraction.rawCurvatureCommutator line 924
def OAI.PositiveEinsteinFour.CurvatureContraction.derivativeGreenContraction line 930
theorem OAI.PositiveEinsteinFour.CurvatureContraction.rawGreen_decomposition line 938
Source documentation
The full half-commutator splits into its two explicitly computed curvature actions. This is a finite identity, with no PDE estimate.
```
theorem rawGreen_decomposition
    (A R : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ)
    (t : Fin 3 → ℝ) (Z : Tensor) :
    derivativeGreenContraction A (rawCurvatureCommutator t R Z) Z =
      bundleGreenContraction A t Z + covectorGreenContraction A R Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.derivativeGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.rawCurvatureCommutator, OAI.PositiveEinsteinFour.CurvatureContraction.bundleGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.covectorGreenContraction
theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_rawGreen line 959
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_rawGreen line 968

theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_derivativeGreen_of_commutator line 976

Source documentation

Substituting precisely the ordinary Ricci identity computes the self-dual Green integrand.

theorem plus_derivativeGreen_of_commutator (t u : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi)
    (D : Fin 4 → Fin 4 → Fin 4 → Mat)
    (hD : ∀ i k j, D i k j - D k i j =
      rawCurvatureCommutator t (einsteinCoefficient t u) Z i k j) :
    derivativeGreenContraction (plusCoefficient t) (fun i k j => D i k j - D k i j) Z =
      (7 / 6 : ℝ) * (∑ s, t s ^ 2) * Z.squaredNorm -
        4 * diagonalGradientForm t Z -
        4 * diagonalGradientForm (fun s => t s ^ 2 - (∑ r, t r ^ 2) / 3) Z := by
…

Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.rawCurvatureCommutator, OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.derivativeGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient

theorem OAI.PositiveEinsteinFour.CurvatureContraction.integral_derivativeGreen line 991

theorem OAI.PositiveEinsteinFour.CurvatureContraction.integral_plusGreen_of_commutator line 1007

Source documentation

The self-dual half-commutator in the metric Green formula has the claimed scalar integral as a consequence of the raw Ricci identity.

theorem integral_plusGreen_of_commutator {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (m : Ω → ℝ) (t u : Ω → Fin 3 → ℝ) (Z : Ω → Tensor)
    (D : Ω → Fin 4 → Fin 4 → Fin 4 → Mat)
    (ht : ∀ x, ∑ s, t x s = 0) (hz : ∀ x, (Z x).traceFree)
    (hb : ∀ x, (Z x).bianchi)
    (hD : ∀ x i k j, D x i k j - D x k i j =
      rawCurvatureCommutator (t x) (einsteinCoefficient (t x) (u x)) (Z x) i k j) :
    (1 / 2 : ℝ) * (∫ x, ∑ p : Averages.CurvatureIndex,
      m x * plusCoefficient (t x) p.1.1 p.1.2 p.2.1 p.2.2 *
        matrixPairing (D x p.1.1 p.1.2 p.2.1 - D x p.1.2 p.1.1 p.2.1)
          (rawMatrixSlice (Z x).matrix p.2.2) ∂μ) =
      ∫ x, m x * ((7 / 6 : ℝ) * (∑ s, t x s ^ 2) * (Z x).squaredNorm -
…

Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.rawCurvatureCommutator, OAI.PositiveEinsteinFour.CurvatureContraction.einsteinCoefficient, OAI.PositiveEinsteinFour.Averages.CurvatureIndex, OAI.PositiveEinsteinFour.CurvatureContraction.plusCoefficient

theorem OAI.PositiveEinsteinFour.CurvatureContraction.integral_minusGreen_of_commutator line 1028
theorem OAI.PositiveEinsteinFour.CurvatureContraction.ricciGradient_self_pairing line 1049

theorem OAI.PositiveEinsteinFour.CurvatureContraction.integral_identityGreen_of_ricci line 1060

Source documentation

The scalar rough-Laplacian term is evaluated using the equation already derived from the two raw Ricci identities.

theorem integral_identityGreen_of_ricci {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (m : Ω → ℝ) (t : Ω → Fin 3 → ℝ) (Z : Ω → Tensor)
    (L : Ω → RawGradient) (ht : ∀ x, ∑ s, t x s = 0)
    (hz : ∀ x, (Z x).traceFree) (hb : ∀ x, (Z x).bianchi)
    (hL : ∀ x, L x = ricciGradient (t x) (Z x)) :
    -(∫ x, m x * rawPairing (L x) (Z x).matrix ∂μ) =
      ∫ x, m x * (-13 * (Z x).squaredNorm + 20 * diagonalGradientForm (t x) (Z x)) ∂μ := by
…

abbrev OAI.PositiveEinsteinFour.HighestHessian.DerivativeCoefficient line 1090
def OAI.PositiveEinsteinFour.HighestHessian.derivativePairing line 1092
theorem OAI.PositiveEinsteinFour.HighestHessian.matrix_pairing_comm line 1096
theorem OAI.PositiveEinsteinFour.HighestHessian.matrix_pairing_add_left line 1099
theorem OAI.PositiveEinsteinFour.HighestHessian.matrix_pairing_add_right line 1103
theorem OAI.PositiveEinsteinFour.HighestHessian.derivativePairing_add_left line 1107
theorem OAI.PositiveEinsteinFour.HighestHessian.derivativePairing_add_right line 1112
theorem OAI.PositiveEinsteinFour.HighestHessian.derivativePairing_comm line 1117
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_derivativePairing line 1134
theorem OAI.PositiveEinsteinFour.HighestHessian.derivativePairing_weightTensor line 1144
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_derivative_green line 1163
Source documentation
The unsymmetrized weight tensor gives exactly the derivative-of-weight term in the geometric Green formula, with no outer-slot symmetry premise.
```
theorem weightedQuadratic_derivative_green (A : DerivativeCoefficient)
    (hA : ∀ i k j l, A k i l j = A i k j l)
    (m : ℝ) (X : Hessian) (a : Vec) (Z : Tensor) :
    weightedQuadratic (fun W => derivativePairing A W W) m X (weightTensor a Z) =
      (∑ p : Averages.CurvatureIndex,
        (m * A p.1.1 p.1.2 p.2.1 p.2.2 *
          matrixPairing (X p.1.1 p.2.1) (X p.1.2 p.2.2) +
          a p.1.2 * A p.1.1 p.1.2 p.2.1 p.2.2 *
            matrixPairing (X p.1.1 p.2.1) (rawMatrixSlice Z.matrix p.2.2))) / 6 := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.DerivativeCoefficient, OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.derivativePairing, OAI.PositiveEinsteinFour.HighestHessian.weightTensor, OAI.PositiveEinsteinFour.Averages.CurvatureIndex
theorem OAI.PositiveEinsteinFour.HighestHessian.blockCoefficient_pair_swap line 1175
theorem OAI.PositiveEinsteinFour.HighestHessian.plusDerivativeQuadratic_eq_derivativePairing line 1185

theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_plus_green line 1208

Source documentation

The self-dual piece of the local square is precisely the normalized geometric derivative-slot Green integrand.

theorem weightedQuadratic_plus_green (t : Fin 3 → ℝ)
    (m : ℝ) (X : Hessian) (a : Vec) (Z : Tensor) :
    weightedQuadratic (plusDerivativeQuadratic t) m X (weightTensor a Z) =
      (∑ p : Averages.CurvatureIndex,
        (m * plusCoefficient t p.1.1 p.1.2 p.2.1 p.2.2 *
          matrixPairing (X p.1.1 p.2.1) (X p.1.2 p.2.2) +
          a p.1.2 * plusCoefficient t p.1.1 p.1.2 p.2.1 p.2.2 *
            matrixPairing (X p.1.1 p.2.1) (rawMatrixSlice Z.matrix p.2.2))) / 6 := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.plusDerivativeQuadratic, OAI.PositiveEinsteinFour.HighestHessian.weightTensor, OAI.PositiveEinsteinFour.Averages.CurvatureIndex

theorem OAI.PositiveEinsteinFour.HighestHessian.gradientVector_add line 1242
theorem OAI.PositiveEinsteinFour.HighestHessian.gradientVector_innerSlice line 1247
def OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing line 1255
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing_add_left line 1259
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing_add_right line 1265
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing_comm line 1271
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixSlotQuadratic_eq_matrixHessianPairing line 1277
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_matrixHessianPairing line 1292
theorem OAI.PositiveEinsteinFour.HighestHessian.gradientVector_weightTensor line 1302
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing_weightTensor line 1307

theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_matrix_green line 1319

Source documentation

Arbitrary-frame matrix form, before pointwise diagonalization.

theorem weightedQuadratic_matrix_green (A : Mat) (hA : symmetric A)
    (m : ℝ) (X : Hessian) (a : Vec) (Z : Tensor) :
    weightedQuadratic (fun W => matrixHessianPairing A W W) m X (weightTensor a Z) =
      (m * (∑ i, inner ℝ (gradientVector (X i))
          (matrixSlotOperator A (gradientVector (X i)))) +
        ∑ i, a i * inner ℝ (tensorGradientVector Z)
          (matrixSlotOperator A (gradientVector (X i)))) / 6 := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing, OAI.PositiveEinsteinFour.HighestHessian.weightTensor

theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_matrixSlot_green line 1332

Source documentation

In a single diagonal frame the local polynomial quadratic equals the same arbitrary-frame form. This assertion does not select a global frame.

theorem weightedQuadratic_matrixSlot_green
    (t : Fin 3 → ℝ) (m : ℝ) (X : Hessian)
    (hs : ∀ i j, symmetric (X i j)) (ht : ∀ i j, traceFree (X i j))
    (a : Vec) (Z : Tensor) (hz : Z.traceFree) :
    weightedQuadratic (matrixSlotQuadratic t) m X (weightTensor a Z) =
      (m * (∑ i, inner ℝ (gradientVector (X i))
          (matrixSlotOperator (Matrix.diagonal t) (gradientVector (X i)))) +
        ∑ i, a i * inner ℝ (tensorGradientVector Z)
          (matrixSlotOperator (Matrix.diagonal t) (gradientVector (X i)))) / 6 := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.matrixSlotQuadratic, OAI.PositiveEinsteinFour.HighestHessian.weightTensor

def OAI.PositiveEinsteinFour.Geometry.traceCoefficient line 1398
def OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivative line 1401
theorem OAI.PositiveEinsteinFour.Geometry.trace_coefficient_coordinates line 1405
theorem OAI.PositiveEinsteinFour.Geometry.trace_coefficient_eq line 1419
Source documentation
The trace operator applied to the derived Weyl Laplacian is six times the coefficient used in the trace Green identity.
```
theorem trace_coefficient_eq (A : Mat) (hs : symmetric A) (ht : traceFree A) :
    (4 : ℝ) • weylLaplacian A - matrixSlotAction A (weylLaplacian A) =
      (6 : ℝ) • traceCoefficient A := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotAction, OAI.PositiveEinsteinFour.Geometry.traceCoefficient
theorem OAI.PositiveEinsteinFour.Geometry.traceCurvatureBlock_weylLaplacian line 1425
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_traceCoefficient line 1440
Source documentation
Differentiate the invariant polynomial coefficient, retaining its radial derivative term.
```
theorem hasDerivAt_traceCoefficient {A : ℝ → Mat} {Z : Mat} {r : ℝ}
    (hA : HasDerivAt A Z r) :
    HasDerivAt (fun t => traceCoefficient (A t))
      (traceCoefficientDerivative (A r) Z) r := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.traceCoefficient, OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivative
theorem OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivative_radial line 1457
Source documentation
At positive norm the radial derivative is read off from the usual Frobenius contraction, exactly as in the scalar trace calculation.
```
theorem traceCoefficientDerivative_radial (A Z : Mat) (v p : ℝ)
    (hZ : symmetric Z) (hv : Matrix.trace (A * A) = 6 * v ^ 2)
    (hp : matrixPairing A Z = 6 * v * p) :
    traceCoefficientDerivative A Z =
      (4 + v ^ 2) • Z + (2 * v * p) • A - (10 : ℝ) • matrixSlotAction A Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivative, OAI.PositiveEinsteinFour.Geometry.matrixSlotAction
theorem OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice_gradientTensor line 1490
theorem OAI.PositiveEinsteinFour.Geometry.tensorGradientVector_gradientTensor line 1496
theorem OAI.PositiveEinsteinFour.Geometry.rawThirdLaplacian_vector line 1504
theorem OAI.PositiveEinsteinFour.Geometry.metric_ricci_gradient line 1514
theorem OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian_of_raw_ricci line 1563
Source documentation
Convert the raw equation into the exact vector Laplacian used by the metric Green identity, without changing any tensor component.
```
theorem frameGradientLaplacian_of_raw_ricci (g : SmoothMetric M) (e : FrameBundle g)
    (t : Fin 3 → ℝ)
    (hraw : rawThirdLaplacian (plusWeylThirdDerivative g e.base e.frame) =
      ricciGradient t (plusGradientTensor g e.base e.frame)) :
    frameGradientLaplacian g e =
      rawGradientVector (ricciGradient t (plusGradientTensor g e.base e.frame)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.rawThirdLaplacian, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative, OAI.PositiveEinsteinFour.Geometry.plusGradientTensor, OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian, OAI.PositiveEinsteinFour.Geometry.rawGradientVector

theorem OAI.PositiveEinsteinFour.Geometry.metric_identity_contraction line 1574

Source documentation

The ordinary gradient/Laplacian contraction agrees with the scalar term used in the identity Green calculation at this frame.

theorem metric_identity_contraction (g : SmoothMetric M) (e : FrameBundle g)
    (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (hs : ∀ i, symmetric (plusWeylGradient g e.base e.frame i))
    (hz : ∀ i, traceFree (plusWeylGradient g e.base e.frame i))
    (hb : ∀ r i, gradientDivergence (plusWeylGradient g e.base e.frame) r i = 0)
    (hraw : rawThirdLaplacian (plusWeylThirdDerivative g e.base e.frame) =
      ricciGradient t (plusGradientTensor g e.base e.frame)) :
    inner ℝ (frameGradientVector g e) (frameGradientLaplacian g e) =
      13 * (plusGradientTensor g e.base e.frame).squaredNorm -
        20 * diagonalGradientForm t (plusGradientTensor g e.base e.frame) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.rawThirdLaplacian, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative, OAI.PositiveEinsteinFour.Geometry.plusGradientTensor, OAI.PositiveEinsteinFour.Geometry.frameGradientVector, OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian

def OAI.PositiveEinsteinFour.Geometry.matrixVectorMap line 1615
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_matrixVector line 1620
theorem OAI.PositiveEinsteinFour.Geometry.continuous_traceCoefficient line 1625
theorem OAI.PositiveEinsteinFour.Geometry.continuous_traceCoefficientDerivative line 1634
def OAI.PositiveEinsteinFour.Geometry.traceCoefficientVectorMap line 1649
def OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivativeVectorMap line 1653

theorem OAI.PositiveEinsteinFour.Geometry.weighted_metric_trace_green line 1663

Source documentation

Before any scalar contraction, both trace subtractions give this identity on the actual frame bundle. The coefficient is a polynomial in the actual Weyl matrix and its derivative is derived above.

theorem weighted_metric_trace_green
    (g : SmoothMetric M) {μ : Measure (FrameBundle g)}
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (φ : Fin 4 → FrameFlow g μ)
    (m : C(FrameBundle g, ℝ)) (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hT : Continuous (fun e : FrameBundle g => plusWeyl g e.base e.frame))
    (hDT : ∀ i, Continuous (fun e : FrameBundle g => plusWeylGradient g e.base e.frame i))
    (hX : ∀ i, Continuous (frameHessianSlice g i i))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((φ i).map s e))
      (dm i ((φ i).map t e)) t)
    (hTd : ∀ i t e, HasDerivAt
      (fun s => plusWeyl g ((φ i).map s e).base ((φ i).map s e).frame)
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.frameHessianSlice

theorem OAI.PositiveEinsteinFour.HighestHessian.oppositeMatrix_eq_neg_rightQuaternion line 1740
theorem OAI.PositiveEinsteinFour.HighestHessian.sum_four_two_swap line 1745
theorem OAI.PositiveEinsteinFour.HighestHessian.rightDerivativeSlotForm_matrix line 1754
theorem OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm_eq_derivativePairing line 1775
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_minus_green line 1804
theorem OAI.PositiveEinsteinFour.Geometry.trace_square_eq_six_norm_sq line 1843
theorem OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm_eq_sqrt_trace line 1856
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_normalizedBlockNorm line 1862

theorem OAI.PositiveEinsteinFour.Geometry.matrixPairing_eq_radial_derivative line 1887

Source documentation

The radial coefficient needed by the trace Green formula is forced by the derivative of the actual norm, rather than supplied independently.

theorem matrixPairing_eq_radial_derivative {A : ℝ → Mat} {Z : Mat} {r p : ℝ}
    (hA : HasDerivAt A Z r) (hs : ∀ t, symmetric (A t)) (hZ : symmetric Z)
    (hv : 0 < normalizedBlockNorm (A r))
    (hp : HasDerivAt (fun t => normalizedBlockNorm (A t)) p r) :
    matrixPairing (A r) Z = 6 * normalizedBlockNorm (A r) * p := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm

def OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient line 1918
Source documentation
The uncompressed Ricci right side in an arbitrary frame. The first coefficient is 6 + 3; the remaining two terms are the differentiated matrix equation and the full bundle curvature contribution.
```
def invariantRicciGradient (A : Mat) (Z : Angular.Gradient) : Angular.Gradient :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient
theorem OAI.PositiveEinsteinFour.Geometry.third_laplacian_eq_invariantRicciGradient line 1922

theorem OAI.PositiveEinsteinFour.Geometry.metric_invariant_ricci_gradient line 1966

Source documentation

The actual Ricci equation uses just the ordinary covariant slot identities and parallel differentiation. In particular it has no choice of eigenframe among its hypotheses.

theorem metric_invariant_ricci_gradient
    (g : SmoothMetric M) (h : WeylCovariantIdentities g)
    {μ : Measure (FrameBundle g)} (φ : Fin 4 → FrameFlow g μ)
    (hT : ∀ k r e, HasDerivAt
      (fun s => plusWeyl g ((φ k).map s e).base ((φ k).map s e).frame)
      (plusWeylGradient g ((φ k).map r e).base ((φ k).map r e).frame k) r)
    (hX : ∀ k i r e, HasDerivAt
      (fun s => plusWeylHessian g ((φ k).map s e).base ((φ k).map s e).frame i i)
      (plusWeylThirdDerivative g ((φ k).map r e).base ((φ k).map r e).frame k i i) r)
    (e : FrameBundle g) (R : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ)
    (hb : ∀ r i, gradientDivergence (plusWeylGradient g e.base e.frame) r i = 0)
    (hinner : ∀ i k j,
…

theorem OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian_of_invariant_ricci line 2003
Source documentation
Conversion to the Euclidean vector used in the actual Green formula.
```
theorem frameGradientLaplacian_of_invariant_ricci
    (g : SmoothMetric M) (e : FrameBundle g)
    (hraw : (fun j => ∑ i, plusWeylThirdDerivative g e.base e.frame i i j) =
      invariantRicciGradient (plusWeyl g e.base e.frame)
        (plusWeylGradient g e.base e.frame)) :
    frameGradientLaplacian g e = gradientVector
      (invariantRicciGradient (plusWeyl g e.base e.frame)
        (plusWeylGradient g e.base e.frame)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative, OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian, OAI.PositiveEinsteinFour.Geometry.gradientVector
def OAI.PositiveEinsteinFour.Geometry.regularizedBlockNorm line 2039
def OAI.PositiveEinsteinFour.Geometry.regularizedRadialDerivative line 2042
def OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeight line 2045
def OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeightDerivative line 2048
theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeightDerivative_add line 2053

theorem OAI.PositiveEinsteinFour.Geometry.regularized_weight_cost_polarization line 2063

Source documentation

Mixed entries of the quadratic cost reduce to the diagonal costs of two directions and their sum, which suffices for the integral limit.

theorem regularized_weight_cost_polarization (ε : ℝ) (A B Z₁ Z₂ V₁ V₂ : Mat) :
    2 * regularizedWeylWeightDerivative ε A B Z₁ V₁ *
        regularizedWeylWeightDerivative ε A B Z₂ V₂ / regularizedWeylWeight ε A B =
      (regularizedWeylWeightDerivative ε A B (Z₁ + Z₂) (V₁ + V₂) ^ 2 -
        regularizedWeylWeightDerivative ε A B Z₁ V₁ ^ 2 -
        regularizedWeylWeightDerivative ε A B Z₂ V₂ ^ 2) / regularizedWeylWeight ε A B := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeightDerivative, OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeight

theorem OAI.PositiveEinsteinFour.Geometry.regularizedBlockNorm_zero line 2072
theorem OAI.PositiveEinsteinFour.Geometry.regularizedBlockNorm_pos line 2076
theorem OAI.PositiveEinsteinFour.Geometry.norm_le_regularizedBlockNorm line 2081
theorem OAI.PositiveEinsteinFour.Geometry.regularizedBlockNorm_le line 2087
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedBlockNorm line 2092
theorem OAI.PositiveEinsteinFour.Geometry.continuous_normalizedBlockNorm line 2097
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedBlockNorm line 2103
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedRadialDerivative line 2110
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedWeylWeight line 2121
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedWeylWeightDerivative line 2127
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedRadialDerivative line 2138
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedWeylWeight line 2147
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedWeylWeightDerivative line 2154
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedBlockNorm line 2164
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedWeylWeight line 2190
theorem OAI.PositiveEinsteinFour.Geometry.regularized_weight_factor_lower line 2203
theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeight_pos line 2212
theorem OAI.PositiveEinsteinFour.Geometry.matrixPairing_self_norm line 2219
theorem OAI.PositiveEinsteinFour.Geometry.abs_trace_mul_le_norm line 2225
theorem OAI.PositiveEinsteinFour.Geometry.abs_regularizedRadialDerivative_le line 2239
Source documentation
The regularized derivative has a bound independent of the smoothing parameter. This is the domination needed at Weyl zeros.
```
theorem abs_regularizedRadialDerivative_le (ε : ℝ) (hε : 0 < ε)
    (A Z : Mat) (hZ : symmetric Z) :
    |regularizedRadialDerivative ε A Z| ≤ normalizedBlockNorm Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.regularizedRadialDerivative, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm
theorem OAI.PositiveEinsteinFour.Geometry.regularized_weight_factor_upper line 2252
theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeight_bounds line 2261
theorem OAI.PositiveEinsteinFour.Geometry.abs_regularizedWeylWeightDerivative_le line 2269
theorem OAI.PositiveEinsteinFour.Geometry.regularized_weight_cost_le line 2292
abbrev OAI.PositiveEinsteinFour.QuaternionFrame.ThreeSpace line 2327
def OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix line 2330
Source documentation
Matrix of a three-dimensional orthogonal change in the fixed Euclidean basis.
```
def frameMatrix (φ : ThreeSpace ≃ₗᵢ[ℝ] ThreeSpace) : Mat :=
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.ThreeSpace
theorem OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix_one line 2334
theorem OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix_mul line 2337
theorem OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix_apply line 2341
theorem OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix_orthogonal line 2347
theorem OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix_axisReflection line 2357
theorem OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix_orthogonalReflection line 2365
theorem OAI.PositiveEinsteinFour.QuaternionFrame.normalized_span line 2373
theorem OAI.PositiveEinsteinFour.QuaternionFrame.reflection_has_signed_lift line 2380
Source documentation
Each reflection used by Cartan--Dieudonné has a concrete quaternion lift after multiplying its three-dimensional matrix by a common sign.
```
theorem reflection_has_signed_lift (v : ThreeSpace) :
    ∃ c : ℝ, c ^ 2 = 1 ∧ Nonempty
      (QuaternionLift quaternionMatrix Angular.oppositeMatrix
        (c • frameMatrix (Submodule.reflection (ℝ ∙ v)ᗮ))) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.ThreeSpace, OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix
theorem OAI.PositiveEinsteinFour.QuaternionFrame.signed_matrix_mul line 2409
theorem OAI.PositiveEinsteinFour.QuaternionFrame.reflection_list_has_signed_lift line 2413
theorem OAI.PositiveEinsteinFour.QuaternionFrame.exists_signed_left_lift line 2434
Source documentation
Every orthogonal spectral basis admits the required oriented four-frame lift. The common sign disappears from conjugation of the Weyl matrix.
```
theorem exists_signed_left_lift (φ : ThreeSpace ≃ₗᵢ[ℝ] ThreeSpace) :
    ∃ c : ℝ, c ^ 2 = 1 ∧ Nonempty
      (QuaternionLift quaternionMatrix Angular.oppositeMatrix (c • frameMatrix φ)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.ThreeSpace, OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix
theorem OAI.PositiveEinsteinFour.QuaternionFrame.signed_conjugation line 2443
Source documentation
The harmless sign in the lifted three-dimensional basis cancels from both matrix slots, exactly as needed for diagonalization.
```
theorem signed_conjugation (c : ℝ) (hc : c ^ 2 = 1) (R A : Mat) :
    (c • R)ᵀ * A * (c • R) = Rᵀ * A * R := by
…
```
theorem OAI.PositiveEinsteinFour.QuaternionFrame.matrix_spectral_square line 2450
theorem OAI.PositiveEinsteinFour.QuaternionFrame.exists_spectral_shape line 2469
Source documentation
A nonzero symmetric trace-free Weyl block has the paper's normalized shape in an actual orthogonal eigenbasis.
```
theorem exists_spectral_shape (A : Mat) (hA : symmetric A) (ht : traceFree A)
    (hv : 0 < normalizedBlockNorm A) :
    ∃ φ : ThreeSpace ≃ₗᵢ[ℝ] ThreeSpace, ∃ S : Shape,
      (frameMatrix φ)ᵀ * A * frameMatrix φ =
        Matrix.diagonal (fun i => normalizedBlockNorm A * S.s i) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.ThreeSpace, OAI.PositiveEinsteinFour.QuaternionFrame.frameMatrix
theorem OAI.PositiveEinsteinFour.QuaternionFrame.exists_lifted_spectral_shape line 2518
Source documentation
The local spectral shape is realized by a genuine oriented four-dimensional quaternion lift. The possible global sign on the three-dimensional eigenbasis cancels from both matrix slots.
```
theorem exists_lifted_spectral_shape (A : Mat) (hA : symmetric A) (ht : traceFree A)
    (hv : 0 < normalizedBlockNorm A) :
    ∃ R : Mat, Rᵀ * R = 1 ∧
      Nonempty (QuaternionLift quaternionMatrix Angular.oppositeMatrix R) ∧
      ∃ S : Shape, Rᵀ * A * R =
        Matrix.diagonal (fun i => normalizedBlockNorm A * S.s i) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix
def OAI.PositiveEinsteinFour.Geometry.matrixEntryMap line 2552
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_matrixEntry line 2557
theorem OAI.PositiveEinsteinFour.Geometry.symmetric_of_hasDerivAt line 2562
theorem OAI.PositiveEinsteinFour.Geometry.traceFree_of_hasDerivAt line 2571
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_gradientDivergence line 2578
theorem OAI.PositiveEinsteinFour.Geometry.gradientDivergence_of_hasDerivAt line 2585
theorem OAI.PositiveEinsteinFour.Geometry.hessian_divergence_eq line 2597
def OAI.PositiveEinsteinFour.Geometry.frameLaplacianMatrix line 2608
theorem OAI.PositiveEinsteinFour.Geometry.frameLaplacianMatrix_constraints line 2613
Source documentation
All three constraints follow from differentiating the corresponding Hessian identities along parallel frame flow; none is an extra Ricci input.
```
theorem frameLaplacianMatrix_constraints
    (g : SmoothMetric M) (h : WeylCovariantIdentities g)
    {μ : Measure (FrameBundle g)} (φ : Fin 4 → FrameFlow g μ)
    (hX : ∀ i j t e, HasDerivAt
      (fun s => plusWeylHessian g ((φ i).map s e).base ((φ i).map s e).frame i j)
      (plusWeylThirdDerivative g ((φ i).map t e).base ((φ i).map t e).frame i i j) t)
    (e : FrameBundle g) :
    (∀ j, symmetric (frameLaplacianMatrix g e j)) ∧
    (∀ j, traceFree (frameLaplacianMatrix g e j)) ∧
    (∀ a b, gradientDivergence (frameLaplacianMatrix g e) a b = 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.WeylCovariantIdentities, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative, OAI.PositiveEinsteinFour.Geometry.frameLaplacianMatrix, OAI.PositiveEinsteinFour.Geometry.gradientDivergence
def OAI.PositiveEinsteinFour.Geometry.weylGradientEnergy line 2679
def OAI.PositiveEinsteinFour.Geometry.weylMatrixEnergy line 2682
def OAI.PositiveEinsteinFour.Geometry.weylRadialSquare line 2685
theorem OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivative_pairing line 2688
theorem OAI.PositiveEinsteinFour.Geometry.traceCoefficientDerivative_sum line 2703
theorem OAI.PositiveEinsteinFour.Geometry.weylRadialSquare_eq_norm_gradient line 2715

theorem OAI.PositiveEinsteinFour.Geometry.weighted_metric_trace_scalar line 2728

Source documentation

The actual trace subtraction gives the scalar term of the weighted Hessian estimate in every frame, including at Weyl zeros.

theorem weighted_metric_trace_scalar
    (g : SmoothMetric M) {μ : Measure (FrameBundle g)}
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (φ : Fin 4 → FrameFlow g μ)
    (m : C(FrameBundle g, ℝ)) (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hT : Continuous (fun e : FrameBundle g => plusWeyl g e.base e.frame))
    (hDT : ∀ i, Continuous (fun e : FrameBundle g => plusWeylGradient g e.base e.frame i))
    (hX : ∀ i, Continuous (frameHessianSlice g i i))
    (hsT : ∀ e : FrameBundle g, symmetric (plusWeyl g e.base e.frame))
    (hsZ : ∀ e : FrameBundle g, ∀ i, symmetric (plusWeylGradient g e.base e.frame i))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((φ i).map s e))
      (dm i ((φ i).map t e)) t)
…

theorem OAI.PositiveEinsteinFour.Geometry.quaternion_skew_sum line 2785
theorem OAI.PositiveEinsteinFour.Geometry.bundleCurvatureAction_general_sum line 2795
Source documentation
The full bundle term is the unweighted Bianchi coupling plus the mixed action of the entire symmetric matrix.
```
theorem bundleCurvatureAction_general_sum (A : Mat) (Z : Tensor)
    (j : Fin 4) (a b : Fin 3) :
    2 * (∑ i, bundleCurvatureAction A i j (rawMatrixSlice Z.matrix i) a b) =
      -(rawCoupling Z.matrix a b j + generalMixedAction A Z.matrix a b j) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice
theorem OAI.PositiveEinsteinFour.Geometry.generalMatrixAction_diagonal line 2842
Source documentation
The arbitrary coefficient action specializes to the earlier diagonal formula without changing the underlying matrix-slot operator.
```
theorem generalMatrixAction_diagonal (t : Fin 3 → ℝ) (Z : Tensor) :
    generalMatrixAction (Matrix.diagonal t) Z.matrix = rawMatrixCurvature t Z := by
…
```

theorem OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient_compressed line 2852

Source documentation

The actual invariant Ricci right side is the compressed expression 13Z−20P(B_F(A)Z), as an equality of all matrix and tangent entries.

theorem invariantRicciGradient_compressed (A : Mat)
    (hA : symmetric A) (hAt : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    invariantRicciGradient A (fun j => rawMatrixSlice Z.matrix j) =
      fun j => rawMatrixSlice ((13 : ℝ) • Z.matrix -
        (20 : ℝ) • rawBianchiProjection (generalMatrixAction A Z.matrix)) j := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient, OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice

theorem OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient_pairing line 2878
Source documentation
The coefficient 20 holds against every genuine Bianchi test tensor in an arbitrary frame. This is the bilinear form needed by both scalar and varying matrix-slot Green identities.
```
theorem invariantRicciGradient_pairing (A : Mat)
    (hA : symmetric A) (hAt : traceFree A)
    (Z W : Tensor) (hz : Z.traceFree) (hbz : Z.bianchi) (hbw : W.bianchi) :
    inner ℝ (gradientVector (invariantRicciGradient A
      (fun j => rawMatrixSlice Z.matrix j))) (tensorGradientVector W) =
      13 * rawPairing Z.matrix W.matrix -
        20 * rawPairing (generalMatrixAction A Z.matrix) W.matrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.gradientVector, OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient, OAI.PositiveEinsteinFour.Geometry.rawMatrixSlice, OAI.PositiveEinsteinFour.Geometry.tensorGradientVector
def OAI.PositiveEinsteinFour.Geometry.ricciCompressionTensor line 2892
theorem OAI.PositiveEinsteinFour.Geometry.ricciCompressionTensor_matrix line 2896
theorem OAI.PositiveEinsteinFour.Geometry.ricciCompressionTensor_bianchi line 2902

theorem OAI.PositiveEinsteinFour.Geometry.compressed_energy_of_bianchi_ricci line 2913

Source documentation

A Bianchi rough Laplacian is enough to identify the compression energy. No separate assertion that the projector has the desired range is needed.

theorem compressed_energy_of_bianchi_ricci (A : Mat) (Z L : Tensor)
    (hZ : Z.bianchi) (hL : L.bianchi)
    (hRicci : L.matrix = (13 : ℝ) • Z.matrix -
      (20 : ℝ) • rawBianchiProjection (generalMatrixAction A Z.matrix)) :
    rawPairing (generalMatrixAction A Z.matrix)
      (rawBianchiProjection (generalMatrixAction A Z.matrix)) =
        rawPairing (rawBianchiProjection (generalMatrixAction A Z.matrix))
          (rawBianchiProjection (generalMatrixAction A Z.matrix)) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_generalTensor line 2932
Source documentation
The concrete vector-valued matrix action is the bounded matrix-slot operator used in the metric Green identity.
```
theorem matrixSlotOperator_generalTensor (A : Mat) (Z : Tensor) (hz : Z.traceFree) :
    matrixSlotOperator A (tensorGradientVector Z) =
      rawGradientVector (generalMatrixAction A Z.matrix) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.tensorGradientVector, OAI.PositiveEinsteinFour.Geometry.rawGradientVector
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_general_pairing line 2944

theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_laplacian_pairing line 2952

Source documentation

The varying-operator Green main term has the coefficient 20 times the true compression norm, once the actual rough Laplacian is Bianchi.

theorem matrixSlot_laplacian_pairing (A : Mat) (Z L : Tensor)
    (hz : Z.traceFree) (hZ : Z.bianchi) (hL : L.bianchi)
    (hRicci : L.matrix = (13 : ℝ) • Z.matrix -
      (20 : ℝ) • rawBianchiProjection (generalMatrixAction A Z.matrix)) :
    inner ℝ (tensorGradientVector L) (matrixSlotOperator A (tensorGradientVector Z)) =
      13 * rawPairing (generalMatrixAction A Z.matrix) Z.matrix -
        20 * rawPairing (rawBianchiProjection (generalMatrixAction A Z.matrix))
          (rawBianchiProjection (generalMatrixAction A Z.matrix)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.tensorGradientVector, OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_kappa_comp line 2989
theorem OAI.PositiveEinsteinFour.Geometry.continuous_kappa line 3017
theorem OAI.PositiveEinsteinFour.Geometry.continuous_kappaV line 3021
theorem OAI.PositiveEinsteinFour.Geometry.continuous_kappaB line 3025
theorem OAI.PositiveEinsteinFour.Geometry.kappa_rectangle_bound line 3029
def OAI.PositiveEinsteinFour.Geometry.regularizedKappa line 3048
def OAI.PositiveEinsteinFour.Geometry.regularizedKappaDerivative line 3051
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedKappa line 3057
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedKappaDerivative line 3064
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedKappa line 3075
theorem OAI.PositiveEinsteinFour.Geometry.regularizedNorm_rectangle line 3083
theorem OAI.PositiveEinsteinFour.Geometry.regularizedKappa_bounds line 3093
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedKappa line 3118
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedKappaDerivative line 3124
structure OAI.PositiveEinsteinFour.Geometry.MetricGreenData line 3169
Source documentation
Petersen's tensor commutators and ordinary differentiation in parallel frames, with Brin--Karcher measure-preserving flows. Ricci is normalized to 3g; the last two curvature entries are reversed for the covector action. The normalization of an arbitrary Einstein metric is separate.
```
structure MetricGreenData (g : SmoothMetric M) (μ : Measure (FrameBundle g)) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.gradientConstraints line 3212
Source documentation
Matrix symmetry and trace constraints on the first derivative are consequences of parallel differentiation of the actual Weyl block.
```
theorem gradientConstraints (d : MetricGreenData g μ) (e : FrameBundle g) :
    (∀ i, symmetric (plusWeylGradient g e.base e.frame i)) ∧
    (∀ i, traceFree (plusWeylGradient g e.base e.frame i)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.laplacianConstraints line 3227
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.ricciGradient line 3234
def OAI.PositiveEinsteinFour.Geometry.gradientVectorMap line 3245
Source documentation
Reindexing the derivative and matrix components is continuous.
```
def gradientVectorMap : (Fin 4 → Mat) →L[ℝ] GradientVector :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.GradientVector
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_gradientVector line 3250
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.laplacianVector line 3259
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousGradientVector line 3266
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousHessianVector line 3270
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousThirdVector line 3274
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.derivativeGradientVector line 3278
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.derivativeHessianVector line 3284
def OAI.PositiveEinsteinFour.Geometry.frameRegularizedWeight line 3316
def OAI.PositiveEinsteinFour.Geometry.frameRegularizedWeightDerivative line 3323

theorem OAI.PositiveEinsteinFour.Geometry.frameRegularizedWeight_hasDerivAt line 3336

Source documentation

The derivative assumption on a Green weight follows from ordinary parallel-frame differentiation of the two Weyl blocks.

theorem frameRegularizedWeight_hasDerivAt
    (g : SmoothMetric M) {μ : Measure (FrameBundle g)} (φ : Fin 4 → FrameFlow g μ)
    (ε : ℝ) (hε : 0 < ε)
    (hT : Continuous (fun e : FrameBundle g => plusWeyl g e.base e.frame))
    (hU : Continuous (fun e : FrameBundle g => minusWeyl g e.base e.frame))
    (hZ : ∀ i, Continuous (fun e : FrameBundle g => plusWeylGradient g e.base e.frame i))
    (hV : ∀ i, Continuous (fun e : FrameBundle g => minusWeylGradient g e.base e.frame i))
    (hsT : ∀ e : FrameBundle g, symmetric (plusWeyl g e.base e.frame))
    (hsU : ∀ e : FrameBundle g, symmetric (minusWeyl g e.base e.frame))
    (hdT : ∀ i t e, HasDerivAt
      (fun s => plusWeyl g ((φ i).map s e).base ((φ i).map s e).frame)
      (plusWeylGradient g ((φ i).map t e).base ((φ i).map t e).frame i) t)
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.minusWeylGradient

theorem OAI.PositiveEinsteinFour.Geometry.frameRegularizedWeight_pos line 3358
theorem OAI.PositiveEinsteinFour.Geometry.integral_regularizedWeight_tendsto line 3388
theorem OAI.PositiveEinsteinFour.Geometry.integral_regularizedWeightDerivative_tendsto line 3411

theorem OAI.PositiveEinsteinFour.Geometry.integral_regularizedWeightCost_tendsto line 3445

Source documentation

The quadratic weight cost also passes to the limit, with a bound independent of the regularization parameter.

theorem integral_regularizedWeightCost_tendsto
    (A B Z V : Ω → Mat) (F : Ω → ℝ)
    (hA : Continuous A) (hB : Continuous B) (hZ : Continuous Z) (hV : Continuous V)
    (hF : Continuous F) (hsZ : ∀ x, symmetric (Z x)) (hsV : ∀ x, symmetric (V x))
    (hpinch : ∀ x, normalizedBlockNorm (A x) + normalizedBlockNorm (B x) < 2)
    (ε : ℕ → ℝ) (hε : ∀ n, 0 < ε n) (he : ∀ n, ε n ≤ 1 / 3)
    (hlim : Tendsto ε atTop (𝓝 0)) :
    Tendsto (fun n => ∫ x,
      regularizedWeylWeightDerivative (ε n) (A x) (B x) (Z x) (V x) ^ 2 /
        regularizedWeylWeight (ε n) (A x) (B x) * F x ∂μ) atTop
      (𝓝 (∫ x, regularizedWeylWeightDerivative 0 (A x) (B x) (Z x) (V x) ^ 2 /
        regularizedWeylWeight 0 (A x) (B x) * F x ∂μ)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeightDerivative, OAI.PositiveEinsteinFour.Geometry.regularizedWeylWeight

def OAI.PositiveEinsteinFour.CurvatureContraction.generalGradientForm line 3508
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalGradientForm_diagonal line 3511
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_add line 3516
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_smul line 3522
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_one line 3528
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_self_pairing line 3534
theorem OAI.PositiveEinsteinFour.CurvatureContraction.rawCoupling_self_pairing line 3540
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_square_pairing line 3548

theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_linear_square_pairing line 3565

Source documentation

This is the full bundle polynomial before adding the covector curvature. It is an arbitrary-matrix identity on the actual Bianchi gradient.

theorem generalMixedAction_linear_square_pairing (A : Mat)
    (hs : symmetric A) (ht : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    -(1 / 2 : ℝ) * rawPairing (generalMixedAction (A + A * A) Z.matrix) Z.matrix =
      (2 / 3 : ℝ) * Matrix.trace (A * A) * Z.squaredNorm -
        4 * generalGradientForm A Z - 4 * generalGradientForm (traceFreeSquare A) Z := by
…

Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.generalGradientForm

def OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient line 3577
Source documentation
Both matrix indices are kept in the actual curvature coefficient.
```
def generalCoefficient (Q : Fin 3 → Mat4) (A : Mat)
    (i k j l : Fin 4) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_eq_blockTensor line 3581
theorem OAI.PositiveEinsteinFour.CurvatureContraction.sum_four_swap line 3593
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_oneForm line 3601
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_plus_oneForm line 3627
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_minus_oneForm line 3632
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixPairing_bundle_general line 3652

theorem OAI.PositiveEinsteinFour.CurvatureContraction.weighted_bundle_general_pairing line 3665

Source documentation

The two-form contraction is performed before the remaining matrix-bundle action, so no diagonalization is used.

theorem weighted_bundle_general_pairing (K : Fin 4 → Fin 4 → ℝ)
    (b : Fin 3 → ℝ)
    (hK : ∀ r, (∑ i, ∑ k, K i k * quaternionMatrix r i k) = b r)
    (A : Mat) (N P : Mat) :
    (∑ i, ∑ k, K i k * matrixPairing (bundleCurvatureAction A i k N) P) =
      (1 / 2 : ℝ) * ∑ r, b r *
        (matrixPairing (matrixAction r N) P +
          ∑ s, A r s * matrixPairing (matrixAction s N) P) := by
…

theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_bundle_pairing line 3708
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_minus_bundle_pairing line 3725
theorem OAI.PositiveEinsteinFour.CurvatureContraction.symmetric_product_expansion line 3733

theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_bundle_general_pairing line 3743

Source documentation

The product of the full Weyl block with the curvature connection produces exactly A+A².

theorem plus_bundle_general_pairing (A : Mat) (hs : symmetric A)
    (j l : Fin 4) (N P : Mat) :
    (∑ i, ∑ k, generalCoefficient quaternionMatrix A i k j l *
      matrixPairing (bundleCurvatureAction A i k N) P) =
      ∑ r, ∑ s, (A + A * A) r s * quaternionMatrix r j l *
        matrixPairing (matrixAction s N) P := by
…

Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient

theorem OAI.PositiveEinsteinFour.CurvatureContraction.quaternion_pairing_sum_general line 3753
theorem OAI.PositiveEinsteinFour.CurvatureContraction.matrixAction_mixed_slices_pairing line 3767
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalMixedAction_pairing_sum line 3776
def OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction line 3785
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction_plus line 3792
Source documentation
The complete bundle half-commutator in an arbitrary orthonormal frame.
```
theorem generalBundleGreenContraction_plus (A : Mat) (hs : symmetric A) (Z : Tensor) :
    generalBundleGreenContraction (generalCoefficient quaternionMatrix A) A Z =
      -(1 / 2 : ℝ) * rawPairing (generalMixedAction (A + A * A) Z.matrix) Z.matrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction_minus line 3819
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction_polynomial line 3824
theorem OAI.PositiveEinsteinFour.CurvatureContraction.clifford_column_pairing line 3833

theorem OAI.PositiveEinsteinFour.CurvatureContraction.symmetric_clifford_column_contraction line 3851

Source documentation

A symmetric coefficient contracts the Clifford product to its trace. This includes all off-diagonal matrix entries.

theorem symmetric_clifford_column_contraction
    (Q : Fin 3 → Mat4)
    (hskew : ∀ s, (Q s)ᵀ = -Q s)
    (hanti : ∀ r s, Q r * Q s + Q s * Q r =
      (if r = s then (-2 : ℝ) else 0) • (1 : Mat4))
    (C : Mat) (hC : symmetric C) (l h : Fin 4) :
    (∑ r, ∑ s, C r s * (∑ j, Q r j l * Q s j h)) =
      Matrix.trace C * (if l = h then 1 else 0) := by
…

theorem OAI.PositiveEinsteinFour.CurvatureContraction.pair_generalCoefficient line 3882
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_pairing line 3899
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_pairing_zero line 3911
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient_ricci line 3934
theorem OAI.PositiveEinsteinFour.CurvatureContraction.transpose_mul_one_add line 3954
theorem OAI.PositiveEinsteinFour.CurvatureContraction.symmetric_add_square line 3959

theorem OAI.PositiveEinsteinFour.CurvatureContraction.plus_generalCoefficient_ricci line 3969

Source documentation

The covector contraction of the full plus block gives its squared matrix norm, including all off-diagonal entries.

theorem plus_generalCoefficient_ricci (A U : Mat)
    (hs : symmetric A) (ht : traceFree A) (l h : Fin 4) :
    (1 / 2 : ℝ) * (∑ j, ∑ i, ∑ k, generalCoefficient quaternionMatrix A i k j l *
      (generalCoefficient quaternionMatrix (1 + A) i k j h +
        generalCoefficient Angular.oppositeMatrix (1 + U) i k j h)) =
      (Matrix.trace (A * A) / 2) * (if l = h then 1 else 0) := by
…

Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient, OAI.PositiveEinsteinFour.Angular.oppositeMatrix

theorem OAI.PositiveEinsteinFour.CurvatureContraction.oppositeMatrix_transpose line 3990
theorem OAI.PositiveEinsteinFour.CurvatureContraction.minus_generalCoefficient_ricci line 3997
def OAI.PositiveEinsteinFour.CurvatureContraction.generalEinsteinCoefficient line 4021
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalEinsteinCoefficient_eq_tensor line 4025
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCovectorGreenContraction_plus line 4031
theorem OAI.PositiveEinsteinFour.CurvatureContraction.generalCovectorGreenContraction_minus line 4042
theorem OAI.PositiveEinsteinFour.CurvatureContraction.general_plus_green_polynomial line 4055
Source documentation
Both actual curvature actions in the plus derivative Green term, with the full symmetric Weyl coefficient matrix.
```
theorem general_plus_green_polynomial (A U : Mat)
    (hs : symmetric A) (ht : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    generalBundleGreenContraction (generalCoefficient quaternionMatrix A) A Z +
      covectorGreenContraction (generalCoefficient quaternionMatrix A)
        (generalEinsteinCoefficient A U) Z =
      (7 / 6 : ℝ) * Matrix.trace (A * A) * Z.squaredNorm -
        4 * generalGradientForm A Z - 4 * generalGradientForm (traceFreeSquare A) Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.covectorGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.generalEinsteinCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.generalGradientForm
theorem OAI.PositiveEinsteinFour.CurvatureContraction.general_minus_green_polynomial line 4067
def OAI.PositiveEinsteinFour.CurvatureContraction.generalRawCurvatureCommutator line 4079
Source documentation
The two raw curvature actions in the commutator of a covariant Weyl gradient, with an arbitrary matrix in the Weyl bundle slot.
```
def generalRawCurvatureCommutator (A : Mat)
    (R : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ) (Z : Tensor)
    (i k j : Fin 4) : Mat :=
…
```
theorem OAI.PositiveEinsteinFour.CurvatureContraction.sum_last_first_general line 4085
theorem OAI.PositiveEinsteinFour.CurvatureContraction.general_rawGreen_decomposition line 4104
Source documentation
The actual raw commutator contracts to the already computed bundle and covector terms before any scalar estimate is applied.
```
theorem general_rawGreen_decomposition
    (K R : Fin 4 → Fin 4 → Fin 4 → Fin 4 → ℝ)
    (A : Mat) (Z : Tensor) :
    derivativeGreenContraction K (generalRawCurvatureCommutator A R Z) Z =
      generalBundleGreenContraction K A Z + covectorGreenContraction K R Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.derivativeGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.generalRawCurvatureCommutator, OAI.PositiveEinsteinFour.CurvatureContraction.generalBundleGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.covectorGreenContraction
theorem OAI.PositiveEinsteinFour.CurvatureContraction.general_plus_rawGreen line 4127
Source documentation
The complete self-dual raw Green contraction has the invariant polynomial required by the weighted Hessian estimate.
```
theorem general_plus_rawGreen (A U : Mat)
    (hs : symmetric A) (ht : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    derivativeGreenContraction (generalCoefficient quaternionMatrix A)
      (generalRawCurvatureCommutator A (generalEinsteinCoefficient A U) Z) Z =
      (7 / 6 : ℝ) * Matrix.trace (A * A) * Z.squaredNorm -
        4 * generalGradientForm A Z - 4 * generalGradientForm (traceFreeSquare A) Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.CurvatureContraction.derivativeGreenContraction, OAI.PositiveEinsteinFour.CurvatureContraction.generalCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.generalRawCurvatureCommutator, OAI.PositiveEinsteinFour.CurvatureContraction.generalEinsteinCoefficient, OAI.PositiveEinsteinFour.CurvatureContraction.generalGradientForm
theorem OAI.PositiveEinsteinFour.CurvatureContraction.general_minus_rawGreen line 4137
theorem OAI.PositiveEinsteinFour.Geometry.gradientVector_pairing line 4166
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_pairing line 4178
theorem OAI.PositiveEinsteinFour.Geometry.generalMatrixAction_gradientVector line 4188
theorem OAI.PositiveEinsteinFour.Geometry.generalMatrixAction_gradient_pairing line 4198
def OAI.PositiveEinsteinFour.Geometry.weylCompressionEnergy line 4210
Source documentation
The true Bianchi compression energy, before any spectral coordinates.
```
def weylCompressionEnergy (A : Mat) (Z : Angular.Gradient) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_ricci_compressed line 4214
theorem OAI.PositiveEinsteinFour.Geometry.invariant_ricci_identity_scalar line 4232
Source documentation
The identity contraction is valid without diagonalizing the Weyl block.
```
theorem invariant_ricci_identity_scalar (A : Mat) (hA : symmetric A) (hAt : traceFree A)
    (Z L : Angular.Gradient) (hZ : ∀ i, symmetric (Z i))
    (htZ : ∀ i, traceFree (Z i)) (hbZ : ∀ a b, gradientDivergence Z a b = 0)
    (hRicci : L = invariantRicciGradient A Z) :
    inner ℝ (gradientVector Z) (gradientVector L) / 6 =
      13 * weylGradientEnergy Z - 20 * weylMatrixEnergy A Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient, OAI.PositiveEinsteinFour.Geometry.gradientVector, OAI.PositiveEinsteinFour.Geometry.weylGradientEnergy, OAI.PositiveEinsteinFour.Geometry.weylMatrixEnergy

theorem OAI.PositiveEinsteinFour.Geometry.invariant_ricci_matrix_scalar line 4251

Source documentation

The normalized varying-matrix main term, with its actual projected energy and no diagonal-frame or extra compression-energy premise.

theorem invariant_ricci_matrix_scalar (A : Mat) (hA : symmetric A) (hAt : traceFree A)
    (Z L : Angular.Gradient) (hZ : ∀ i, symmetric (Z i))
    (htZ : ∀ i, traceFree (Z i)) (hbZ : ∀ a b, gradientDivergence Z a b = 0)
    (hL : ∀ i, symmetric (L i)) (hbL : ∀ a b, gradientDivergence L a b = 0)
    (hRicci : L = invariantRicciGradient A Z) :
    (-inner ℝ (gradientVector Z) (matrixSlotOperator A (gradientVector L)) +
      (1 / 2 : ℝ) * inner ℝ (gradientVector Z)
        (matrixSlotOperator (weylLaplacian A) (gradientVector Z))) / 6 =
      -10 * weylMatrixEnergy A Z - 3 * weylMatrixEnergy (traceFreeSquare A) Z +
        20 * weylCompressionEnergy A Z := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.invariantRicciGradient, OAI.PositiveEinsteinFour.Geometry.gradientVector, OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.weylMatrixEnergy, OAI.PositiveEinsteinFour.Geometry.weylCompressionEnergy

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.identityScalar line 4288
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.matrixScalar line 4298

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.identityGreen line 4326

Source documentation

The first Green integral for the metric Hessian, with the invariant first-derivative scalar substituted.

theorem identityGreen (d : MetricGreenData g μ)
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (m : C(FrameBundle g, ℝ)) (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((d.flow i).map s e))
      (dm i ((d.flow i).map t e)) t) :
    (∫ e, weightedQuadratic hessianNormSq (m e) (plusWeylHessian g e.base e.frame)
      (weightTensor (WithLp.toLp 2 (fun i => dm i e))
        (plusGradientTensor g e.base e.frame)) ∂μ) =
    ∫ e, m e * (-13 * weylGradientEnergy (plusWeylGradient g e.base e.frame) +
      20 * weylMatrixEnergy (plusWeyl g e.base e.frame)
        (plusWeylGradient g e.base e.frame)) ∂μ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusGradientTensor, OAI.PositiveEinsteinFour.Geometry.weylGradientEnergy, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.weylMatrixEnergy, OAI.PositiveEinsteinFour.Geometry.plusWeyl

def OAI.PositiveEinsteinFour.Geometry.regularizedDeficit line 4384
def OAI.PositiveEinsteinFour.Geometry.regularizedDeficitDerivative line 4387
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedDeficit line 4390
theorem OAI.PositiveEinsteinFour.Geometry.abs_regularizedDeficit_le line 4399
theorem OAI.PositiveEinsteinFour.Geometry.abs_regularizedDeficitDerivative_le line 4412
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedDeficit line 4421
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedDeficitDerivative line 4426
theorem OAI.PositiveEinsteinFour.Geometry.regularized_weight_mixed_cost_le line 4453
theorem OAI.PositiveEinsteinFour.Geometry.integral_regularizedWeightMixedCost_tendsto line 4483
theorem OAI.PositiveEinsteinFour.Geometry.derivative_zero_at_level_accPt line 4560
Source documentation
At a non-isolated point of a level set, the ordinary derivative is zero.
```
theorem derivative_zero_at_level_accPt {f : ℝ → ℝ} {x c v : ℝ}
    (hd : HasDerivAt f v x) (hx : f x = c)
    (ha : AccPt x (𝓟 {y | f y = c})) : v = 0 := by
…
```

theorem OAI.PositiveEinsteinFour.Geometry.countable_nonzero_derivative_on_level line 4569

Source documentation

Nonzero derivatives on any one level form a countable set.

theorem countable_nonzero_derivative_on_level (f df : ℝ → ℝ)
    (hd : ∀ x, HasDerivAt f (df x) x) (c : ℝ) :
    {x | f x = c ∧ df x ≠ 0}.Countable := by
…

theorem OAI.PositiveEinsteinFour.Geometry.ae_derivative_zero_on_level line 4588
Source documentation
Lebesgue almost everywhere, an ordinary derivative vanishes whenever its function lies on a specified level.
```
theorem ae_derivative_zero_on_level (f df : ℝ → ℝ)
    (hd : ∀ x, HasDerivAt f (df x) x) (c : ℝ) :
    ∀ᵐ x, f x = c → df x = 0 := by
…
```

theorem OAI.PositiveEinsteinFour.Geometry.ae_flow_derivative_zero_on_level line 4597

Source documentation

A measure-preserving flow transfers the one-dimensional level-set statement to its base measure; no measure-zero assertion is a premise.

theorem ae_flow_derivative_zero_on_level
    {Ω : Type*} [TopologicalSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]
    (μ : Measure Ω) [SFinite μ]
    (φ : ℝ → Ω ≃ᵐ Ω)
    (hφ : Continuous (fun p : ℝ × Ω => φ p.1 p.2))
    (hp : ∀ t, MeasurePreserving (φ t) μ μ)
    (f df : Ω → ℝ) (hf : Continuous f) (hdf : Continuous df)
    (hd : ∀ t x, HasDerivAt (fun s => f (φ s x)) (df (φ t x)) t)
    (c : ℝ) : ∀ᵐ x ∂μ, f x = c → df x = 0 := by
…

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.gradient_zero_ae_on_zero line 4635
Source documentation
The actual covariant Weyl gradient vanishes almost everywhere on the zero set of its block. This justifies the zero-set case in the norm-weight limit without assuming either Weyl block is everywhere nonzero.
```
theorem MetricGreenData.gradient_zero_ae_on_zero
    {g : SmoothMetric M} {μ : Measure (FrameBundle g)} [SFinite μ]
    (d : MetricGreenData g μ) :
    ∀ᵐ e ∂μ, plusWeyl g e.base e.frame = 0 →
      ∀ i, plusWeylGradient g e.base e.frame i = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient
theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_add_right line 4673
theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_smul_right line 4678
def OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm line 4694
Source documentation
The actual original curvature form, with the same contractions as the four geometric Green identities.
```
def generalOriginalCurvatureForm (A U : Mat) (X : Hessian) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HighestHessian.symmetricUnit line 4701
Source documentation
The symmetric elementary off-diagonal coefficient.
```
def symmetricUnit (r s : Fin 3) : Mat :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.symmetricMatrix_expansion line 4704
def OAI.PositiveEinsteinFour.Geometry.generalCoefficientMap line 4734
Source documentation
The coefficient is a fixed bounded linear function of the Weyl block.
```
def generalCoefficientMap (Q : Fin 3 → Mat4) (i k j l : Fin 4) : Mat →L[ℝ] ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.generalCoefficient_pair_swap line 4744
theorem OAI.PositiveEinsteinFour.Geometry.generalCoefficient_skew line 4756
theorem OAI.PositiveEinsteinFour.Geometry.generalCoefficient_divergence line 4768
theorem OAI.PositiveEinsteinFour.Geometry.inner_matrixVector_sub line 4793
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousGradientSlice line 4805
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousHessianSlice line 4809
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousThirdSlice line 4813

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusCurvatureGreen line 4820

Source documentation

The actual plus-block derivative Green integral, before selecting any pointwise spectral coordinates. The only new premise is the classical curvature-block decomposition.

theorem plusCurvatureGreen (d : MetricGreenData g μ)
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (hdecomp : ∀ e : FrameBundle g, frameCurvature g e.base e.frame =
      Angular.einsteinCurvatureTensor (plusWeyl g e.base e.frame) (minusWeyl g e.base e.frame))
    (m : C(FrameBundle g, ℝ)) (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((d.flow i).map s e))
      (dm i ((d.flow i).map t e)) t) :
    (∫ e, weightedQuadratic
      (fun X => derivativePairing
        (generalCoefficient quaternionMatrix (plusWeyl g e.base e.frame)) X X)
      (m e) (plusWeylHessian g e.base e.frame)
      (weightTensor (WithLp.toLp 2 (fun i => dm i e))
…

Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameCurvature, OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian

theorem OAI.PositiveEinsteinFour.Geometry.integral_matrix_combination line 4965

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.matrixGreen line 4998

Source documentation

The varying-matrix term has the scalar coefficients of the Hessian inequality, including its cubic correction.

theorem matrixGreen (d : MetricGreenData g μ)
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (m : C(FrameBundle g, ℝ)) (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((d.flow i).map s e))
      (dm i ((d.flow i).map t e)) t) :
    (∫ e, weightedQuadratic
      (fun X => matrixHessianPairing (plusWeyl g e.base e.frame) X X)
      (m e) (plusWeylHessian g e.base e.frame)
      (weightTensor (WithLp.toLp 2 (fun i => dm i e))
        (plusGradientTensor g e.base e.frame)) ∂μ) =
    ∫ e, m e * (-10 * weylMatrixEnergy (plusWeyl g e.base e.frame)
          (plusWeylGradient g e.base e.frame) -
…

Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusGradientTensor, OAI.PositiveEinsteinFour.Geometry.weylMatrixEnergy, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient

def OAI.PositiveEinsteinFour.Geometry.scalarCoordinates line 5103
def OAI.PositiveEinsteinFour.Geometry.scalarGradient line 5106
def OAI.PositiveEinsteinFour.Geometry.scalarHessian line 5110
def OAI.PositiveEinsteinFour.Geometry.scalarThird line 5115
def OAI.PositiveEinsteinFour.Geometry.scalarLaplacian line 5121
def OAI.PositiveEinsteinFour.Geometry.scalarGradientVector line 5124
def OAI.PositiveEinsteinFour.Geometry.scalarTraceFreeHessian line 5127
structure OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData line 5131
Source documentation
Raw classical scalar calculus, stated on the actual metric tensors.
```
structure ScalarCovariantData {g : SmoothMetric M} {μ : Measure (FrameBundle g)}
    (d : MetricGreenData g μ) (a : M → ℝ) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.MetricGreenData
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.continuousLaplacian line 5156
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.continuousGradientVector line 5159
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.derivativeLaplacian line 5162
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.third_symmetric line 5167
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.laplacianGradient_commute line 5179
def OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix line 5213
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_add line 5215
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_sub line 5219
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_smul line 5223
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_sum line 5227
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_one line 5231
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_mul line 5235
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_trace line 5245
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_transpose line 5249
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_symmetric line 5254
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_traceFree line 5262
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_pairing line 5268
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_slot line 5273
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_traceFreeSquare line 5281
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_norm line 5288
def OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient line 5300
Source documentation
Passive rotation of all three slots of a matrix-valued covector.
```
def turnGradient (R : Mat) (P : Mat4) (Z : Angular.Gradient) : Angular.Gradient :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient_symmetric line 5303
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient_traceFree line 5312
theorem OAI.PositiveEinsteinFour.QuaternionFrame.matrixPairing_comm line 5320
theorem OAI.PositiveEinsteinFour.QuaternionFrame.matrixPairing_sum_smul_right line 5323
theorem OAI.PositiveEinsteinFour.QuaternionFrame.orthogonal_sum_contraction line 5329
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient_pairing line 5347
Source documentation
Every quadratic contraction is preserved by simultaneous changes of the matrix basis and the covector basis.
```
theorem turnGradient_pairing (R : Mat) (hR : R * Rᵀ = 1)
    (P : Mat4) (hP : P * Pᵀ = 1) (Z W : Angular.Gradient) :
    (∑ i, matrixPairing (turnGradient R P Z i) (turnGradient R P W i)) =
      ∑ i, matrixPairing (Z i) (W i) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient
def OAI.PositiveEinsteinFour.Geometry.regularizedMatrixWeight line 5377
theorem OAI.PositiveEinsteinFour.Geometry.abs_regularizedMatrixWeight_le line 5382
theorem OAI.PositiveEinsteinFour.Geometry.integral_regularizedMatrixWeight_tendsto line 5407
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_frame_inner line 5482
theorem OAI.PositiveEinsteinFour.Bianchi.rawQuaternion_self_pairing line 5490
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_rawQuaternion_self line 5499
theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_matrix_pairing line 5506
theorem OAI.PositiveEinsteinFour.Bianchi.weighted_quaternion_matrix_pairing line 5518
theorem OAI.PositiveEinsteinFour.Bianchi.general_generator_energy line 5528
Source documentation
The full matrix generator energy follows from the actual one-fifth Bianchi projection and the arbitrary-matrix mixed compression.
```
theorem general_generator_energy (A : Mat) (hA : symmetric A) (htA : traceFree A)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ r, ∑ s, A r s * rawPairing (rawGradientGenerator r Z.matrix)
      (rawGradientGenerator s Z.matrix)) = -40 * generalGradientForm A Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator
theorem OAI.PositiveEinsteinFour.HighestHessian.sum_rotate_three line 5569
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing_innerSlices line 5580
Source documentation
The actual matrix-slot operator is the sum of its four inner-slice forms.
```
theorem matrixHessianPairing_innerSlices (A : Mat) (X : Hessian)
    (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j)) :
    matrixHessianPairing A X X = ∑ i, generalGradientForm A (innerSlice X i) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing, OAI.PositiveEinsteinFour.HighestHessian.innerSlice
theorem OAI.PositiveEinsteinFour.HighestHessian.general_innerAction_energy line 5591
Source documentation
The full weighted inner-generator energy uses only each slice's Bianchi identity.
```
theorem general_innerAction_energy (A : Mat) (hA : symmetric A) (htA : traceFree A)
    (X : Hessian) (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i r, divergence X i r = 0) :
    hessianGram A (fun r => innerAction r X) = -40 * matrixHessianPairing A X X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.hessianGram, OAI.PositiveEinsteinFour.HighestHessian.innerAction, OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing
def OAI.PositiveEinsteinFour.HighestHessian.generalDerivativeSlot line 5604
Source documentation
The two actual derivative slots, before taking a trace-free coefficient.
```
def generalDerivativeSlot (Q : Fin 3 → Mat4) (r s : Fin 3) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.generalDerivativeSlot_slices line 5607
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianPairing_outer_inner_cross line 5618
theorem OAI.PositiveEinsteinFour.HighestHessian.generalDerivativeSlot_inner_cross line 5627
Source documentation
Off-diagonal as well as diagonal derivative-slot compression.
```
theorem generalDerivativeSlot_inner_cross (r s : Fin 3) (X : Hessian)
    (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i t, divergence X i t = 0) :
    generalDerivativeSlot quaternionMatrix r s X =
      -(1 / 5 : ℝ) * hessianPairing (outerAction r X) (innerAction s X) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.generalDerivativeSlot, OAI.PositiveEinsteinFour.HighestHessian.outerAction, OAI.PositiveEinsteinFour.HighestHessian.innerAction
theorem OAI.PositiveEinsteinFour.HighestHessian.outerAction_pairing line 5668
theorem OAI.PositiveEinsteinFour.HighestHessian.general_outerAction_energy line 5691
theorem OAI.PositiveEinsteinFour.HighestHessian.sum_swap_last_two line 5698
theorem OAI.PositiveEinsteinFour.HighestHessian.generalDerivativePairing_eq line 5707
Source documentation
Reordering the actual derivative contraction and the two Weyl indices.
```
theorem generalDerivativePairing_eq (Q : Fin 3 → Mat4) (A : Mat) (X : Hessian) :
    derivativePairing (generalCoefficient Q A) X X =
      (1 / 2 : ℝ) * ∑ r, ∑ s, A r s * generalDerivativeSlot Q r s X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.derivativePairing, OAI.PositiveEinsteinFour.HighestHessian.generalDerivativeSlot
theorem OAI.PositiveEinsteinFour.HighestHessian.general_cross_energy line 5731
theorem OAI.PositiveEinsteinFour.HighestHessian.general_plus_energy line 5745
Source documentation
No outer-slot symmetry is required for the full-matrix plus compression.
```
theorem general_plus_energy (A : Mat) (hA : symmetric A) (htA : traceFree A)
    (X : Hessian) (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i r, divergence X i r = 0) :
    hessianGram A (fun r => totalPlus r X) =
      -40 * matrixHessianPairing A X X -
        20 * derivativePairing (generalCoefficient quaternionMatrix A) X X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.hessianGram, OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.matrixHessianPairing, OAI.PositiveEinsteinFour.HighestHessian.derivativePairing
theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_pairing_slice line 5768
theorem OAI.PositiveEinsteinFour.HighestHessian.sum_six_rotate line 5778
theorem OAI.PositiveEinsteinFour.HighestHessian.general_minus_energy_entry line 5787
theorem OAI.PositiveEinsteinFour.HighestHessian.general_minus_energy line 5820
Source documentation
The full-matrix opposite-block compression holds on every tensor.
```
theorem general_minus_energy (U : Mat) (hU : symmetric U) (htU : traceFree U)
    (X : Hessian) :
    hessianGram U (fun r => totalMinus r X) =
      -4 * derivativePairing (generalCoefficient Angular.oppositeMatrix U) X X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.hessianGram, OAI.PositiveEinsteinFour.HighestHessian.totalMinus, OAI.PositiveEinsteinFour.HighestHessian.derivativePairing, OAI.PositiveEinsteinFour.Angular.oppositeMatrix
theorem OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm_eq_of_inner_bianchi line 5848
Source documentation
Exact equality on the full inner-Bianchi space, including the unsymmetrized derivative of a scalar weight.
```
theorem generalOriginalCurvatureForm_eq_of_inner_bianchi (A U : Mat) (X : Hessian)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i r, divergence X i r = 0) :
    generalOriginalCurvatureForm A U X = generalCasimirCurvatureForm A U X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.generalCasimirCurvatureForm
def OAI.PositiveEinsteinFour.Geometry.regularizedHessianWeight line 5879
theorem OAI.PositiveEinsteinFour.Geometry.regularizedHessianWeight_bound line 5885
theorem OAI.PositiveEinsteinFour.Geometry.integral_regularizedHessianWeight_tendsto line 5913
structure OAI.PositiveEinsteinFour.Geometry.OppositeWeylData line 6013
Source documentation
The same classical first-order calculus for the opposite Weyl block, using the already specified actual parallel frame flow.
```
structure OppositeWeylData {g : SmoothMetric M} {μ : Measure (FrameBundle g)}
    (d : MetricGreenData g μ) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.MetricGreenData
theorem OAI.PositiveEinsteinFour.Geometry.oppositeMatrix_skew line 6026
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusCurvatureGreen line 6035
theorem OAI.PositiveEinsteinFour.Geometry.scalar_flow_green line 6168
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.valueField line 6183
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.gradientField line 6185
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.hessianField line 6188
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.thirdField line 6191
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.laplacianField line 6194
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.laplacianDerivativeField line 6196
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.scalar_pairing_green line 6202
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.laplacian_square_green line 6223
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.hessian_square_green line 6255
def OAI.PositiveEinsteinFour.Geometry.PetersenScalarCalculusInput line 6308
def OAI.PositiveEinsteinFour.Geometry.PetersenPoissonInput line 6311
theorem OAI.PositiveEinsteinFour.Variance.centered_product_integral line 6326
theorem OAI.PositiveEinsteinFour.QuaternionFrame.shape_exists_minimum_parameter line 6361
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_posSemidef line 6397
theorem OAI.PositiveEinsteinFour.QuaternionFrame.shape_shift_bounds line 6402
theorem OAI.PositiveEinsteinFour.QuaternionFrame.shape_minimum_parameter_bound line 6415
theorem OAI.PositiveEinsteinFour.QuaternionFrame.shape_traceCube line 6425
theorem OAI.PositiveEinsteinFour.QuaternionFrame.gradientTensor_energy line 6459
def OAI.PositiveEinsteinFour.QuaternionFrame.slotLinear line 6466
theorem OAI.PositiveEinsteinFour.QuaternionFrame.matrixSlotAction_sum_smul line 6480
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient_slot line 6488
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylGradientEnergy_turn line 6497
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylMatrixEnergy_turn line 6503
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylMatrixSquareEnergy_turn line 6515
theorem OAI.PositiveEinsteinFour.QuaternionFrame.trace_turnGradient line 6522
Source documentation
The radial trace is a covector under the same actual four-frame change.
```
theorem trace_turnGradient (R : Mat) (hR : R * Rᵀ = 1) (P : Mat4)
    (A : Mat) (Z : Angular.Gradient) (i : Fin 4) :
    Matrix.trace (conjugateMatrix R A * turnGradient R P Z i) =
      ∑ j, P j i * Matrix.trace (A * Z j) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient
theorem OAI.PositiveEinsteinFour.QuaternionFrame.orthogonal_square_sum line 6530
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylRadialSquare_turn line 6553
theorem OAI.PositiveEinsteinFour.QuaternionFrame.orthogonal_matrix_contraction line 6561
theorem OAI.PositiveEinsteinFour.QuaternionFrame.sum_squares_turnGradient line 6577
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weighted_sum_turnGradient line 6586
def OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField line 6612
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField_eq line 6615
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField_turn line 6623
Source documentation
The full cubic trace, including its distinguished covector, is preserved by the same local change of frame.
```
theorem weightedCubicField_turn (R : Mat) (hR : R * Rᵀ = 1)
    (P : Mat4) (hP : P * Pᵀ = 1) (a : Fin 4 → ℝ) (Z : Angular.Gradient) :
    weightedCubicField (fun i => ∑ k, P k i * a k) (turnGradient R P Z) =
      weightedCubicField a Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField, OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient
theorem OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm_eq line 6647

theorem OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm_lower line 6656

Source documentation

The exact coercive constant for the original Green curvature form holds in every orthonormal frame.

theorem generalOriginalCurvatureForm_lower (A U : Mat) (X : Hessian)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hX : condition X) (x y : ℝ)
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) :
    (4 - 2 * x - 2 * y) * hessianNormSq X ≤ generalOriginalCurvatureForm A U X := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm

theorem OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm_nonneg line 6667

Source documentation

Positivity includes the closed sectional boundary, with no local or global diagonalization hypothesis.

theorem generalOriginalCurvatureForm_nonneg (A U : Mat) (X : Hessian)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hX : condition X) (x y : ℝ)
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2) :
    0 ≤ generalOriginalCurvatureForm A U X := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm

theorem OAI.PositiveEinsteinFour.HighestHessian.generalCasimir_add_smul line 6676

theorem OAI.PositiveEinsteinFour.HighestHessian.generalOriginal_weighted_square line 6691

Source documentation

The local weighted square in the original arbitrary-matrix Green form, before any projection cost or global integration.

theorem generalOriginal_weighted_square (A U : Mat) (X Y : Hessian)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hX : condition X) (hY : condition Y) (x y m : ℝ) (hm : 0 < m)
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2) :
    0 ≤ weightedQuadratic (generalOriginalCurvatureForm A U) m X Y +
      generalOriginalCurvatureForm A U Y / (24 * m) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm

theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix_inverse line 6741
theorem OAI.PositiveEinsteinFour.QuaternionFrame.shape_minimum_shift_posSemidef line 6752
Source documentation
The lower bound on every normalized eigenvalue gives positive semidefiniteness at the exact minimum shift.
```
theorem shape_minimum_shift_posSemidef (A R : Mat) (hR : Rᵀ * R = 1)
    (S : Shape) (v r : ℝ) (hv : 0 ≤ v)
    (hdiag : conjugateMatrix R A = Matrix.diagonal (fun i => v * S.s i))
    (hmin : ∀ i, -r ≤ S.s i) :
    (A + (v * r) • (1 : Mat)).PosSemidef := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix

theorem OAI.PositiveEinsteinFour.QuaternionFrame.minimum_spectral_sum_le_two line 6777

Source documentation

Both constructed spectral minima remain within any admissible pair of shifts. This is precisely the parameter domain v*r+b*s<=2.

theorem minimum_spectral_sum_le_two
    (A U R T : Mat) (hR : Rᵀ * R = 1) (hT : Tᵀ * T = 1)
    (S V : Shape) (v b r s x y : ℝ)
    (hA : conjugateMatrix R A = Matrix.diagonal (fun i => v * S.s i))
    (hU : conjugateMatrix T U = Matrix.diagonal (fun i => b * V.s i))
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (hr : ∃ i, S.s i = -r) (hs : ∃ i, V.s i = -s) :
    v * r + b * s ≤ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix

def OAI.PositiveEinsteinFour.Bianchi.coordinatePairing line 6807
theorem OAI.PositiveEinsteinFour.Bianchi.coordinatePairing_comm line 6810
theorem OAI.PositiveEinsteinFour.Bianchi.reverse_coefficient_pairing line 6816
theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_eq_rawNorm line 6832
theorem OAI.PositiveEinsteinFour.Bianchi.costParameters_pairing line 6836
theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_pairing_01 line 6849
theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_pairing_02 line 6858
theorem OAI.PositiveEinsteinFour.Bianchi.coefficient_pairing_12 line 6867
theorem OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient_pairing_of_ne line 6876
theorem OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient_pairing line 6894
Source documentation
The full polarized coefficient identity, including the trace term.
```
theorem rawCostCoefficient_pairing (s t : Fin 3)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ r, rawPairing (rawCostCoefficient s r Z.matrix) (rawCostCoefficient t r Z.matrix)) =
      (if s = t then 84 * Z.squaredNorm else 0) +
        44 * rawPairing (rawGradientGenerator s Z.matrix) (rawGradientGenerator t Z.matrix) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator
theorem OAI.PositiveEinsteinFour.Geometry.OppositeWeylData.gradientConstraints line 6931
theorem OAI.PositiveEinsteinFour.Geometry.OppositeWeylData.gradient_zero_ae_on_zero line 6947
structure OAI.PositiveEinsteinFour.Geometry.PetersenOrientedNormInput line 6993
def OAI.PositiveEinsteinFour.Geometry.OrientationPreservingFlow line 7001
def OAI.PositiveEinsteinFour.Geometry.orientedNormRegularization line 7004
theorem OAI.PositiveEinsteinFour.Geometry.orientedNormRegularization_smooth line 7008
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_eq_of_frame_derivative line 7019
theorem OAI.PositiveEinsteinFour.Geometry.regularizedRadialDerivative_scale line 7039
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_sub_of_data line 7051
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_H_of_data line 7063
theorem OAI.PositiveEinsteinFour.Geometry.contMDiff_H_of_pos line 7081
theorem OAI.PositiveEinsteinFour.Geometry.PetersenOrientedNormInput.plus_regularized_gradient line 7096
theorem OAI.PositiveEinsteinFour.Geometry.PetersenOrientedNormInput.minus_regularized_gradient line 7115
def OAI.PositiveEinsteinFour.QuaternionFrame.turnVector line 7153
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnVector_add line 7155
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnVector_smul line 7161
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnVector_sum line 7170
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnVector_zero line 7177
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnVector_norm line 7181
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.quaternion_turnVector line 7190
Source documentation
The passive vector change intertwines each imaginary quaternion with its rotated linear combination.
```
theorem QuaternionLift.quaternion_turnVector {R : Mat}
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (s : Fin 3) (v : Vec) :
    quaternion s (turnVector P.matrix v) =
      turnVector P.matrix (∑ r, R r s • quaternion r v) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.turnVector
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.quaternion_row_contraction line 7228
Source documentation
Orthogonality contracts the changed quaternion row against the changed matrix row.
```
theorem QuaternionLift.quaternion_row_contraction {R : Mat}
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (hR : R * Rᵀ = 1) (r : Fin 3) (v : Vec) :
    (∑ a, R r a • quaternion a (turnVector P.matrix v)) =
      turnVector P.matrix (quaternion r v) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.turnVector
def OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient line 7244
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_field line 7247
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_symmetric line 7264
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_bianchi line 7278
Source documentation
The Bianchi constraint itself is preserved by a lifted change of frame. This is a finite contraction of the quaternion intertwining law.
```
theorem turnRawGradient_bianchi (R : Mat) (hR : R * Rᵀ = 1)
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (Z : RawGradient) (hZ : ∀ s, ∑ r, quaternion r (Z r s) = 0) (b : Fin 3) :
    (∑ a, quaternion a (turnRawGradient R P.matrix Z a b)) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient_bianchi line 7311
theorem OAI.PositiveEinsteinFour.QuaternionFrame.matrixAction_eq_commutator line 7328
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.conjugate_rotation line 7334
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.matrixAction_conjugate line 7344
Source documentation
The spin-two matrix action is the conjugation action forced by the same quaternion lift, rather than an independent representation premise.
```
theorem QuaternionLift.matrixAction_conjugate {R : Mat}
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (hR : Rᵀ * R = 1) (s : Fin 3) (M : Mat) :
    matrixAction s (conjugateMatrix R M) =
      conjugateMatrix R (∑ r, R r s • matrixAction r M) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix
theorem OAI.PositiveEinsteinFour.Geometry.traceFree_four_square line 7373
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.traceFreeHessian_symmetric line 7386
theorem OAI.PositiveEinsteinFour.Geometry.scalarTraceFreeHessian_trace line 7393
theorem OAI.PositiveEinsteinFour.Geometry.scalarTraceFreeHessian_square line 7401
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.integrated_bochner line 7412
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.coefficient_green line 7479

theorem OAI.PositiveEinsteinFour.HighestHessian.general_trace_subtracted_condition line 7540

Source documentation

Subtracting the actual matrix Weyl equation removes the complete Ricci commutator, including the skew derivative part.

theorem general_trace_subtracted_condition (A : Mat) (X : Hessian)
    (hA : symmetric A) (htA : traceFree A)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0)
    (hcomm : ∀ i j a b, X i j a b - X j i a b = bundleCurvatureAction A i j A a b) :
    condition (X - traceComponent (weylLaplacian A)) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.condition

def OAI.PositiveEinsteinFour.HighestHessian.generalMatrixActionSquare line 7576
Source documentation
The operator on a matrix obtained by contracting two infinitesimal matrix rotations with the full Weyl coefficient.
```
def generalMatrixActionSquare (A M : Mat) : Mat :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.generalMatrixActionSquare_add line 7579
theorem OAI.PositiveEinsteinFour.HighestHessian.generalMatrixActionSquare_smul line 7585
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixSlotAction_coeff_add line 7590
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixSlotAction_coeff_smul line 7597
theorem OAI.PositiveEinsteinFour.HighestHessian.generalMatrixActionSquare_diagonal line 7603
theorem OAI.PositiveEinsteinFour.HighestHessian.generalMatrixActionSquare_symmetricUnit line 7612
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixAction_cross_01 line 7619
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixAction_cross_02 line 7634
theorem OAI.PositiveEinsteinFour.HighestHessian.matrixAction_cross_12 line 7649
theorem OAI.PositiveEinsteinFour.HighestHessian.general_matrixAction_square line 7666
Source documentation
The diagonal spin-two identity extends to the full symmetric trace-free coefficient by its three off-diagonal entries.
```
theorem general_matrixAction_square (A M : Mat)
    (hA : symmetric A) (htA : traceFree A) (hM : symmetric M) (htM : traceFree M) :
    generalMatrixActionSquare A M = (24 : ℝ) • matrixSlotAction A M := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.generalMatrixActionSquare
def OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing line 7679
Source documentation
The polarized arbitrary-matrix curvature operator.
```
def generalCurvaturePairing (A U : Mat) (X Y : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_self line 7684
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedPairing_comm line 7689
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_comm line 7700
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_add_left line 7706
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_smul_left line 7713
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_add_right line 7720
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_smul_right line 7727
theorem OAI.PositiveEinsteinFour.HighestHessian.traceLift_pairing_double_sum line 7734

theorem OAI.PositiveEinsteinFour.HighestHessian.general_traceLift_curvatureAction line 7743

Source documentation

The exact trace-component action is invariant under an arbitrary symmetric trace-free Weyl coefficient.

theorem general_traceLift_curvatureAction (A U M : Mat)
    (hA : symmetric A) (htA : traceFree A) (hM : symmetric M) (htM : traceFree M)
    (Y : Hessian) :
    generalCurvaturePairing A U (traceLift M) Y =
      hessianPairing (traceLift ((4 : ℝ) • M - matrixSlotAction A M)) Y := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing

def OAI.PositiveEinsteinFour.HighestHessian.generalTraceCurvatureBlock line 7782
theorem OAI.PositiveEinsteinFour.HighestHessian.general_traceComponent_curvatureAction line 7785
theorem OAI.PositiveEinsteinFour.HighestHessian.generalTraceCurvatureBlock_symmetric line 7797
theorem OAI.PositiveEinsteinFour.HighestHessian.generalTraceCurvatureBlock_traceFree line 7816

theorem OAI.PositiveEinsteinFour.HighestHessian.general_traceComponent_curvaturePairing line 7829

Source documentation

The full trace curvature term pairs through the actual tensor trace.

theorem general_traceComponent_curvaturePairing (A U M : Mat)
    (hA : symmetric A) (htA : traceFree A) (hM : symmetric M) (htM : traceFree M)
    (X : Hessian) (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i r, divergence X i r = 0) :
    generalCurvaturePairing A U (traceComponent M) X =
      (5 / 12 : ℝ) * matrixPairing (generalTraceCurvatureBlock A M) (hessianTrace X) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.generalTraceCurvatureBlock

theorem OAI.PositiveEinsteinFour.HighestHessian.general_prescribed_trace_curvaturePairing line 7839

theorem OAI.PositiveEinsteinFour.HighestHessian.general_weighted_trace_subtraction line 7854

Source documentation

Exact trace subtraction includes the unsymmetrized weight derivative.

theorem general_weighted_trace_subtraction (A U M : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A)
    (hM : symmetric M) (htM : traceFree M)
    (X L : Hessian) (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hb : ∀ i r, divergence X i r = 0) (htrace : hessianTrace X = M) (m : ℝ) :
    m * generalCurvaturePairing A U (X - traceComponent M) (X - traceComponent M) +
        generalCurvaturePairing A U (X - traceComponent M) L =
      m * generalCurvaturePairing A U X X + generalCurvaturePairing A U X L -
        m * generalCurvaturePairing A U (traceComponent M) (traceComponent M) -
          generalCurvaturePairing A U (traceComponent M) L := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing

theorem OAI.PositiveEinsteinFour.HighestHessian.generalTraceCurvatureBlock_weylLaplacian line 7876
Source documentation
The prescribed trace is exactly the invariant polynomial coefficient already differentiated in the geometric trace Green identity.
```
theorem generalTraceCurvatureBlock_weylLaplacian (A : Mat)
    (hA : symmetric A) (htA : traceFree A) :
    generalTraceCurvatureBlock A (weylLaplacian A) = (6 : ℝ) • traceCoefficient A :=
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.generalTraceCurvatureBlock
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField_tensor line 7899
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField_smul line 7907
theorem OAI.PositiveEinsteinFour.QuaternionFrame.distinguished_matrix_symmetric line 7912
theorem OAI.PositiveEinsteinFour.QuaternionFrame.distinguished_matrix_traceFree line 7920
theorem OAI.PositiveEinsteinFour.QuaternionFrame.distinguished_matrix_turn line 7927

theorem OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField_sharp line 7936

Source documentation

Sharp cubic contraction for arbitrary symmetric trace-free Bianchi gradients and arbitrary distinguished covectors.

theorem weightedCubicField_sharp (a : Vec) (Z : Angular.Gradient)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    |weightedCubicField a Z| ≤ ‖a‖ *
      ((24 / 5 : ℝ) * Real.sqrt (3 / 5) * weylGradientEnergy Z *
        Real.sqrt (weylGradientEnergy Z)) := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField

theorem OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField_squared_weight_bound line 8012

Source documentation

The actual cubic trace with the squared-weight derivative has exactly the coefficient used in the scalar quartic relaxation.

theorem weightedCubicField_squared_weight_bound (M : ℝ) (hM : 0 ≤ M)
    (p q : Vec) (Z : Angular.Gradient)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    -(5 / 36 : ℝ) * weightedCubicField (((-(3 / 4 : ℝ) * M) • (p - q)) : Vec) Z ≤
      (1 / 2 : ℝ) * Real.sqrt (3 / 5) * (‖p‖ + ‖q‖) * M *
        (weylGradientEnergy Z * Real.sqrt (weylGradientEnergy Z)) := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField

def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.traceFreeHessianField line 8060
def OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.traceFreeHessianDerivativeField line 8068
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.derivativeTraceFreeHessian line 8076
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.traceFreeHessian_divergence line 8087
theorem OAI.PositiveEinsteinFour.Geometry.scalarTraceFreeHessian_pairing line 8099
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.weighted_traceFree_green line 8122
abbrev OAI.PositiveEinsteinFour.SectionalPlane.Vec4 line 8201
def OAI.PositiveEinsteinFour.SectionalPlane.act line 8203
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_add line 8206
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_smul line 8211
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_sum line 8216
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_mul line 8221
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_smul_vector line 8226
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_zero line 8231
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_one line 8235
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_norm line 8239
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_inner_adjoint line 8247
theorem OAI.PositiveEinsteinFour.SectionalPlane.act_skew_self line 8259
theorem OAI.PositiveEinsteinFour.SectionalPlane.exists_common_vector line 8270
Source documentation
Every pair of unit imaginary quaternions admits a common vector on which their actions are opposite. The trace-zero product makes its positive projection nonzero.
```
theorem exists_common_vector (s t : Fin 3 → ℝ)
    (hs : ∑ i, s i ^ 2 = 1) (ht : ∑ i, t i ^ 2 = 1) :
    ∃ v : Vec4, ‖v‖ = 1 ∧
      act (imaginaryCombination quaternionMatrix s) v =
        -act (imaginaryCombination oppositeMatrix t) v := by
…
```
Mentions: OAI.PositiveEinsteinFour.SectionalPlane.Vec4, OAI.PositiveEinsteinFour.SectionalPlane.act
def OAI.PositiveEinsteinFour.SectionalPlane.coefficient line 8336
theorem OAI.PositiveEinsteinFour.SectionalPlane.coefficient_eq_sum line 8338
theorem OAI.PositiveEinsteinFour.SectionalPlane.quaternion_gram line 8348
theorem OAI.PositiveEinsteinFour.SectionalPlane.opposite_gram line 8355
theorem OAI.PositiveEinsteinFour.SectionalPlane.coefficient_combination line 8363
theorem OAI.PositiveEinsteinFour.SectionalPlane.exists_two_plane line 8371
theorem OAI.PositiveEinsteinFour.HighestHessian.innerBianchi_add line 8411

theorem OAI.PositiveEinsteinFour.HighestHessian.generalOriginal_polarization line 8431

Source documentation

Polarization retains the exact full-matrix Green form on arbitrary inner-Bianchi tensors, including nonsymmetric outer derivative slots.

theorem generalOriginal_polarization (A U : Mat) (hA : symmetric A) (hU : symmetric U)
    (htA : traceFree A) (htU : traceFree U) (X Y : Hessian)
    (hmX : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbX : ∀ i r, divergence X i r = 0)
    (hmY : ∀ i j, symmetric (Y i j) ∧ traceFree (Y i j))
    (hbY : ∀ i r, divergence Y i r = 0) :
    (generalOriginalCurvatureForm A U (X + Y) - generalOriginalCurvatureForm A U X -
      generalOriginalCurvatureForm A U Y) / 2 = generalCurvaturePairing A U X Y := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing

theorem OAI.PositiveEinsteinFour.HighestHessian.general_weightedQuadratic_eq line 8450
theorem OAI.PositiveEinsteinFour.HighestHessian.generalPlus_projection_pairing line 8464
theorem OAI.PositiveEinsteinFour.HighestHessian.generalMinus_projection_pairing line 8474
theorem OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing_highestProjection line 8484

theorem OAI.PositiveEinsteinFour.HighestHessian.general_weighted_highestProjection_square line 8493

Source documentation

The local square uses the actual orthogonal projection, with arbitrary symmetric matrix coefficients and no pointwise eigenframe.

theorem general_weighted_highestProjection_square (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (X L : Hessian) (hX : condition X)
    (x y m : ℝ) (hm : 0 < m)
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2) :
    0 ≤ (m / 6) * generalCurvaturePairing A U X X +
      generalCurvaturePairing A U X L / 6 +
      generalCurvaturePairing A U (highestProjection L) (highestProjection L) / (24 * m) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection

def OAI.PositiveEinsteinFour.HighestHessian.generalTraceCorrection line 8524

theorem OAI.PositiveEinsteinFour.HighestHessian.general_local_weighted_original_square line 8530

Source documentation

The full arbitrary-frame local Hessian inequality, including the exact prescribed trace and the constructed highest-projection cost.

theorem general_local_weighted_original_square (A U M : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hM : symmetric M) (htM : traceFree M) (X L : Hessian)
    (hmX : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbX : ∀ i r, divergence X i r = 0) (htrace : hessianTrace X = M)
    (hY : condition (X - traceComponent M))
    (hmL : ∀ i j, symmetric (L i j) ∧ traceFree (L i j))
    (hbL : ∀ i r, divergence L i r = 0)
    (x y m : ℝ) (hm : 0 < m)
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2) :
    0 ≤ weightedQuadratic (generalOriginalCurvatureForm A U) m X L +
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.generalOriginalCurvatureForm

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.highestRemainder line 8575
Source documentation
Membership of the actual trace-free Hessian in the highest subspace is a theorem, rather than an additional geometric input.
```
theorem MetricGreenData.highestRemainder
    {g : SmoothMetric M} {μ : Measure (FrameBundle g)}
    (d : MetricGreenData g μ) (e : FrameBundle g) :
    condition (plusWeylHessian g e.base e.frame -
      traceComponent (weylLaplacian (plusWeyl g e.base e.frame))) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusWeyl
def OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients line 8603
Source documentation
The coefficients in the orthonormal basis (L_a R_b)/2 of real four-by-four matrices, with the scalar quaternion in position zero.
```
def rightQuaternionCoefficients (M : Mat4) : Mat4 :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients_pairing line 8622
Source documentation
The exact Parseval identity for this real orthogonal expansion.
```
theorem rightQuaternionCoefficients_pairing (M N : Mat4) :
    (∑ a, ∑ b, rightQuaternionCoefficients M a b * rightQuaternionCoefficients N a b) =
      ∑ i, ∑ j, M i j * N i j := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients
def OAI.PositiveEinsteinFour.HighestHessian.rightMatrixAction line 8628
def OAI.PositiveEinsteinFour.HighestHessian.rightCoefficientAction line 8631
theorem OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients_action_zero line 8636
theorem OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients_action_one line 8644
theorem OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients_action_two line 8652
theorem OAI.PositiveEinsteinFour.HighestHessian.rightQuaternionCoefficients_action line 8660
theorem OAI.PositiveEinsteinFour.HighestHessian.rightCoefficientAction_pairing line 8668
theorem OAI.PositiveEinsteinFour.HighestHessian.rightMatrixAction_pairing line 8675
def OAI.PositiveEinsteinFour.HighestHessian.rightVectorEnergy line 8687
Source documentation
Only the three imaginary right-quaternion coefficients enter the opposite-block action.
```
def rightVectorEnergy (X : Hessian) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HighestHessian.rightVectorGram line 8692
Source documentation
Their ordinary three-dimensional coefficient Gram form.
```
def rightVectorGram (U : Mat) (X : Hessian) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.rightVectorEnergy_le line 8698
Source documentation
The omitted scalar right-quaternion coefficient has nonnegative energy.
```
theorem rightVectorEnergy_le (X : Hessian) : rightVectorEnergy X ≤ hessianNormSq X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.rightVectorEnergy
theorem OAI.PositiveEinsteinFour.HighestHessian.sum_pair_triple line 8716
theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_complement_gram line 8736
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianGram_totalMinus line 8745
Source documentation
The complete minus Gram matrix is the scalar part minus this positive three-dimensional Gram form. This identity is valid for every Hessian.
```
theorem hessianGram_totalMinus (U : Mat) (X : Hessian) :
    hessianGram U (fun r => totalMinus r X) =
      4 * ((∑ r, U r r) * rightVectorEnergy X - rightVectorGram U X) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.hessianGram, OAI.PositiveEinsteinFour.HighestHessian.totalMinus, OAI.PositiveEinsteinFour.HighestHessian.rightVectorEnergy, OAI.PositiveEinsteinFour.HighestHessian.rightVectorGram
theorem OAI.PositiveEinsteinFour.HighestHessian.rightVectorGram_nonneg line 8794
Source documentation
Positive semidefiniteness is used only on the actual coefficient vectors.
```
theorem rightVectorGram_nonneg (U : Mat) (hU : U.PosSemidef) (X : Hessian) :
    0 ≤ rightVectorGram U X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.rightVectorGram
theorem OAI.PositiveEinsteinFour.HighestHessian.rightVectorGram_shift line 8812
theorem OAI.PositiveEinsteinFour.HighestHessian.shift_nonneg_of_traceFree line 8827
Source documentation
A shifted positive matrix with zero trace has a nonnegative shift.
```
theorem shift_nonneg_of_traceFree (U : Mat) (hU : traceFree U) (y : ℝ)
    (hUy : (U + y • (1 : Mat)).PosSemidef) : 0 ≤ y := by
…
```
theorem OAI.PositiveEinsteinFour.HighestHessian.general_minus_cost line 8837
Source documentation
Sharp opposite-block upper cost, with no eigenframe and no additional condition on the two-derivative tensor.
```
theorem general_minus_cost (U : Mat) (hU : traceFree U) (y : ℝ) (hy : 0 ≤ y)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (X : Hessian) :
    hessianGram U (fun r => totalMinus r X) / 4 ≤ y * hessianNormSq X := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.hessianGram, OAI.PositiveEinsteinFour.HighestHessian.totalMinus
theorem OAI.PositiveEinsteinFour.HighestHessian.general_minus_cost_of_shift line 8847
Source documentation
The sign of the shift is already forced by the matrix hypotheses.
```
theorem general_minus_cost_of_shift (U : Mat) (hU : traceFree U) (y : ℝ)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (X : Hessian) :
    hessianGram U (fun r => totalMinus r X) / 4 ≤ y * hessianNormSq X :=
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.hessianGram, OAI.PositiveEinsteinFour.HighestHessian.totalMinus
def OAI.PositiveEinsteinFour.Geometry.ShiftedCurvaturePositive line 8875
Source documentation
Pointwise shifted-matrix positivity is the elementary sectional condition consumed by the local tensor estimate. Its geometric derivation from the curvature decomposition is separate from the weighted estimate.
```
def ShiftedCurvaturePositive (g : SmoothMetric M) : Prop :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.localWeightedHessian line 8880

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.integratedWeightedHessian line 8906

Source documentation

The pointwise square integrates directly on the actual frame bundle.

theorem MetricGreenData.integratedWeightedHessian
    {g : SmoothMetric M} {μ : Measure (FrameBundle g)}
    (d : MetricGreenData g μ) (o : OppositeWeylData d)
    (hp : ShiftedCurvaturePositive g) (m : FrameBundle g → ℝ)
    (hm : ∀ e, 0 < m e) (a : FrameBundle g → Vec) :
    0 ≤ ∫ e,
      weightedQuadratic
        (generalOriginalCurvatureForm (plusWeyl g e.base e.frame) (minusWeyl g e.base e.frame))
        (m e) (plusWeylHessian g e.base e.frame)
        (weightTensor (a e) (plusGradientTensor g e.base e.frame)) +
      generalTraceCorrection (plusWeyl g e.base e.frame) (minusWeyl g e.base e.frame)
        (weylLaplacian (plusWeyl g e.base e.frame)) (m e)
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.OppositeWeylData, OAI.PositiveEinsteinFour.Geometry.ShiftedCurvaturePositive, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusGradientTensor

theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_combination_pairing line 8941
theorem OAI.PositiveEinsteinFour.Bianchi.rawPairing_entries line 8949
theorem OAI.PositiveEinsteinFour.Bianchi.quaternionCombination_pairing line 8955
Source documentation
Polarized version of the real outer-quaternion calculation.
```
theorem quaternionCombination_pairing (a : Vec) (Z W : RawGradient)
    (C D : Fin 3 → RawGradient) :
    hessianPairing (quaternionCombination a Z C) (quaternionCombination a W D) =
      ‖a‖ ^ 2 * (rawPairing Z W + ∑ s, rawPairing (C s) (D s)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.RawGradient, OAI.PositiveEinsteinFour.Bianchi.quaternionCombination, OAI.PositiveEinsteinFour.Bianchi.rawPairing

theorem OAI.PositiveEinsteinFour.Bianchi.totalPlus_weightPlusPart_pairing line 8995

Source documentation

Both generator indices of the real-vector identity are retained.

theorem totalPlus_weightPlusPart_pairing (s t : Fin 3) (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    hessianPairing (totalPlus s (weightPlusPart a Z))
      (totalPlus t (weightPlusPart a Z)) =
      ‖a‖ ^ 2 * ((if s = t then (7 / 12 : ℝ) * Z.squaredNorm else 0) +
        (3 / 4 : ℝ) * rawPairing (rawGradientGenerator s Z.matrix)
          (rawGradientGenerator t Z.matrix)) := by
…

Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart, OAI.PositiveEinsteinFour.Bianchi.rawPairing, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator

theorem OAI.PositiveEinsteinFour.Bianchi.totalPlus_weightPlusPart_generalCost line 9009
Source documentation
The plus contribution to the sharp cost, with a full symmetric Weyl matrix.
```
theorem totalPlus_weightPlusPart_generalCost (A : Mat)
    (hA : symmetric A) (ht : traceFree A) (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    hessianGram A (fun r => totalPlus r (weightPlusPart a Z)) =
      -30 * ‖a‖ ^ 2 * generalGradientForm A Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart
theorem OAI.PositiveEinsteinFour.HighestHessian.hessianNormSq_nonneg line 9032
theorem OAI.PositiveEinsteinFour.HighestHessian.general_nonneg_of_plus_energy line 9037
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_sub line 9053
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ProjectionCost.lean:16 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.HighestHessian.totalPlus_sub@path.
theorem OAI.PositiveEinsteinFour.HighestHessian.projected_plus_pairing line 9059
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ProjectionCost.lean:22 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.HighestHessian.projected_plus_pairing@path.
theorem OAI.PositiveEinsteinFour.HighestHessian.projection_difference_plus_energy line 9072
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ProjectionCost.lean:35 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.HighestHessian.projection_difference_plus_energy@path.

theorem OAI.PositiveEinsteinFour.HighestHessian.general_highestProjection_curvature_le line 9084

Source documentation

The projection cost is bounded by the real-vector plus part in any frame.

theorem general_highestProjection_curvature_le (A U : Mat) (hA : symmetric A)
    (hU : symmetric U) (x y : ℝ) (hy : 0 ≤ y)
    (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (W : Hessian) (hp : (∑ r, hessianNormSq (totalPlus r W)) = 48 * hessianNormSq W) :
    generalCurvaturePairing A U (highestProjection W) (highestProjection W) ≤
      generalCurvaturePairing A U W W := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection

theorem OAI.PositiveEinsteinFour.HighestHessian.general_highestProjection_weight_cost line 9104

Source documentation

The original sharp projection bound, with no diagonal frame assumption.

theorem general_highestProjection_weight_cost (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (a : Vec) (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    generalCurvaturePairing A U
      (highestProjection (weightTensor a Z)) (highestProjection (weightTensor a Z)) ≤
      ‖a‖ ^ 2 * ((7 / 12 : ℝ) * (4 + y) * Z.squaredNorm -
        (5 / 4 : ℝ) * generalGradientForm A Z) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.generalCurvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection, OAI.PositiveEinsteinFour.HighestHessian.weightTensor

def OAI.PositiveEinsteinFour.Geometry.hessianVectorMap line 9151
def OAI.PositiveEinsteinFour.Geometry.vectorHessianMap line 9156
theorem OAI.PositiveEinsteinFour.Geometry.continuous_highestProjection line 9161
theorem OAI.PositiveEinsteinFour.Geometry.continuous_hessianPairing line 9169
theorem OAI.PositiveEinsteinFour.Geometry.continuous_derivativePairing line 9176
theorem OAI.PositiveEinsteinFour.Geometry.continuous_matrixHessianPairing line 9182
theorem OAI.PositiveEinsteinFour.Geometry.continuous_weightedQuadratic line 9192
theorem OAI.PositiveEinsteinFour.Geometry.continuous_weylGradientEnergy line 9200
theorem OAI.PositiveEinsteinFour.Geometry.continuous_matrixSlotAction line 9205
theorem OAI.PositiveEinsteinFour.Geometry.continuous_weylMatrixEnergy line 9218
theorem OAI.PositiveEinsteinFour.Geometry.continuous_weylRadialSquare line 9225
theorem OAI.PositiveEinsteinFour.Geometry.rawBianchiProjection_coordinates line 9231
theorem OAI.PositiveEinsteinFour.Geometry.continuous_weylCompressionEnergy line 9237
theorem OAI.PositiveEinsteinFour.Geometry.continuous_generalCurvaturePairing line 9251
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousFullHessian line 9285
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousWeightTensor line 9289
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousProjectionCost line 9307
theorem OAI.PositiveEinsteinFour.Geometry.matrixPairing_weightTensor_trace line 9339
theorem OAI.PositiveEinsteinFour.Geometry.general_traceCorrection_weyl line 9359
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceGreen line 9388
abbrev OAI.PositiveEinsteinFour.ScalarHessian.Matrix4 line 9437
def OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing line 9439
def OAI.PositiveEinsteinFour.ScalarHessian.scalarNormSq line 9441
def OAI.PositiveEinsteinFour.ScalarHessian.coefficients line 9444
Source documentation
Coefficients of the basis -I_i J_j, whose squared norms are four.
```
def coefficients (S : Matrix4) : Mat := fun i j =>
…
```
Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4
def OAI.PositiveEinsteinFour.ScalarHessian.reconstruct line 9447
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficients_pairing_row_zero line 9449
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficients_pairing_row_one line 9455
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficients_pairing_row_two line 9461
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficients_pairing line 9467
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_apply line 9474
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_entry_zero line 9478
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_entry_one line 9486
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_entry_two line 9494
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_entry_three line 9502
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_entry line 9510
theorem OAI.PositiveEinsteinFour.ScalarHessian.reconstruct_coefficients line 9519
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_comm line 9527
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_sum_left line 9530
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_smul_left line 9540
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_reconstruct line 9544
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_coefficients line 9555
Source documentation
Parseval's identity in the nine actual quaternion product directions.
```
theorem scalarPairing_coefficients (S T : Matrix4)
    (hs : Sᵀ = S) (ht : Matrix.trace S = 0) :
    scalarPairing S T = 4 * ∑ i, ∑ j, coefficients S i j * coefficients T i j := by
…
```
Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4, OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing, OAI.PositiveEinsteinFour.ScalarHessian.coefficients
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarNormSq_coefficients line 9561
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarNormSq_nonneg line 9565
theorem OAI.PositiveEinsteinFour.QuaternionFrame.normalizedBlockNorm_le_shift line 9587
Source documentation
A trace-free block bounded below by -x has normalized norm at most x; the zero block is included.
```
theorem normalizedBlockNorm_le_shift (A : Mat) (hs : symmetric A) (ht : traceFree A)
    (x : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef) :
    normalizedBlockNorm A ≤ x := by
…
```

theorem OAI.PositiveEinsteinFour.QuaternionFrame.normalizedBlockNorm_sum_le_two line 9604

Source documentation

The shifted curvature domain implies the full closed scalar norm triangle, without excluding zeros of either block.

theorem normalizedBlockNorm_sum_le_two (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2) :
    normalizedBlockNorm A + normalizedBlockNorm U ≤ 2 := by
…

def OAI.PositiveEinsteinFour.Geometry.invariantHessianForm line 9634
theorem OAI.PositiveEinsteinFour.Geometry.invariant_green_polynomial_identity line 9640
theorem OAI.PositiveEinsteinFour.Geometry.general_weightedQuadratic_original line 9650
def OAI.PositiveEinsteinFour.Geometry.hessianIntegral line 9670
theorem OAI.PositiveEinsteinFour.Geometry.hessianIntegral_apply line 9673
theorem OAI.PositiveEinsteinFour.Geometry.hessianIntegral_combination line 9679
theorem OAI.PositiveEinsteinFour.Geometry.continuous_generalCoefficient line 9694
theorem OAI.PositiveEinsteinFour.Geometry.continuous_weylLaplacian line 9706
theorem OAI.PositiveEinsteinFour.Geometry.continuous_traceComponent line 9715
theorem OAI.PositiveEinsteinFour.Geometry.continuous_traceFreeSquare line 9732
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusMatrixMap line 9750
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusMatrixMap line 9753
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.gradientMap line 9756
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianMap line 9759
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weightTensorMap line 9762
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianIdentityField line 9767
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianPlusField line 9774
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianMatrixField line 9786
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianMinusField line 9797
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceComponentMap line 9809
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianTraceField line 9813
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianCostField line 9822
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.gradientEnergyField line 9829
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.matrixEnergyField line 9832
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.squareEnergyField line 9836
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.compressionEnergyField line 9841
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radialEnergyField line 9846
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusNormField line 9850
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusNormField line 9854
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weightCubicField line 9858
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weightedHessianGreen line 9868
Source documentation
The weighted Hessian estimate with every Green contribution evaluated on the actual metric tensors. The geometric shifted-positivity condition is kept separate; no new integral estimate is an input.
```
theorem weightedHessianGreen (d : MetricGreenData g μ) (o : OppositeWeylData d)
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (hp : ShiftedCurvaturePositive g)
    (hdecomp : ∀ e : FrameBundle g, frameCurvature g e.base e.frame =
      Angular.einsteinCurvatureTensor (plusWeyl g e.base e.frame) (minusWeyl g e.base e.frame))
    (m : C(FrameBundle g, ℝ)) (hmpos : ∀ e, 0 < m e)
    (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((d.flow i).map s e))
      (dm i ((d.flow i).map t e)) t) :
    0 ≤ ∫ e, m e * invariantHessianForm (plusWeyl g e.base e.frame)
        (minusWeyl g e.base e.frame) (plusWeylGradient g e.base e.frame) -
      (5 / 36 : ℝ) * (∑ i, dm i e * Matrix.trace (plusWeylGradient g e.base e.frame i *
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.OppositeWeylData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ShiftedCurvaturePositive, OAI.PositiveEinsteinFour.Geometry.frameCurvature, OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.invariantHessianForm, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient
def OAI.PositiveEinsteinFour.Geometry.derivativeBasis line 9951
def OAI.PositiveEinsteinFour.Geometry.highestProjectionMap line 9953
theorem OAI.PositiveEinsteinFour.Geometry.highestProjectionMap_apply line 9956
theorem OAI.PositiveEinsteinFour.Geometry.weightTensor_basis_sum line 9958
def OAI.PositiveEinsteinFour.Geometry.projectedWeightKernel line 9964
theorem OAI.PositiveEinsteinFour.Geometry.projection_weight_cost_expansion line 9969
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousProjectedWeightKernel line 9987
def OAI.PositiveEinsteinFour.Geometry.RicciThree line 10026
def OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunSectionalInput line 10031
Source documentation
Equation (5) in the proof of the published Lemma 1, with strict sectional positivity and scalar curvature twelve.
```
def GurskyLeBrunSectionalInput (g : SmoothMetric M) : Prop :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.shiftedCurvaturePositive_of_published line 10039
theorem OAI.PositiveEinsteinFour.Geometry.strict_norm_pinching_of_published line 10046
def OAI.PositiveEinsteinFour.ScalarHessian.blockActionLinear line 10075
def OAI.PositiveEinsteinFour.ScalarHessian.blockAction line 10093
theorem OAI.PositiveEinsteinFour.ScalarHessian.clifford_triple line 10096
theorem OAI.PositiveEinsteinFour.ScalarHessian.folded_clifford_triple line 10113
theorem OAI.PositiveEinsteinFour.ScalarHessian.weighted_clifford_sandwich line 10121
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockAction_product line 10157
theorem OAI.PositiveEinsteinFour.ScalarHessian.plusAction_basis line 10180
theorem OAI.PositiveEinsteinFour.ScalarHessian.minusAction_basis line 10187
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockAction_reconstruct line 10197
theorem OAI.PositiveEinsteinFour.ScalarHessian.basis_pairing line 10202
theorem OAI.PositiveEinsteinFour.ScalarHessian.plusAction_pairing line 10209
Source documentation
The plus operator is the ordinary coefficient-matrix quadratic form on the columns of the nine-product expansion.
```
theorem plusAction_pairing (A : Mat) (hA : symmetric A) (htA : traceFree A)
    (S : Matrix4) (hS : Sᵀ = S) (htS : Matrix.trace S = 0) :
    scalarPairing (blockAction quaternionMatrix A S) S =
      4 * ∑ j, ∑ r, ∑ s, A r s * coefficients S r j * coefficients S s j := by
…
```
Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4, OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing, OAI.PositiveEinsteinFour.ScalarHessian.blockAction, OAI.PositiveEinsteinFour.ScalarHessian.coefficients
theorem OAI.PositiveEinsteinFour.ScalarHessian.minusAction_pairing line 10225
Source documentation
The minus operator acts on the rows of the same expansion.
```
theorem minusAction_pairing (U : Mat) (hU : symmetric U) (htU : traceFree U)
    (S : Matrix4) (hS : Sᵀ = S) (htS : Matrix.trace S = 0) :
    scalarPairing (blockAction oppositeMatrix U S) S =
      4 * ∑ i, ∑ r, ∑ s, U r s * coefficients S i r * coefficients S i s := by
…
```
Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4, OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing, OAI.PositiveEinsteinFour.ScalarHessian.blockAction, OAI.PositiveEinsteinFour.ScalarHessian.coefficients
def OAI.PositiveEinsteinFour.ScalarHessian.scalarCurvatureContraction line 10259
theorem OAI.PositiveEinsteinFour.ScalarHessian.sum_five_permute line 10265

theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarCurvatureContraction_tuple line 10283

Source documentation

The curvature term in the tuple-indexed Green identity is exactly the contraction above; this is only reindexing, with no tensor hypothesis.

theorem scalarCurvatureContraction_tuple (A U : Mat) (p : Vec) :
    (1 / 2 : ℝ) * ∑ q : (Fin 4 × Fin 4) × (Fin 4 × Fin 4),
      (generalCoefficient quaternionMatrix A q.1.1 q.1.2 q.2.1 q.2.2 +
        generalCoefficient oppositeMatrix U q.1.1 q.1.2 q.2.1 q.2.2) *
        (∑ h, generalEinsteinCoefficient A U q.1.1 q.1.2 q.2.1 h * p h) * p q.2.2 =
      scalarCurvatureContraction A U p := by
…

Mentions: OAI.PositiveEinsteinFour.ScalarHessian.scalarCurvatureContraction

theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarCurvatureContraction_eq line 10293
theorem OAI.PositiveEinsteinFour.Geometry.orthogonal_basis_conjugation_injective line 10346
theorem OAI.PositiveEinsteinFour.Geometry.chartRicci_three_of_frame line 10360
theorem OAI.PositiveEinsteinFour.Geometry.ricciThree_of_frame_contraction line 10374
def OAI.PositiveEinsteinFour.Geometry.blockRadialGradient line 10398
theorem OAI.PositiveEinsteinFour.Geometry.trace_eq_norm_mul_radial line 10401
theorem OAI.PositiveEinsteinFour.Geometry.weylRadialSquare_eq line 10410
theorem OAI.PositiveEinsteinFour.Geometry.invariantHessianForm_eq_collected line 10420
def OAI.PositiveEinsteinFour.Geometry.regularizedProjectionCost line 10449
theorem OAI.PositiveEinsteinFour.Geometry.regularizedProjectionCost_eq_matrixWeight line 10459
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.integral_regularizedProjectionCost_tendsto line 10468
def OAI.PositiveEinsteinFour.Geometry.regularizedHessianIntegrand line 10504
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedHessianGreen line 10516
def OAI.PositiveEinsteinFour.QuaternionFrame.rawField line 10554
def OAI.PositiveEinsteinFour.QuaternionFrame.fieldRaw line 10555
theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawField_fieldRaw line 10558
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fieldRaw_rawField line 10559
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_fieldRaw line 10561
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_add line 10566
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_sub line 10572
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_smul line 10583
theorem OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient_sum line 10589
theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawMatrixRotation_field line 10600
theorem OAI.PositiveEinsteinFour.QuaternionFrame.matrixAction_sum_smul line 10608
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.rawMatrixRotation_turn line 10614
def OAI.PositiveEinsteinFour.QuaternionFrame.rawQuaternion line 10637
theorem OAI.PositiveEinsteinFour.QuaternionFrame.quaternion_sum line 10640
theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawQuaternion_sum_smul line 10647
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.rawQuaternion_turn line 10654
theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawCoupling_eq line 10675
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.rawCoupling_turn line 10682
Source documentation
The actual Casimir coupling is unchanged by the passive frame transformation, because both of its generator indices rotate together.
```
theorem QuaternionLift.rawCoupling_turn {R : Mat}
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (hR : Rᵀ * R = 1) (Z : RawGradient) :
    rawCoupling (turnRawGradient R P.matrix Z) =
      turnRawGradient R P.matrix (rawCoupling Z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.turnRawGradient
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.rawBianchiProjection_turn line 10710
theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawPairing_turn line 10718
theorem OAI.PositiveEinsteinFour.QuaternionFrame.generalMatrixAction_field line 10726
theorem OAI.PositiveEinsteinFour.QuaternionFrame.generalMatrixAction_turn line 10730
theorem OAI.PositiveEinsteinFour.QuaternionFrame.gradientTensor_matrix_eq_fieldRaw line 10738
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.weylCompressionEnergy_turn line 10745
Source documentation
The genuine squared norm of the projected matrix action is invariant under the locally constructed frame change.
```
theorem QuaternionLift.weylCompressionEnergy_turn {R : Mat}
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (hR : Rᵀ * R = 1) (A : Mat) (Z : Angular.Gradient)
    (hs : ∀ i, symmetric (Z i)) :
    weylCompressionEnergy (conjugateMatrix R A) (turnGradient R P.matrix Z) =
      weylCompressionEnergy A Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.turnGradient
theorem OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.invariantHessianForm_turn line 10758
def OAI.PositiveEinsteinFour.ScalarHessian.coefficientQuadratic line 10789
def OAI.PositiveEinsteinFour.ScalarHessian.crossVector line 10792
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficientQuadratic_nonneg line 10795
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficientQuadratic_cross_identity line 10807
theorem OAI.PositiveEinsteinFour.ScalarHessian.coefficientQuadratic_le_two_shift line 10820
Source documentation
The upper eigenvalue bound follows directly from shifted positivity, with no spectral frame.
```
theorem coefficientQuadratic_le_two_shift (A : Mat) (hA : symmetric A)
    (ht : traceFree A) (x : ℝ) (hx : (A + x • (1 : Mat)).PosSemidef)
    (c : Fin 3 → ℝ) :
    coefficientQuadratic A c ≤ 2 * x * ∑ r, c r ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.ScalarHessian.coefficientQuadratic
def OAI.PositiveEinsteinFour.ScalarHessian.columnGram line 10829
def OAI.PositiveEinsteinFour.ScalarHessian.rowGram line 10831
theorem OAI.PositiveEinsteinFour.ScalarHessian.columnGram_le_two_shift line 10833
theorem OAI.PositiveEinsteinFour.ScalarHessian.rowGram_le_two_shift line 10842

theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarHessian_operator_bound line 10852

Source documentation

The sharp scalar-Hessian operator bound for arbitrary symmetric Weyl matrices and their actual shifted positive forms.

theorem scalarHessian_operator_bound (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (S : Matrix4) (hS : Sᵀ = S) (htS : Matrix.trace S = 0) :
    scalarPairing (blockAction quaternionMatrix A S) S +
      scalarPairing (blockAction oppositeMatrix U S) S ≤ 4 * scalarNormSq S := by
…

Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4, OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing, OAI.PositiveEinsteinFour.ScalarHessian.blockAction, OAI.PositiveEinsteinFour.ScalarHessian.scalarNormSq

def OAI.PositiveEinsteinFour.SectionalPlane.quadratic line 10889
theorem OAI.PositiveEinsteinFour.SectionalPlane.quadratic_smul line 10892
theorem OAI.PositiveEinsteinFour.SectionalPlane.quadratic_add_scalar line 10901
theorem OAI.PositiveEinsteinFour.SectionalPlane.exists_minimum_shift line 10911
Source documentation
An attained minimum on the unit sphere supplies the exact PSD shift.
```
theorem exists_minimum_shift (A : Geometry.Mat3) (hA : symmetric A) :
    ∃ s : EuclideanSpace ℝ (Fin 3), ‖s‖ = 1 ∧
      (A + (-quadratic A s) • (1 : Geometry.Mat3)).PosSemidef := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.SectionalPlane.quadratic
def OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue line 10942
theorem OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue_add line 10945
theorem OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue_smul line 10949
theorem OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue_sum line 10953
theorem OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue_twoFormProduct line 10963
theorem OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue_blockTensor line 10980
theorem OAI.PositiveEinsteinFour.SectionalPlane.plane_independent line 10986
theorem OAI.PositiveEinsteinFour.SectionalPlane.rayleigh_sum_pos line 11006
Source documentation
Positivity on actual two-planes bounds every pair of unit block Rayleigh quotients; both blocks can be minimized independently.
```
theorem rayleigh_sum_pos (A B : Geometry.Mat3)
    (hp : ∀ u v : Vec4, LinearIndependent ℝ ![u, v] →
      0 < sectionalValue (einsteinCurvatureTensor A B) u v)
    (s t : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) (ht : ‖t‖ = 1) :
    0 < 2 + quadratic A s + quadratic B t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.SectionalPlane.Vec4, OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue, OAI.PositiveEinsteinFour.SectionalPlane.quadratic
theorem OAI.PositiveEinsteinFour.SectionalPlane.shifts_of_positive_planes line 11036
Source documentation
The published sectional criterion follows from the proved plane realization and elementary extrema on two unit spheres.
```
theorem shifts_of_positive_planes (A B : Geometry.Mat3)
    (hA : symmetric A) (hB : symmetric B)
    (hp : ∀ u v : Vec4, LinearIndependent ℝ ![u, v] →
      0 < sectionalValue (einsteinCurvatureTensor A B) u v) :
    ∃ x y : ℝ, (A + x • (1 : Geometry.Mat3)).PosSemidef ∧
      (B + y • (1 : Geometry.Mat3)).PosSemidef ∧ x + y < 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.SectionalPlane.Vec4, OAI.PositiveEinsteinFour.SectionalPlane.sectionalValue
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map_eq_combination line 11059
theorem OAI.PositiveEinsteinFour.Geometry.sectionalValue_frame line 11069
theorem OAI.PositiveEinsteinFour.Geometry.sectionalInput_of_curvature_decomposition line 11107
Source documentation
The pointwise sectional threshold follows from ordinary curvature-block symmetry/decomposition and actual positive sectional curvature. No eigenvalue/sectional estimate is a premise.
```
theorem sectionalInput_of_curvature_decomposition (g : SmoothMetric M)
    (hdecomp : RicciThree g → ∀ c (e : OrthonormalFrame g c), frameCurvature g c e =
      Angular.einsteinCurvatureTensor (plusWeyl g c e) (minusWeyl g c e))
    (hplus : ∀ e : FrameBundle g, TraceHessian.symmetric (plusWeyl g e.base e.frame))
    (hminus : ∀ e : FrameBundle g, TraceHessian.symmetric (minusWeyl g e.base e.frame)) :
    GurskyLeBrunSectionalInput g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.frameCurvature, OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunSectionalInput
def OAI.PositiveEinsteinFour.AlgebraicCurvature.pair line 11138
def OAI.PositiveEinsteinFour.AlgebraicCurvature.pairIndex line 11141
def OAI.PositiveEinsteinFour.AlgebraicCurvature.pairSign line 11151
def OAI.PositiveEinsteinFour.AlgebraicCurvature.matrixOf line 11154
def OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf line 11157
def OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew line 11160
def OAI.PositiveEinsteinFour.AlgebraicCurvature.LastSkew line 11162
def OAI.PositiveEinsteinFour.AlgebraicCurvature.PairSymmetric line 11164
def OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstBianchi line 11166
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.pairSymmetric_of_bianchi line 11169
def OAI.PositiveEinsteinFour.AlgebraicCurvature.ricci line 11183
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.first_diagonal_zero line 11185
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.last_diagonal_zero line 11188
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_matrixOf_row0 line 11191
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_matrixOf_row1 line 11211
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_matrixOf_row2 line 11231
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_matrixOf_row3 line 11251
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_matrixOf line 11273
Source documentation
First and last skew symmetry reconstruct the whole four-tensor from its 36 canonical two-form matrix entries.
```
theorem tensorOf_matrixOf {R : CurvatureArray} (hf : FirstSkew R) (hl : LastSkew R) :
    tensorOf (matrixOf R) = R := by
…
```
Mentions: OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew, OAI.PositiveEinsteinFour.AlgebraicCurvature.LastSkew, OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf, OAI.PositiveEinsteinFour.AlgebraicCurvature.matrixOf
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.matrixOf_symmetric line 11282
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensor_eq_of_matrixOf_eq line 11287
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.pairIndex_reverse line 11292
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.pairSign_reverse line 11295
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_firstSkew line 11298
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_lastSkew line 11303
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.pair_sum line 11310
Source documentation
Compression of an antisymmetric coordinate sum to the six increasing index pairs. The factor two records the two orders of each pair.
```
theorem pair_sum (Q : Mat4) (hQ : Qᵀ = -Q) (f : Fin 6 → ℝ) :
    (∑ i : Fin 4, ∑ j : Fin 4, pairSign i j * Q i j * f (pairIndex i j)) =
      2 * ∑ a : Fin 6, Q (pair a).1 (pair a).2 * f a := by
…
```
Mentions: OAI.PositiveEinsteinFour.AlgebraicCurvature.pairSign, OAI.PositiveEinsteinFour.AlgebraicCurvature.pairIndex, OAI.PositiveEinsteinFour.AlgebraicCurvature.pair
def OAI.PositiveEinsteinFour.AlgebraicCurvature.canonicalBlock line 11321
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.pair_bilinear_sum line 11326
def OAI.PositiveEinsteinFour.AlgebraicCurvature.mixedBlock line 11368
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.mixedBlock_tensorOf line 11372
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.curvatureBlock_tensorOf line 11386
def OAI.PositiveEinsteinFour.AlgebraicCurvature.plusFormula line 11392
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.plusFormula_row0 line 11397
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.plusFormula_row1 line 11403
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.plusFormula_row2 line 11409
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.plusFormula_eq line 11415
def OAI.PositiveEinsteinFour.AlgebraicCurvature.minusFormula line 11423
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.minusFormula_row0 line 11428
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.minusFormula_row1 line 11434
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.minusFormula_row2 line 11440
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.minusFormula_eq line 11446
structure OAI.PositiveEinsteinFour.AlgebraicCurvature.EinsteinRelations line 11454
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.einsteinRelations_of_ricci line 11466
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blockTensor_apply line 11522
def OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor line 11526
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_row0 line 11529
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_row1 line 11572
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_row2 line 11615
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_row3 line 11658
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_row4 line 11701
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_row5 line 11744
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.matrixOf_blocksTensor line 11787
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.matrixOf_tensorOf line 11799
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blockTensor_firstSkew line 11804
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blockTensor_lastSkew line 11811
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_firstSkew line 11818
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.blocksTensor_lastSkew line 11827
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.tensorOf_eq_blocksTensor line 11836
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.einstein_decomposition line 11845
Source documentation
The Einstein block decomposition follows from ordinary algebraic curvature symmetries and Ricci normalization, using the actual quaternion contractions. No decomposition or sectional threshold is assumed.
```
theorem einstein_decomposition (R : CurvatureArray) (hf : FirstSkew R)
    (hl : LastSkew R) (hp : PairSymmetric R)
    (hr : ∀ j k, ricci R j k = if j = k then 3 else 0) :
    R = einsteinCurvatureTensor
      (curvatureBlock (fun p q => R p.1 p.2 q.2 q.1) quaternionMatrix - 1)
      (curvatureBlock (fun p q => R p.1 p.2 q.2 q.1) oppositeMatrix - 1) := by
…
```
Mentions: OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew, OAI.PositiveEinsteinFour.AlgebraicCurvature.LastSkew, OAI.PositiveEinsteinFour.AlgebraicCurvature.PairSymmetric, OAI.PositiveEinsteinFour.AlgebraicCurvature.ricci
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.einstein_decomposition_of_bianchi line 11875
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.curvaturePairing_symmetric line 11883
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.curvatureBlock_sub_one_symmetric line 11891
theorem OAI.PositiveEinsteinFour.QuaternionFrame.blockRadialGradient_turn line 11919
theorem OAI.PositiveEinsteinFour.QuaternionFrame.blockRadialGradient_diagonal line 11928

theorem OAI.PositiveEinsteinFour.QuaternionFrame.blockRadialGradient_refined_kato line 11943

Source documentation

Refined Kato for the actual radial derivative of a symmetric trace-free block. No nonvanishing or eigenframe premise is required.

theorem blockRadialGradient_refined_kato (A : Mat) (Z : Angular.Gradient)
    (hA : symmetric A) (htA : traceFree A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    (5 / 3 : ℝ) * ‖blockRadialGradient A Z‖ ^ 2 ≤ weylGradientEnergy Z := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.Geometry.regularizedHessianIntegrand_eq_weight line 12005
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.invariantHessianField line 12033
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.cubicEntryField line 12044
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.integral_regularizedHessian_tendsto line 12050
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.unregularizedHessianGreen line 12068
Source documentation
The nonsmooth norm weight satisfies the actual integrated Hessian inequality. No positivity of either Weyl norm is required.
```
theorem unregularizedHessianGreen (d : MetricGreenData g μ) (o : OppositeWeylData d)
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (hp : ShiftedCurvaturePositive g)
    (hdecomp : ∀ e : FrameBundle g, frameCurvature g e.base e.frame =
      Angular.einsteinCurvatureTensor (plusWeyl g e.base e.frame) (minusWeyl g e.base e.frame))
    (hpinch : ∀ e : FrameBundle g, normalizedBlockNorm (plusWeyl g e.base e.frame) +
      normalizedBlockNorm (minusWeyl g e.base e.frame) < 2) :
    0 ≤ ∫ e, regularizedHessianIntegrand g 0 e ∂μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.OppositeWeylData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ShiftedCurvaturePositive, OAI.PositiveEinsteinFour.Geometry.frameCurvature, OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.regularizedHessianIntegrand
theorem OAI.PositiveEinsteinFour.Geometry.regularizedRadial_zero_implies line 12114
theorem OAI.PositiveEinsteinFour.Geometry.radial_zero_ae_on_level line 12125
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radial_zero_ae_on_level line 12158
theorem OAI.PositiveEinsteinFour.Geometry.OppositeWeylData.radial_zero_ae_on_level line 12166
theorem OAI.PositiveEinsteinFour.ScalarHessian.sum_four_swap line 12192
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockAction_entry line 12200
def OAI.PositiveEinsteinFour.ScalarHessian.blockQuadratic line 12233
Source documentation
The row of the four-index operator is (i,j) and the column (k,l).
```
def blockQuadratic (Q : Fin 3 → Matrix4) (A : Mat) (S : Matrix4) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockQuadratic_eq_pairing line 12236
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarHessian_coefficient_bound line 12259
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.weyl_blocks_traceFree line 12288
def OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi line 12344
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.divergence_eq_ricci_derivatives line 12347
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.divergence_zero_of_ricci_parallel line 12358
def OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray line 12376
def OAI.PositiveEinsteinFour.Geometry.bianchiCycle line 12379
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_precompose_five line 12385
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_differentialBianchi line 12403
Source documentation
The cyclic differential identity is preserved by the actual tensor pullback; no orthogonality or frame-flow premise is required.
```
theorem frameTensor_differentialBianchi (A : Mat4) (T : CovariantCoordinates 5)
    (h : AlgebraicCurvature.DifferentialBianchi (curvatureDerivativeArray T)) :
    AlgebraicCurvature.DifferentialBianchi (curvatureDerivativeArray (frameTensor A T)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.Geometry.frameTensor
def OAI.PositiveEinsteinFour.Geometry.orientationSign line 12458
theorem OAI.PositiveEinsteinFour.Geometry.orientationSign_sq line 12460
def OAI.PositiveEinsteinFour.Geometry.reflectedGradient line 12464
theorem OAI.PositiveEinsteinFour.Geometry.reflectedGradient_divergence line 12467
theorem OAI.PositiveEinsteinFour.Geometry.reflectedGradient_energy line 12479
theorem OAI.PositiveEinsteinFour.Geometry.reflectedGradient_radial_norm line 12495
theorem OAI.PositiveEinsteinFour.Geometry.opposite_refinedKato line 12509
theorem OAI.PositiveEinsteinFour.Geometry.OppositeWeylData.refinedKato line 12529

theorem OAI.PositiveEinsteinFour.Geometry.refined_kato_matrixPairing line 12556

Source documentation

The invariant radial Kato estimate gives a polynomial contraction bound, including at the zero matrix.

theorem refined_kato_matrixPairing (A : Mat) (Z : Fin 4 → Mat)
    (hA : symmetric A) (htA : traceFree A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    (∑ i, matrixPairing A (Z i) ^ 2) ≤
      (3 / 5 : ℝ) * matrixPairing A A * ∑ i, matrixPairing (Z i) (Z i) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.gradientDivergence

theorem OAI.PositiveEinsteinFour.Geometry.refined_kato_contraction line 12581

Source documentation

Coordinate form of the refined Kato contraction estimate. The off-diagonal entries have their full Frobenius multiplicity.

theorem refined_kato_contraction (A : Mat) (Z : Fin 4 → Mat)
    (hA : symmetric A) (htA : traceFree A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    (∑ i, (∑ a, ∑ b, A a b * Z i a b) ^ 2) ≤
      (3 / 5 : ℝ) * (∑ a, ∑ b, A a b ^ 2) *
        ∑ i, ∑ a, ∑ b, Z i a b ^ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.gradientDivergence

def OAI.PositiveEinsteinFour.Geometry.regularizedRadialSecond line 12613
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedRadialDerivative line 12617
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedRadialSecond line 12639
theorem OAI.PositiveEinsteinFour.Geometry.regularizedRadialSecond_sum line 12648
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedNormField line 12674
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedRadialField line 12678
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedSecondField line 12684
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedRadialField_derivative line 12691

theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.testedRegularizedNormEquation line 12700

Source documentation

The weak scalar norm equation at positive regularization. Its matrix Laplacian term is fixed by the proved Bianchi commutator equation.

theorem testedRegularizedNormEquation (d : MetricGreenData g μ)
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (ε : ℝ) (hε : 0 < ε) (k : C(FrameBundle g, ℝ))
    (dk : Fin 4 → C(FrameBundle g, ℝ))
    (hk : ∀ i t e, HasDerivAt (fun s => k ((d.flow i).map s e))
      (dk i ((d.flow i).map t e)) t) :
    (∫ e, k e * ((weylGradientEnergy (plusWeylGradient g e.base e.frame) +
        Matrix.trace (plusWeyl g e.base e.frame * weylLaplacian (plusWeyl g e.base e.frame)) / 6 -
        ∑ i, (d.regularizedRadialField ε hε i e) ^ 2) / d.regularizedNormField ε e) +
      ∑ i, dk i e * d.regularizedRadialField ε hε i e ∂μ) = 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.weylGradientEnergy, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.plusWeyl

theorem OAI.PositiveEinsteinFour.Geometry.scalar_block_quadratic_tuple line 12763
theorem OAI.PositiveEinsteinFour.Geometry.scalar_curvature_contraction_commuted line 12772
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradientVector_apply line 12790
def OAI.PositiveEinsteinFour.Geometry.scalarWeylHessianForm line 12793
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.curvature_identity line 12797
theorem OAI.PositiveEinsteinFour.ScalarHessian.weighted_clifford_product_zero line 12903
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockAction_one line 12928
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockAction_trace line 12936
def OAI.PositiveEinsteinFour.ScalarHessian.traceFreePart line 12964
theorem OAI.PositiveEinsteinFour.ScalarHessian.traceFreePart_symmetric line 12966
theorem OAI.PositiveEinsteinFour.ScalarHessian.traceFreePart_trace line 12971
theorem OAI.PositiveEinsteinFour.ScalarHessian.traceFreePart_norm line 12976
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_one_right line 12982
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_sub_right line 12985
theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarPairing_smul_right line 12989
theorem OAI.PositiveEinsteinFour.ScalarHessian.blockQuadratic_traceFreePart line 12993

theorem OAI.PositiveEinsteinFour.ScalarHessian.scalarHessian_coefficient_bound_full line 13010

Source documentation

The actual scalar Hessian may retain its trace; the Weyl contraction only sees the trace-free part.

theorem scalarHessian_coefficient_bound_full (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (S : Matrix4) (hS : Sᵀ = S) :
    blockQuadratic quaternionMatrix A S + blockQuadratic oppositeMatrix U S ≤
      4 * scalarNormSq (traceFreePart S) := by
…

Mentions: OAI.PositiveEinsteinFour.ScalarHessian.Matrix4, OAI.PositiveEinsteinFour.ScalarHessian.blockQuadratic, OAI.PositiveEinsteinFour.ScalarHessian.scalarNormSq, OAI.PositiveEinsteinFour.ScalarHessian.traceFreePart

theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawPairing_self_nonneg line 13041
theorem OAI.PositiveEinsteinFour.QuaternionFrame.rawPairing_sub_right line 13044

theorem OAI.PositiveEinsteinFour.QuaternionFrame.projected_diagonal_energy_lower line 13050

Source documentation

The explicit Bianchi curvature action is an orthogonal test of the true projected action. Its squared norm is therefore a lower bound.

theorem projected_diagonal_energy_lower (S : Shape) (v : ℝ) (p k l : Vec) :
    (curvatureAction S v p k l).squaredNorm ≤
      rawPairing
        (rawBianchiProjection (generalMatrixAction
          (Matrix.diagonal (fun a => v * S.s a)) (parameters S p k l).matrix))
        (rawBianchiProjection (generalMatrixAction
          (Matrix.diagonal (fun a => v * S.s a)) (parameters S p k l).matrix)) := by
…

theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylMatrixEnergy_diagonal line 13073
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weighted_row_norms line 13083
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylMatrixEnergy_shape line 13090
theorem OAI.PositiveEinsteinFour.QuaternionFrame.shape_traceFreeSquare line 13100
theorem OAI.PositiveEinsteinFour.QuaternionFrame.weylMatrixEnergy_squareShape line 13120

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariantHessianForm_spectral_upper_of_frame line 13137

Source documentation

All scalar contractions needed by the source Hessian form can be evaluated in the single pointwise spectral frame. No smooth eigenframe or second-block diagonalization is involved.

theorem invariantHessianForm_spectral_upper_of_frame (A U : Mat) (Z : Angular.Gradient)
    (R : Mat) (hR : Rᵀ * R = 1)
    (P : QuaternionLift quaternionMatrix Angular.oppositeMatrix R)
    (S : Shape)
    (hS : conjugateMatrix R A = Matrix.diagonal (fun i => normalizedBlockNorm A * S.s i))
    (hv : 0 < normalizedBlockNorm A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    ∃ (p k l : Vec),
      (parameters S p k l).squaredNorm / 6 = weylGradientEnergy Z ∧
      ‖p‖ ^ 2 = ‖blockRadialGradient A Z‖ ^ 2 ∧
      weylMatrixEnergy A Z =
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.conjugateMatrix

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariantHessianForm_spectral_upper line 13209

Source documentation

The pointwise spectral frame is constructed from the actual block.

theorem invariantHessianForm_spectral_upper (A U : Mat) (Z : Angular.Gradient)
    (hA : symmetric A) (htA : traceFree A) (hv : 0 < normalizedBlockNorm A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    ∃ (S : Shape) (p k l : Vec),
      (parameters S p k l).squaredNorm / 6 = weylGradientEnergy Z ∧
      ‖p‖ ^ 2 = ‖blockRadialGradient A Z‖ ^ 2 ∧
      invariantHessianForm A U Z ≤
        hessianTensorForm S (normalizedBlockNorm A) (normalizedBlockNorm U) p k l := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariantHessianForm_shifted_spectral_upper line 13225

Source documentation

The same spectral shape supplies both the Hessian estimate and the minimum-eigenvalue parameter constrained by positive shifted curvature.

theorem invariantHessianForm_shifted_spectral_upper (A U : Mat) (Z : Angular.Gradient)
    (hA : symmetric A) (htA : traceFree A) (hv : 0 < normalizedBlockNorm A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0)
    (x : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef) :
    ∃ (S : Shape) (r : ℝ) (p k l : Vec),
      1 ≤ r ∧ r ≤ 2 ∧ S.sigma = (3 * r - r ^ 3) / 2 ∧
      normalizedBlockNorm A * r ≤ x ∧
      Matrix.trace (A * (A * A)) = 6 * normalizedBlockNorm A ^ 3 * S.sigma ∧
      (parameters S p k l).squaredNorm / 6 = weylGradientEnergy Z ∧
      ‖p‖ ^ 2 = ‖blockRadialGradient A Z‖ ^ 2 ∧
      weylMatrixEnergy A Z =
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.ricci_zero_blocks_traceFree line 13265
theorem OAI.PositiveEinsteinFour.Geometry.quaternion_cyclic_0 line 13320
theorem OAI.PositiveEinsteinFour.Geometry.quaternion_cyclic_1 line 13331
theorem OAI.PositiveEinsteinFour.Geometry.quaternion_cyclic_2 line 13342
theorem OAI.PositiveEinsteinFour.Geometry.quaternion_cyclic_3 line 13353
theorem OAI.PositiveEinsteinFour.Geometry.quaternion_cyclic_contraction line 13364
theorem OAI.PositiveEinsteinFour.Geometry.opposite_quaternion_cyclic_0 line 13377
theorem OAI.PositiveEinsteinFour.Geometry.opposite_quaternion_cyclic_1 line 13389
theorem OAI.PositiveEinsteinFour.Geometry.opposite_quaternion_cyclic_2 line 13401
theorem OAI.PositiveEinsteinFour.Geometry.opposite_quaternion_cyclic_3 line 13413
theorem OAI.PositiveEinsteinFour.Geometry.opposite_quaternion_cyclic_contraction line 13425
theorem OAI.PositiveEinsteinFour.Geometry.curvature_quaternion_contraction line 13440
Source documentation
Differential Bianchi removes the Hodge-star part of the quaternionic contraction; its remaining part is the ordinary divergence.
```
theorem curvature_quaternion_contraction (D : Fin 4 → Angular.CurvatureArray)
    (hs : ∀ a, AlgebraicCurvature.FirstSkew (D a))
    (hc : AlgebraicCurvature.DifferentialBianchi D) (i k l : Fin 4) :
    (∑ s : Fin 3, ∑ j : Fin 4, ∑ a : Fin 4, ∑ b : Fin 4,
      TraceHessian.quaternionMatrix s i j *
        TraceHessian.quaternionMatrix s a b * D j a b k l) =
      -2 * ∑ j : Fin 4, D j j i k l := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.CurvatureArray, OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew, OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi, OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix
theorem OAI.PositiveEinsteinFour.Geometry.opposite_curvature_quaternion_contraction line 13455
theorem OAI.PositiveEinsteinFour.Geometry.sum_six_last_pair line 13470
theorem OAI.PositiveEinsteinFour.Geometry.gradientBlock_divergence_eq_kernel line 13485
Source documentation
The block divergence is the quaternionic contraction of the complete five-tensor, with the unused two-form pair kept intact.
```
theorem gradientBlock_divergence_eq_kernel (Q : Fin 3 → Mat4)
    (T : CovariantCoordinates 5) (r : Fin 3) (i : Fin 4) :
    (∑ s, ∑ j, Q s i j * gradientBlock T Q j s r) =
      (1 / 8 : ℝ) * ∑ c, ∑ d, Q r c d *
        (∑ s, ∑ j, ∑ a, ∑ b, Q s i j * Q s a b * T ![j, a, b, d, c]) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.gradientBlock
theorem OAI.PositiveEinsteinFour.Geometry.gradientBlock_divergence_zero line 13512
Source documentation
A divergence-free curvature derivative satisfying differential Bianchi has a divergence-free self-dual block.
```
theorem gradientBlock_divergence_zero (T : CovariantCoordinates 5)
    (hs : ∀ a, AlgebraicCurvature.FirstSkew (curvatureDerivativeArray T a))
    (hc : AlgebraicCurvature.DifferentialBianchi (curvatureDerivativeArray T))
    (hd : ∀ i k l, ∑ j, T ![j, j, i, k, l] = 0)
    (r : Fin 3) (i : Fin 4) :
    gradientDivergence (fun j => gradientBlock T TraceHessian.quaternionMatrix j) r i = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.gradientBlock, OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix
theorem OAI.PositiveEinsteinFour.Geometry.gradientBlock_divergence_of_ricci_parallel line 13534
Source documentation
The contracted Ricci identity supplies the remaining divergence condition; all the block-Bianchi algebra is then automatic.
```
theorem gradientBlock_divergence_of_ricci_parallel (T : CovariantCoordinates 5)
    (hs : ∀ a, AlgebraicCurvature.FirstSkew (curvatureDerivativeArray T a))
    (hl : ∀ a, AlgebraicCurvature.LastSkew (curvatureDerivativeArray T a))
    (hp : ∀ a, AlgebraicCurvature.PairSymmetric (curvatureDerivativeArray T a))
    (hc : AlgebraicCurvature.DifferentialBianchi (curvatureDerivativeArray T))
    (hr : ∀ a j k, ∑ i, T ![a, i, j, k, i] = 0)
    (r : Fin 3) (i : Fin 4) :
    gradientDivergence (fun j => gradientBlock T TraceHessian.quaternionMatrix j) r i = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.AlgebraicCurvature.LastSkew, OAI.PositiveEinsteinFour.AlgebraicCurvature.PairSymmetric, OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.gradientBlock, OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix
theorem OAI.PositiveEinsteinFour.Geometry.opposite_gradientBlock_divergence_zero line 13549
Source documentation
The opposite quaternion block satisfies its own Bianchi contraction.
```
theorem opposite_gradientBlock_divergence_zero (T : CovariantCoordinates 5)
    (hs : ∀ a, AlgebraicCurvature.FirstSkew (curvatureDerivativeArray T a))
    (hc : AlgebraicCurvature.DifferentialBianchi (curvatureDerivativeArray T))
    (hd : ∀ i k l, ∑ j, T ![j, j, i, k, l] = 0)
    (r : Fin 3) (i : Fin 4) :
    (∑ s, ∑ j, Angular.oppositeMatrix s i j *
      gradientBlock T Angular.oppositeMatrix j s r) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.AlgebraicCurvature.FirstSkew, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.Geometry.gradientBlock
theorem OAI.PositiveEinsteinFour.Geometry.opposite_gradientBlock_divergence_of_ricci_parallel line 13569
def OAI.PositiveEinsteinFour.Geometry.frameReflectionMatrix line 13600
theorem OAI.PositiveEinsteinFour.Geometry.frameReflectionMatrix_transpose line 13602
theorem OAI.PositiveEinsteinFour.Geometry.frameReflectionMatrix_sq line 13605
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.reflect line 13617
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.reflect_matrix line 13629
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.reflect_vector line 13635
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.reflect_reflect line 13641
def OAI.PositiveEinsteinFour.Geometry.frameReflection line 13655
theorem OAI.PositiveEinsteinFour.Geometry.frameReflection_involutive line 13658
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_reflect line 13664
theorem OAI.PositiveEinsteinFour.Geometry.curvatureBlock_reflect line 13682
theorem OAI.PositiveEinsteinFour.Geometry.curvaturePairing_reflect line 13702
theorem OAI.PositiveEinsteinFour.Geometry.plusWeyl_reflect line 13709
theorem OAI.PositiveEinsteinFour.Geometry.minusWeyl_reflect line 13715
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_reflect line 13719
theorem OAI.PositiveEinsteinFour.Geometry.gradientBlock_frame_reflect line 13729
theorem OAI.PositiveEinsteinFour.Geometry.hessianBlock_frame_reflect line 13748
theorem OAI.PositiveEinsteinFour.Geometry.plusWeylGradient_reflect line 13768
theorem OAI.PositiveEinsteinFour.Geometry.plusWeylHessian_reflect line 13773

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariant_projection_cost line 13798

Source documentation

Normalize the arbitrary-frame real-vector cost without rotating the opposite block or the weight covector.

theorem invariant_projection_cost (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (a : Vec) (Z : Angular.Gradient)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0) :
    generalCurvaturePairing A U
        (highestProjection (weightTensor a (gradientTensor Z)))
        (highestProjection (weightTensor a (gradientTensor Z))) / 6 ≤
      ‖a‖ ^ 2 * ((7 / 12 : ℝ) * (4 + y) * weylGradientEnergy Z -
        (5 / 4 : ℝ) * weylMatrixEnergy A Z) := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariant_projection_parameter_cost line 13824

Source documentation

The normalized invariant cost is bounded by the source's exact two spectral coefficients, retaining the actual total derivative energy.

theorem invariant_projection_parameter_cost (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (a : Vec) (Z : Angular.Gradient)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0)
    (S : Shape) (p k l : Vec)
    (he : (parameters S p k l).squaredNorm / 6 = weylGradientEnergy Z)
    (hB : weylMatrixEnergy A Z =
      curvatureContraction S (normalizedBlockNorm A) (parameters S p k l)) :
    generalCurvaturePairing A U
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariant_squared_weight_parameter_cost line 13848

Source documentation

The exact squared weight changes the denominator to the 9/64 coefficient; all remaining quantities are actual invariant energies.

theorem invariant_squared_weight_parameter_cost (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (M : ℝ) (hM : M ≠ 0) (p q : Vec) (Z : Angular.Gradient)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0)
    (S : Shape) (p' k l : Vec)
    (he : (parameters S p' k l).squaredNorm / 6 = weylGradientEnergy Z)
    (hp : ‖p'‖ ^ 2 = ‖p‖ ^ 2)
    (hB : weylMatrixEnergy A Z =
      curvatureContraction S (normalizedBlockNorm A) (parameters S p' k l)) :
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_four_apply line 13899
theorem OAI.PositiveEinsteinFour.Geometry.loweredCurvatureMatrix_apply line 13926
theorem OAI.PositiveEinsteinFour.Geometry.lowered_derivative_matrix line 13937
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_curvature_lowering line 13968
theorem OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates_second_bianchi line 13987
Source documentation
Differential Bianchi for the actual fully covariant curvature tensor.
```
theorem curvatureCoordinates_second_bianchi (g : SmoothMetric M) (c : M)
    (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hdet : (metricInChart g c z).det ≠ 0) :
    AlgebraicCurvature.DifferentialBianchi
      (curvatureDerivativeArray (covariantDerivative g c (curvatureCoordinates g c) z)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.AlgebraicCurvature.DifferentialBianchi, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_second_bianchi line 14001
theorem OAI.PositiveEinsteinFour.Geometry.frame_algebraic_firstSkew line 14031
theorem OAI.PositiveEinsteinFour.Geometry.frame_algebraic_firstBianchi line 14036
theorem OAI.PositiveEinsteinFour.Geometry.frame_algebraic_pairSymmetric line 14040
theorem OAI.PositiveEinsteinFour.Geometry.frame_algebraic_ricciThree line 14046
theorem OAI.PositiveEinsteinFour.Geometry.frame_einstein_decomposition_of_lastSkew line 14055
theorem OAI.PositiveEinsteinFour.Geometry.frame_weyl_symmetric_of_lastSkew line 14063
theorem OAI.PositiveEinsteinFour.Geometry.frame_weyl_traceFree_of_lastSkew line 14073
theorem OAI.PositiveEinsteinFour.Geometry.sectionalInput_of_lastSkew line 14081
theorem OAI.PositiveEinsteinFour.Geometry.integrable_of_ae_limit_norm_bound line 14111
theorem OAI.PositiveEinsteinFour.Geometry.regularizedRadialDerivative_factor line 14134
theorem OAI.PositiveEinsteinFour.Geometry.regularized_radial_energy_le line 14141
theorem OAI.PositiveEinsteinFour.Geometry.scalarTraceFreeHessian_eq_part line 14184
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.continuousTraceFreeSquare line 14194
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.continuousWeylHessianForm line 14205
theorem OAI.PositiveEinsteinFour.Geometry.ScalarCovariantData.weighted_bochner line 14215