MatrixSlotOperator.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The varying matrix-slot curvature coefficient as an actual bounded operator. The extension to all matrix arrays is self-adjoint; on trace-free arrays it is the trace-free anticommutator used in the Weyl equation.

def OAI.PositiveEinsteinFour.Geometry.matrixEntryKernel line 23
def OAI.PositiveEinsteinFour.Geometry.matrixSlotKernel line 29
theorem OAI.PositiveEinsteinFour.Geometry.matrixEntryKernel_add line 32
theorem OAI.PositiveEinsteinFour.Geometry.matrixEntryKernel_smul line 38
theorem OAI.PositiveEinsteinFour.Geometry.matrixEntryKernel_symmetric line 44
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotKernel_add line 53
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotKernel_smul line 58
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotKernel_symmetric line 63
def OAI.PositiveEinsteinFour.Geometry.matrixSlotLinear line 71
def OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator line 88
Source documentation
The bounded operator that acts on every matrix slice of the Weyl gradient.
```
def matrixSlotOperator (A : Mat) : GradientVector →L[ℝ] GradientVector :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.GradientVector
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_apply line 91
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_selfadjoint line 96
Source documentation
The full-space extension is self-adjoint for every symmetric coefficient. Thus operator Green applies to its first derivatives as well.
```
theorem matrixSlotOperator_selfadjoint (A : Mat) (hA : symmetric A)
    (Z W : GradientVector) :
    inner ℝ (matrixSlotOperator A Z) W = inner ℝ Z (matrixSlotOperator A W) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.GradientVector, OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator
def OAI.PositiveEinsteinFour.Geometry.matrixSlotOperatorLinear line 109
def OAI.PositiveEinsteinFour.Geometry.matrixSlot line 123
Source documentation
Continuous linear dependence on the matrix coefficient.
```
def matrixSlot : Mat →L[ℝ] (GradientVector →L[ℝ] GradientVector) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.GradientVector
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlot_apply line 126
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_matrixSlot line 130
Source documentation
Differentiating the varying coefficient commutes with the concrete matrix-slot construction.
```
theorem hasDerivAt_matrixSlot {T : ℝ → Mat} {dT : Mat} {t : ℝ}
    (hT : HasDerivAt T dT t) :
    HasDerivAt (fun s => matrixSlotOperator (T s)) (matrixSlotOperator dT) t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator
def OAI.PositiveEinsteinFour.Geometry.matrixSlotAction line 136
Source documentation
The uncompressed trace-free anticommutator on a matrix.
```
def matrixSlotAction (A M : Mat) : Mat := fun a b =>
…
```
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotAction_diagonal line 140
theorem OAI.PositiveEinsteinFour.Geometry.matrixEntryKernel_action line 148
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_on_traceFree line 161
Source documentation
On actual trace-free gradient slices, the bounded operator is precisely B_F(A) rather than an independently postulated coefficient.
```
theorem matrixSlotOperator_on_traceFree (A : Mat) (Z : GradientVector)
    (hZ : ∀ i, (∑ a, Z (i, a, a)) = 0) (i : Fin 4) (a b : Fin 3) :
    matrixSlotOperator A Z (i, a, b) =
      matrixSlotAction A (fun c d => Z (i, c, d)) a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.GradientVector, OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.matrixSlotAction