CoulombCharts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.CoulombCharts.centerStateHessian_axis_eq line 17
Source documentation
The computed state derivative is the coercive, invertible operator certified by the finite-dimensional algebra, in the actual product-space coordinates.
```
theorem centerStateHessian_axis_eq (k : Fin 3) :
    centerStateHessian 20 (CoulombCalculus.pairHessian (axisVector k)) =
      LocalHessian.stateOperator k := by
…
```
Mentions: OAI.Problem356.CoulombCalculus.pairHessian, OAI.Problem356.LocalHessian.stateOperator
theorem OAI.Problem356.CoulombCharts.centerParameterDerivative_axis_eq line 33
Source documentation
The computed parameter derivative agrees with the mixed Hessian block.
```
theorem centerParameterDerivative_axis_eq (k : Fin 3) :
    centerParameterDerivative (CoulombCalculus.pairHessian (axisVector k)) =
      LocalHessian.parameterOperator k := by
…
```
Mentions: OAI.Problem356.CoulombCalculus.pairHessian, OAI.Problem356.LocalHessian.parameterOperator
theorem OAI.Problem356.CoulombCharts.stationary_state_partial_eq line 42

theorem OAI.Problem356.CoulombCharts.stationary_parameter_partial_eq line 56

Source documentation

Identification of the actual partial parameter derivative.

theorem stationary_parameter_partial_eq (k : Fin 3) :
    fderiv ℝ (stationaryEquation 20 (axisVector k))
        (axisVector k, (0, -axisVector k)) ∘L
      ContinuousLinearMap.inl ℝ E3 (E3 × E3) = LocalHessian.parameterOperator k := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.LocalHessian.parameterOperator

theorem OAI.Problem356.CoulombCharts.nonempty_coulombCharts line 71
Source documentation
Nonlinear local Coulomb branches exist at every coordinate-axis reference triple. Both branch coordinates are analytic local diffeomorphisms on one common source.
```
theorem nonempty_coulombCharts (k : Fin 3) :
    Nonempty (AnalyticStationaryCharts
      (stationaryEquation 20 (axisVector k)) (axisVector k) (0, -axisVector k)) := by
…
```