AnalyticCoulomb.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.AnalyticCoulomb.contDiffAt_inverseDistance line 13

Source documentation

Inverse distance is real analytic off the diagonal; the statement also supplies every finite or infinite differentiability order.

theorem contDiffAt_inverseDistance {E : Type uE} {F : Type uF}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    {n : WithTop ENat} {f g : E → F} {x : E}
    (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x)
    (hne : f x ≠ g x) :
    ContDiffAt ℝ n (fun y => ‖f y - g y‖⁻¹) x := by
…

theorem OAI.Problem356.AnalyticCoulomb.contDiffAt_cost line 24

Source documentation

The real-valued Coulomb formula is analytic at every collision-free triple.

theorem contDiffAt_cost {n : WithTop ENat} (t : Triple)
    (h12 : t.1 ≠ t.2.1) (h13 : t.1 ≠ t.2.2) (h23 : t.2.1 ≠ t.2.2) :
    ContDiffAt ℝ n (fun p : Triple =>
      ‖p.1 - p.2.1‖⁻¹ + ‖p.1 - p.2.2‖⁻¹ + ‖p.2.1 - p.2.2‖⁻¹) t := by
…

Mentions: OAI.Problem356.Triple

theorem OAI.Problem356.AnalyticCoulomb.contDiffAt_partialFDeriv line 37

Source documentation

Analyticity of a parameter-dependent partial derivative. This is the stationarity-map regularity needed by the analytic implicit-function theorem.

theorem contDiffAt_partialFDeriv {P : Type uP} {S : Type uS} {R : Type uR}
    [NormedAddCommGroup P] [NormedSpace ℝ P]
    [NormedAddCommGroup S] [NormedSpace ℝ S]
    [NormedAddCommGroup R] [NormedSpace ℝ R]
    {F : P × S → R} {p : P × S}
    (hF : ContDiffAt ℝ (⊤ : WithTop ENat) F p) :
    ContDiffAt ℝ (⊤ : WithTop ENat)
      (fun q : P × S => fderiv ℝ (fun s => F (q.1, s)) q.2) p := by
…

theorem OAI.Problem356.AnalyticCoulomb.contDiffAt_partialHessian line 55

Source documentation

Joint analyticity of the state Hessian, hence its continuity for the positive-definiteness persistence step.

theorem contDiffAt_partialHessian {P : Type uP} {S : Type uS} {R : Type uR}
    [NormedAddCommGroup P] [NormedSpace ℝ P]
    [NormedAddCommGroup S] [NormedSpace ℝ S]
    [NormedAddCommGroup R] [NormedSpace ℝ R]
    {F : P × S → R} {p : P × S}
    (hF : ContDiffAt ℝ (⊤ : WithTop ENat) F p) :
    ContDiffAt ℝ (⊤ : WithTop ENat)
      (fun q : P × S => fderiv ℝ
        (fun s => fderiv ℝ (fun r => F (q.1, r)) s) q.2) p := by
…

theorem OAI.Problem356.AnalyticCoulomb.contDiffAt_stationarity line 68

Source documentation

In parameter/state coordinates (y,(x,z)), subtracting arbitrary analytic central and outer potentials leaves an analytic Coulomb stationarity map.

theorem contDiffAt_stationarity
    (u v : E3 → ℝ) (p : E3 × (E3 × E3))
    (hu : ContDiffAt ℝ (⊤ : WithTop ENat) u p.2.1)
    (hv : ContDiffAt ℝ (⊤ : WithTop ENat) v p.2.2)
    (hxy : p.2.1 ≠ p.1) (hxz : p.2.1 ≠ p.2.2) (hyz : p.1 ≠ p.2.2) :
    ContDiffAt ℝ (⊤ : WithTop ENat)
      (fun q : E3 × (E3 × E3) =>
        fderiv ℝ (fun s : E3 × E3 =>
          ‖s.1 - q.1‖⁻¹ + ‖s.1 - s.2‖⁻¹ + ‖q.1 - s.2‖⁻¹ - u s.1 - v s.2)
          q.2) p := by
…

Mentions: OAI.Problem356.E3