GeometryJets.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.GeometryJets.KernelDerivative line 16
Source documentation
The derivative interface supplied by the inverse-norm calculus.
```
def KernelDerivative : Prop :=
…
```
theorem OAI.Problem356.GeometryJets.kernelDerivative line 20
theorem OAI.Problem356.GeometryJets.center_nonzero line 25

theorem OAI.Problem356.GeometryJets.hasFDerivAt_center_x line 30

Source documentation

The two opposite outer centers cancel the derivative in the central coordinate.

theorem hasFDerivAt_center_x
    (a : E) (ha : ‖a‖ = 1) :
    HasFDerivAt
      (fun x : E => ‖x - a‖⁻¹ + ‖x - (-a)‖⁻¹ + ‖a - (-a)‖⁻¹)
      (0 : E →L[ℝ] ℝ) (0 : E) := by
…

theorem OAI.Problem356.GeometryJets.hasFDerivAt_center_z line 45

Source documentation

The derivative in the negative outer coordinate at an opposite unit pair.

theorem hasFDerivAt_center_z
    (a : E) (ha : ‖a‖ = 1) :
    HasFDerivAt
      (fun z : E => ‖(0 : E) - a‖⁻¹ + ‖(0 : E) - z‖⁻¹ + ‖a - z‖⁻¹)
      ((5 / 4 : ℝ) • innerSL ℝ a) (-a) := by
…

theorem OAI.Problem356.GeometryJets.hasFDerivAt_center_state line 69

Source documentation

Joint state derivative, with the positive outer coordinate held fixed.

theorem hasFDerivAt_center_state
    (a : E) (ha : ‖a‖ = 1) :
    HasFDerivAt
      (fun p : E × E => ‖p.1 - a‖⁻¹ + ‖p.1 - p.2‖⁻¹ + ‖a - p.2‖⁻¹)
      ((5 / 4 : ℝ) • (innerSL ℝ a).comp (ContinuousLinearMap.snd ℝ E E))
      (0, -a) := by
…

theorem OAI.Problem356.GeometryJets.hasFDerivAt_center_stationary line 99

Source documentation

Subtracting the common central and negative outer potentials makes the center stationary.

theorem hasFDerivAt_center_stationary
    (a : E) (ha : ‖a‖ = 1) (K : ℝ) :
    HasFDerivAt
      (fun p : E × E =>
        (‖p.1 - a‖⁻¹ + ‖p.1 - p.2‖⁻¹ + ‖a - p.2‖⁻¹) -
        ((5 / 2 : ℝ) - K / 2 * ‖p.1‖ ^ 2) -
        ((5 / 4 : ℝ) * inner ℝ a (p.2 + a) - K / 2 * ‖p.2 + a‖ ^ 2))
      (0 : (E × E) →L[ℝ] ℝ) (0, -a) := by
…