AxisHessian.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Explicit nondegeneracy algebra for the two local Coulomb branches. The Hessian eigenvalues are 2 in the axial direction and -1 transversely. A common regularization parameter K = 20 works in every direction.

def OAI.Problem356.LocalHessian.eigenvalue line 16
Source documentation
Eigenvalue of the inverse-distance Hessian at a unit coordinate vector.
```
def eigenvalue (k i : Fin 3) : ℝ := if i = k then 2 else -1
```
def OAI.Problem356.LocalHessian.pairHessian line 19
Source documentation
The inverse-distance Hessian at either chosen unit coordinate vector.
```
def pairHessian (k : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ :=
…
```
def OAI.Problem356.LocalHessian.centralDerivative line 23
Source documentation
First derivative of the central stationary branch for K = 20.
```
def centralDerivative (k : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ :=
…
```
def OAI.Problem356.LocalHessian.oppositeDerivative line 27
Source documentation
First derivative of the opposite stationary branch for K = 20.
```
def oppositeDerivative (k : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ :=
…
```
def OAI.Problem356.LocalHessian.upperBlock line 31
Source documentation
Upper diagonal block of the regularized Hessian.
```
def upperBlock (k : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ :=
…
```
def OAI.Problem356.LocalHessian.lowerBlock line 35
Source documentation
Lower diagonal block of the regularized Hessian.
```
def lowerBlock (k : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ :=
…
```
def OAI.Problem356.LocalHessian.mixedBlock line 39
Source documentation
Mixed block of the regularized Hessian.
```
def mixedBlock (k : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ :=
…
```
def OAI.Problem356.LocalHessian.regularizedHessian line 43
Source documentation
The full six-dimensional regularized Hessian.
```
def regularizedHessian (k : Fin 3) :
    Matrix (Fin 3 ⊕ Fin 3) (Fin 3 ⊕ Fin 3) ℝ :=
…
```
lemma OAI.Problem356.LocalHessian.eigenvalue_cases line 47
lemma OAI.Problem356.LocalHessian.scalar_quadratic_coercive line 52
lemma OAI.Problem356.LocalHessian.scalar_quadratic_positive line 61
lemma OAI.Problem356.LocalHessian.scalar_quadratic_nonnegative line 73
lemma OAI.Problem356.LocalHessian.centralDerivative_isUnit line 83
lemma OAI.Problem356.LocalHessian.oppositeDerivative_isUnit line 90
lemma OAI.Problem356.LocalHessian.central_stationary_equation line 97
lemma OAI.Problem356.LocalHessian.opposite_stationary_equation line 107
lemma OAI.Problem356.LocalHessian.regularizedHessian_quadratic line 117
lemma OAI.Problem356.LocalHessian.regularizedHessian_isHermitian line 131
lemma OAI.Problem356.LocalHessian.regularizedHessian_posDef line 138
lemma OAI.Problem356.LocalHessian.regularizedHessian_isUnit line 159
lemma OAI.Problem356.LocalHessian.stationary_equation line 162