OAI/Analysis/CoulombTransport/StationaryEquation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem356.GeometryJets.stationaryEquation line 17

    Source documentation

    The state gradient of the regularized three-body Coulomb cost. The input is (parameter, (central point, negative outer point)).

    def stationaryEquation (K : ℝ) (a : E) (p : E × (E × E)) : E × E :=
…
  2. def OAI.Problem356.GeometryJets.centerStateHessian line 23

    Source documentation

    The center state Hessian, expressed using the single-pair unit-center Hessian.

    def centerStateHessian (K : ℝ) (Q : E →L[ℝ] E) : (E × E) →L[ℝ] (E × E) :=
…
  3. def OAI.Problem356.GeometryJets.centerParameterDerivative line 31

    Source documentation

    The center derivative with respect to the moving positive outer point.

    def centerParameterDerivative (Q : E →L[ℝ] E) : E →L[ℝ] (E × E) :=
…
  4. lemma OAI.Problem356.GeometryJets.stationaryEquation_center line 34
  5. lemma OAI.Problem356.GeometryJets.hessian_neg_center line 40
  6. lemma OAI.Problem356.GeometryJets.hessian_double_center line 45
  7. lemma OAI.Problem356.GeometryJets.hasFDerivAt_stationary_state_center line 52
  8. lemma OAI.Problem356.GeometryJets.hasFDerivAt_stationary_parameter_center line 79
  9. lemma OAI.Problem356.GeometryJets.contDiffAt_stationaryEquation line 101
  10. lemma OAI.Problem356.GeometryJets.contDiffAt_stationaryEquation_center line 113
  11. def OAI.Problem356.GeometryJets.centerTotalDerivative line 130

    Source documentation

    Total differential with the parameter block followed by the state block.

    def centerTotalDerivative (K : ℝ) (Q : E →L[ℝ] E) :
    (E × (E × E)) →L[ℝ] (E × E) :=
…
  12. lemma OAI.Problem356.GeometryJets.hasFDerivAt_stationary_center line 135