RealVectorProjection.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The real-vector norm calculation behind the plus projection cost.

theorem OAI.PositiveEinsteinFour.Bianchi.quaternion_combination_norm_sq line 17
Source documentation
The real quaternion frame is orthogonal, with common norm |a|. This includes the scalar direction and avoids any complex factorization.
```
theorem quaternion_combination_norm_sq (a : Vec) (r : ℝ) (c : Fin 3 → ℝ) :
    (∑ i : Fin 4, (r * a i + ∑ s : Fin 3, c s * quaternion s a i) ^ 2) =
      (r ^ 2 + ∑ s : Fin 3, c s ^ 2) * ‖a‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.quaternion
def OAI.PositiveEinsteinFour.Bianchi.weightCoupling line 24
Source documentation
The coupled action on a real rank-one weight tensor.
```
def weightCoupling (a : Vec) (Z : Tensor) : Hessian := fun i j b c =>
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
def OAI.PositiveEinsteinFour.Bianchi.weightDoubleCoupling line 28
Source documentation
The twice-coupled action, retaining the ordered generator products.
```
def weightDoubleCoupling (a : Vec) (Z : Tensor) : Hessian := fun i j b c =>
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.weightCoupling_polynomial line 34
Source documentation
The coupled polynomial follows from the actual generator commutators and Casimir, rather than a tensor-representation decomposition.
```
theorem weightCoupling_polynomial (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) (i j : Fin 4) (b c : Fin 3) :
    weightDoubleCoupling a Z i j b c =
      35 * a i * Z.matrix b c j + 2 * weightCoupling a Z i j b c := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightDoubleCoupling, OAI.PositiveEinsteinFour.Bianchi.weightCoupling
def OAI.PositiveEinsteinFour.Bianchi.weightPlusPart line 56
Source documentation
The explicit polynomial (7-K)(a ⊗ Z)/12, where K = Σ I_outer,s ⊗ (I_inner,s + Σ_s).
```
def weightPlusPart (a : Vec) (Z : Tensor) : Hessian := fun i j b c =>
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.weightPlusPart_outer_norm line 59
theorem OAI.PositiveEinsteinFour.Bianchi.weightPlusPart_norm line 80
Source documentation
The coefficient 7/12 is proved directly for real vectors using the actual Bianchi Casimir, with no representation or partial-trace premise.
```
theorem weightPlusPart_norm (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    hessianNormSq (weightPlusPart a Z) = (7 / 12) * ‖a‖ ^ 2 * Z.squaredNorm := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightPlusPart