StationaryMap.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.StationaryMap.statePotential line 18
Source documentation
The state potential with the explicit common central quadratic, K = 20.
```
def statePotential (a y : E) (s : E × E) : ℝ :=
…
```
def OAI.Problem356.StationaryMap.stationary line 24
Source documentation
The concrete stationary equation, with parameter first and state second.
```
def stationary (a : E) (p : E × (E × E)) : E × E :=
…
```
theorem OAI.Problem356.StationaryMap.contDiffAt_stationary line 30
Source documentation
Analyticity of the actual stationary equation on pairwise-distinct triples.
```
theorem contDiffAt_stationary (a : E) {p : E × (E × E)}
    (hxy : p.2.1 ≠ p.1) (hxz : p.2.1 ≠ p.2.2) (hzy : p.2.2 ≠ p.1)
    {n : WithTop ENat} : ContDiffAt ℝ n (stationary a) p := by
…
```
Mentions: OAI.Problem356.StationaryMap.stationary
theorem OAI.Problem356.StationaryMap.contDiffAt_statePotential line 46
Source documentation
Analyticity of the state potential away from all collisions.
```
theorem contDiffAt_statePotential (a y : E) {s : E × E}
    (hxy : s.1 ≠ y) (hxz : s.1 ≠ s.2) (hzy : s.2 ≠ y)
    {n : WithTop ENat} : ContDiffAt ℝ n (statePotential a y) s := by
…
```
Mentions: OAI.Problem356.StationaryMap.statePotential
def OAI.Problem356.StationaryMap.jointPotential line 62
Source documentation
The scalar potential with parameter and state bundled together.
```
def jointPotential (a : E) (p : E × (E × E)) : ℝ := statePotential a p.1 p.2
```
Mentions: OAI.Problem356.StationaryMap.statePotential

theorem OAI.Problem356.StationaryMap.contDiffAt_jointPotential line 65

Source documentation

Joint parameter/state analyticity on pairwise-distinct triples.

theorem contDiffAt_jointPotential (a : E) {p : E × (E × E)}
    (hxy : p.2.1 ≠ p.1) (hxz : p.2.1 ≠ p.2.2) (hzy : p.2.2 ≠ p.1)
    {n : WithTop ENat} : ContDiffAt ℝ n (jointPotential a) p := by
…

Mentions: OAI.Problem356.StationaryMap.jointPotential

def OAI.Problem356.StationaryMap.stateDifferential line 80
Source documentation
The linear form represented by the two components of the stationary map.
```
def stateDifferential (a y : E) (s : E × E) : E × E →L[ℝ] ℝ :=
…
```
theorem OAI.Problem356.StationaryMap.hasFDerivAt_statePotential line 85
Source documentation
The displayed stationary equation really is the state derivative of the supporting potential.
```
theorem hasFDerivAt_statePotential (a y : E) {s : E × E}
    (hxy : s.1 ≠ y) (hxz : s.1 ≠ s.2) (hzy : s.2 ≠ y) :
    HasFDerivAt (statePotential a y) (stateDifferential a y s) s := by
…
```
Mentions: OAI.Problem356.StationaryMap.statePotential, OAI.Problem356.StationaryMap.stateDifferential
def OAI.Problem356.StationaryMap.stationaryDifferential line 106
Source documentation
The full parameter/state derivative of the concrete stationary equation.
```
def stationaryDifferential (p : E × (E × E)) :
    E × (E × E) →L[ℝ] E × E :=
…
```
theorem OAI.Problem356.StationaryMap.hasFDerivAt_stationary line 116
theorem OAI.Problem356.StationaryMap.hasFDerivAt_statePotential_zero line 135
Source documentation
A zero of the explicit stationary map is a stationary point of the scalar potential.
```
theorem hasFDerivAt_statePotential_zero (a y : E) {s : E × E}
    (hxy : s.1 ≠ y) (hxz : s.1 ≠ s.2) (hzy : s.2 ≠ y)
    (hzero : stationary a (y, s) = 0) :
    HasFDerivAt (statePotential a y) (0 : E × E →L[ℝ] ℝ) s := by
…
```
Mentions: OAI.Problem356.StationaryMap.stationary, OAI.Problem356.StationaryMap.statePotential