RealVectorCost.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The second real-vector projection identity in actual tensor coordinates.

def OAI.PositiveEinsteinFour.Bianchi.rawNorm line 17
Source documentation
Frobenius norm of an arbitrary matrix of real four-vectors.
```
def rawNorm (Z : RawGradient) : ℝ := ∑ b, ∑ c, ‖Z b c‖ ^ 2
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.RawGradient
theorem OAI.PositiveEinsteinFour.Bianchi.rawNorm_matrix line 19
theorem OAI.PositiveEinsteinFour.Bianchi.rawNorm_smul line 21
def OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient line 27
Source documentation
Quaternion coefficient of the total derivative of (7-K)L.
```
def rawCostCoefficient (s r : Fin 3) (Z : RawGradient) : RawGradient :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.RawGradient
theorem OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient_coordinates line 35
theorem OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient_norm line 44
Source documentation
The coefficient identity uses the actual twelve Bianchi coordinates.
```
theorem rawCostCoefficient_norm (s : Fin 3) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    64 * rawNorm (rawGradientGenerator s Z.matrix) +
      (∑ r : Fin 3, rawNorm (rawCostCoefficient s r Z.matrix)) =
        84 * Z.squaredNorm + 108 * rawNorm (rawGradientGenerator s Z.matrix) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawNorm, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator, OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient
def OAI.PositiveEinsteinFour.Bianchi.quaternionCombination line 55
Source documentation
A real outer quaternion combination, keeping all inner correlations.
```
def quaternionCombination (a : Vec) (Z : RawGradient)
    (C : Fin 3 → RawGradient) : Hessian := fun i j b c =>
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.RawGradient
theorem OAI.PositiveEinsteinFour.Bianchi.quaternionCombination_slice_norm line 59
theorem OAI.PositiveEinsteinFour.Bianchi.quaternionCombination_norm line 67
Source documentation
No product assumption is made on the inner plus and minus factors.
```
theorem quaternionCombination_norm (a : Vec) (Z : RawGradient)
    (C : Fin 3 → RawGradient) :
    hessianNormSq (quaternionCombination a Z C) =
      ‖a‖ ^ 2 * (rawNorm Z + ∑ s : Fin 3, rawNorm (C s)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.RawGradient, OAI.PositiveEinsteinFour.Bianchi.quaternionCombination, OAI.PositiveEinsteinFour.Bianchi.rawNorm
theorem OAI.PositiveEinsteinFour.Bianchi.weightPlusPart_linearCombination line 89
theorem OAI.PositiveEinsteinFour.Bianchi.totalPlus_weightPlusPart line 98
Source documentation
The total generator is evaluated before taking its norm.
```
theorem totalPlus_weightPlusPart (s : Fin 3) (a : Vec) (Z : Tensor) :
    totalPlus s (weightPlusPart a Z) = (1 / 12 : ℝ) •
      quaternionCombination a ((8 : ℝ) • rawGradientGenerator s Z.matrix)
        (fun r => rawCostCoefficient s r Z.matrix) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart, OAI.PositiveEinsteinFour.Bianchi.quaternionCombination, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator, OAI.PositiveEinsteinFour.Bianchi.rawCostCoefficient
theorem OAI.PositiveEinsteinFour.Bianchi.hessianNormSq_smul line 114
theorem OAI.PositiveEinsteinFour.Bianchi.totalPlus_weightPlusPart_norm line 120
Source documentation
The real-vector identity is proved separately for each actual generator.
```
theorem totalPlus_weightPlusPart_norm (s : Fin 3) (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    hessianNormSq (totalPlus s (weightPlusPart a Z)) = ‖a‖ ^ 2 *
      ((7 / 12) * Z.squaredNorm +
        (3 / 4) * rawNorm (rawGradientGenerator s Z.matrix)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart, OAI.PositiveEinsteinFour.Bianchi.rawNorm, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator
theorem OAI.PositiveEinsteinFour.Bianchi.totalPlus_weightPlusPart_curvature line 133
Source documentation
The weighted trace-free contraction, with the source's positive one-half coefficient and without a partial-trace assumption.
```
theorem totalPlus_weightPlusPart_curvature (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    -(∑ s, t s * hessianNormSq (totalPlus s (weightPlusPart a Z))) / 60 =
      (1 / 2 : ℝ) * ‖a‖ ^ 2 *
        (-(∑ s, t s * rawNorm (rawGradientGenerator s Z.matrix)) / 40) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart, OAI.PositiveEinsteinFour.Bianchi.rawNorm, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator

theorem OAI.PositiveEinsteinFour.Bianchi.totalPlus_weightPlusPart_matrixCost line 146

Source documentation

The second real-vector identity ends in the actual matrix-slot contraction.

theorem totalPlus_weightPlusPart_matrixCost (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    -(∑ s, t s * hessianNormSq (totalPlus s (weightPlusPart a Z))) / 60 =
      (1 / 2 : ℝ) * ‖a‖ ^ 2 *
        (∑ s, t s * (∑ b, ‖Z.matrix s b‖ ^ 2)) := by
…

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

theorem OAI.PositiveEinsteinFour.Bianchi.rawGenerator_energy line 158
Source documentation
The raw inner energy is the Bianchi Casimir.
```
theorem rawGenerator_energy (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ s : Fin 3, rawNorm (rawGradientGenerator s Z.matrix)) = 35 * Z.squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.rawNorm, OAI.PositiveEinsteinFour.Bianchi.rawGradientGenerator
theorem OAI.PositiveEinsteinFour.Bianchi.weightPlusPart_plus_energy line 170
Source documentation
The explicit real plus part has actual total-plus energy forty-eight.
```
theorem weightPlusPart_plus_energy (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    (∑ s : Fin 3, hessianNormSq (totalPlus s (weightPlusPart a Z))) =
      48 * hessianNormSq (weightPlusPart a Z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart
theorem OAI.PositiveEinsteinFour.Bianchi.weightPlusPart_eq_plusPolynomial line 182
Source documentation
This is the same explicit polynomial as the self-adjoint coupled operator.
```
theorem weightPlusPart_eq_plusPolynomial (a : Vec) (Z : Tensor) :
    weightPlusPart a Z = plusPolynomial (weightTensor a Z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart