OAI/Analysis/CoulombTransport/HessianMatrix.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem356.CoulombCalculus.axisVector line 14

   Source documentation

   Unit coordinate vector for either local Coulomb branch.

   def axisVector (k : Fin 3) : EuclideanSpace ℝ (Fin 3) :=
   …

2. theorem OAI.Problem356.CoulombCalculus.norm_axisVector line 17
3. theorem OAI.Problem356.CoulombCalculus.inner_axisVector line 20
4. theorem OAI.Problem356.CoulombCalculus.pairHessian_axisVector line 26

   Source documentation

   The analytic Coulomb Hessian at a coordinate axis is precisely the diagonal matrix used in the finite-dimensional local nondegeneracy calculation.

   theorem pairHessian_axisVector (k : Fin 3) :
       pairHessian (axisVector k) =
         Matrix.toEuclideanCLM (𝕜 := ℝ) (LocalHessian.pairHessian k) := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.pairHessian, OAI.Problem356.CoulombCalculus.axisVector, OAI.Problem356.LocalHessian.pairHessian

5. theorem OAI.Problem356.CoulombCalculus.axisVector_ne_zero line 40
6. theorem OAI.Problem356.CoulombCalculus.pairHessian_axisVector_apply line 46
7. theorem OAI.Problem356.CoulombCalculus.pairHessian_neg_axisVector line 53
8. theorem OAI.Problem356.CoulombCalculus.pairHessian_two_axisVector line 58
9. theorem OAI.Problem356.CoulombCalculus.pairHessian_neg_two_axisVector line 64
10. theorem OAI.Problem356.GeometryJets.centerStateHessian_axisVector line 77

    Source documentation

    Identification of the center state derivative with the positive definite operator verified by the explicit finite matrix calculation.

    theorem centerStateHessian_axisVector (k : Fin 3) :
        centerStateHessian 20 (pairHessian (axisVector k)) = LocalHessian.stateOperator k := by
    …

    Mentions: OAI.Problem356.GeometryJets.centerStateHessian, OAI.Problem356.LocalHessian.stateOperator

11. theorem OAI.Problem356.GeometryJets.centerParameterDerivative_axisVector line 96
12. theorem OAI.Problem356.GeometryJets.fderiv_stationary_axis_state line 105

    Source documentation

    State partial derivative of the actual stationary field at an axis center.

    theorem fderiv_stationary_axis_state (k : Fin 3) :
        fderiv ℝ (stationaryEquation 20 (axisVector k))
          (axisVector k, (0, -axisVector k)) ∘L
            ContinuousLinearMap.inr ℝ (EuclideanSpace ℝ (Fin 3))
              (EuclideanSpace ℝ (Fin 3) × EuclideanSpace ℝ (Fin 3)) =
          LocalHessian.stateOperator k := by
    …

    Mentions: OAI.Problem356.GeometryJets.stationaryEquation, OAI.Problem356.LocalHessian.stateOperator

13. theorem OAI.Problem356.GeometryJets.fderiv_stationary_axis_parameter line 119

    Source documentation

    Parameter partial derivative of the actual stationary field at an axis center.

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

    Mentions: OAI.Problem356.GeometryJets.stationaryEquation, OAI.Problem356.LocalHessian.parameterOperator