OAI/Analysis/CoulombTransport/HessianCLM.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem356.LocalHessian.toEuclideanCLM_isInvertible line 15

    Source documentation

    Invertible matrices induce invertible continuous linear maps in Euclidean coordinates.

    lemma toEuclideanCLM_isInvertible {n : Type uN} [Fintype n] [DecidableEq n]
    (A : Matrix n n ℝ) (hA : IsUnit A) :
    (Matrix.toEuclideanCLM (n := n) (𝕜 := ℝ) A).IsInvertible := by
…
  2. abbrev OAI.Problem356.LocalHessian.AxisSpace line 21
  3. abbrev OAI.Problem356.LocalHessian.StateSpace line 22
  4. abbrev OAI.Problem356.LocalHessian.JointSpace line 23
  5. def OAI.Problem356.LocalHessian.stateCoordinates line 26

    Source documentation

    Passing from sum coordinates to the product coordinates used by the implicit function theorem.

    def stateCoordinates : JointSpace ≃L[ℝ] StateSpace := EuclideanSpace.sumEquivProd

    Mentions: OAI.Problem356.LocalHessian.JointSpace, OAI.Problem356.LocalHessian.StateSpace

  6. def OAI.Problem356.LocalHessian.stateOperator line 29

    Source documentation

    The regularized state derivative as a continuous linear map on product space.

    def stateOperator (k : Fin 3) : StateSpace →L[ℝ] StateSpace :=
…

    Mentions: OAI.Problem356.LocalHessian.StateSpace

  7. lemma OAI.Problem356.LocalHessian.stateOperator_isInvertible line 34
  8. lemma OAI.Problem356.LocalHessian.centralDerivativeCLM_isInvertible line 41
  9. lemma OAI.Problem356.LocalHessian.oppositeDerivativeCLM_isInvertible line 45
  10. lemma OAI.Problem356.LocalHessian.regularizedHessian_coercive line 49
  11. lemma OAI.Problem356.LocalHessian.stateCoordinates_symm_inl line 62
  12. lemma OAI.Problem356.LocalHessian.stateCoordinates_symm_inr line 65
  13. lemma OAI.Problem356.LocalHessian.stateOperator_fst_apply line 68
  14. lemma OAI.Problem356.LocalHessian.stateOperator_snd_apply line 76
  15. lemma OAI.Problem356.LocalHessian.stateOperator_joint_coercive line 84
  16. lemma OAI.Problem356.LocalHessian.stateOperator_coercive line 96
  17. def OAI.Problem356.LocalHessian.parameterOperator line 109

    Source documentation

    The derivative in the parameter variable at the center.

    def parameterOperator (k : Fin 3) : AxisSpace →L[ℝ] StateSpace :=
…

    Mentions: OAI.Problem356.LocalHessian.AxisSpace, OAI.Problem356.LocalHessian.StateSpace

  18. def OAI.Problem356.LocalHessian.branchOperator line 114

    Source documentation

    The derivative of the stationary branch: central and opposite components.

    def branchOperator (k : Fin 3) : AxisSpace →L[ℝ] StateSpace :=
…

    Mentions: OAI.Problem356.LocalHessian.AxisSpace, OAI.Problem356.LocalHessian.StateSpace

  19. lemma OAI.Problem356.LocalHessian.branchOperator_fst_apply line 118
  20. lemma OAI.Problem356.LocalHessian.branchOperator_snd_apply line 123
  21. lemma OAI.Problem356.LocalHessian.parameterOperator_fst_apply line 128
  22. lemma OAI.Problem356.LocalHessian.parameterOperator_snd_apply line 133
  23. lemma OAI.Problem356.LocalHessian.stateOperator_comp_branchOperator line 139
  24. lemma OAI.Problem356.LocalHessian.neg_inverse_comp_parameterOperator line 159
  25. lemma OAI.Problem356.LocalHessian.central_inverse_block_isInvertible line 171
  26. lemma OAI.Problem356.LocalHessian.opposite_inverse_block_isInvertible line 177