CoupledOperator.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The actual real coupled operator used for the plus projection.

def OAI.PositiveEinsteinFour.HighestHessian.rawWeight line 16
Source documentation
A real outer vector tensored with an arbitrary matrix-valued four-vector.
```
def rawWeight (a : Vec) (Z : RawGradient) : Hessian := fun i j b c => a i * Z b c j
```
theorem OAI.PositiveEinsteinFour.HighestHessian.rawWeight_add line 18
theorem OAI.PositiveEinsteinFour.HighestHessian.rawWeight_smul line 24
theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_rawWeight line 31
Source documentation
The total infinitesimal action obeys the product rule on an actual tensor.
```
theorem totalPlus_rawWeight (s : Fin 3) (a : Vec) (Z : RawGradient) :
    totalPlus s (rawWeight a Z) =
      rawWeight (quaternion s a) Z + rawWeight a (rawGradientGenerator s Z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.rawWeight
def OAI.PositiveEinsteinFour.HighestHessian.couplingKernel line 46
Source documentation
The matrix kernel of Σ I_outer,s (I_inner,s + Σ_s).
```
def couplingKernel (p q : TensorIndex) : ℝ := ∑ s : Fin 3,
…
```
def OAI.PositiveEinsteinFour.HighestHessian.coupledOperator line 55
theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_coordinates line 58
theorem OAI.PositiveEinsteinFour.HighestHessian.couplingKernel_symmetric line 64
theorem OAI.PositiveEinsteinFour.HighestHessian.symmetric_matrix_pairing line 78
theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_selfadjoint line 91

theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_apply line 100

Source documentation

Entrywise kernel reduction to the two actual slot actions.

theorem coupledOperator_apply (X : Hessian) (i j : Fin 4) (a b : Fin 3) :
    coupledOperator X i j a b = ∑ s : Fin 3, ∑ k : Fin 4,
      quaternionMatrix s i k * ((∑ l : Fin 4, quaternionMatrix s j l * X k l a b) +
        matrixAction s (X k j) a b) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.coupledOperator

theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_add line 113
theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_smul line 121
theorem OAI.PositiveEinsteinFour.HighestHessian.coupledOperator_rawWeight line 129
Source documentation
The actual coupled operator on a real rank-one tensor.
```
theorem coupledOperator_rawWeight (a : Vec) (Z : RawGradient) :
    coupledOperator (rawWeight a Z) =
      ∑ s : Fin 3, rawWeight (quaternion s a) (rawGradientGenerator s Z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.coupledOperator, OAI.PositiveEinsteinFour.HighestHessian.rawWeight
def OAI.PositiveEinsteinFour.HighestHessian.plusPolynomial line 148
Source documentation
The actual polynomial used for the total-plus spectral projection.
```
def plusPolynomial (X : Hessian) : Hessian :=
…
```