ParametricGraphJets.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.horizontalJacobian line 13
Source comment
The actual first derivative of the horizontal component, in graph coordinates.
```
def horizontalJacobian {n : ℕ} (a : Fin n → Space n → ℝ) (x : Space n) :
    Matrix (Fin n) (Fin n) ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.normalVariation line 18
Source comment
The graph's normal component of an arbitrary parametrized velocity.
```
def normalVariation {n : ℕ} (u β : Space n → ℝ) (a : Fin n → Space n → ℝ)
    (x : Space n) : ℝ := β x - ∑ k, dirDeriv (coordinateVector n k) u x * a k x
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector
def OAI.AffineBernstein.verticalVariation line 22
Source comment
The vertical velocity reconstructed from its normal part and horizontal part.
```
def verticalVariation {n : ℕ} (u η : Space n → ℝ) (a : Fin n → Space n → ℝ)
    (x : Space n) : ℝ := η x + ∑ k, dirDeriv (coordinateVector n k) u x * a k x
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector
def OAI.AffineBernstein.graphVariationArea line 26
Source comment
Actual affine-area density of the variation, in its exact graph jets.
```
def graphVariationArea {n : ℕ} (u β : Space n → ℝ) (a : Fin n → Space n → ℝ)
    (x : Space n) (t : ℝ) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.third_dirDeriv_comm line 33
lemma OAI.AffineBernstein.hessian_dirDeriv line 46
lemma OAI.AffineBernstein.hessian_sum_on line 53
lemma OAI.AffineBernstein.contDiffOn_dirDeriv line 67
lemma OAI.AffineBernstein.inverse_column_contraction line 73
lemma OAI.AffineBernstein.trace_hessian_verticalVariation line 80