Basic.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.AffineBernstein.Space line 10
Also declared: ComparatorChallenges/AffineBernstein.lean:12 (same declaration text).
def OAI.AffineBernstein.coordinateVector line 12
Also declared: ComparatorChallenges/AffineBernstein.lean:14 (same declaration text).
def OAI.AffineBernstein.hessian line 17
Source documentation
Coordinate Hessian. On the open domain it depends only on the restriction of u. The order of the two differentiations is immaterial under the smoothness hypothesis.
Also declared: ComparatorChallenges/AffineBernstein.lean:19 (same declaration text).
```
def hessian {n : ℕ} (u : Space n → ℝ) (x : Space n) : Matrix (Fin n) (Fin n) ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.cofactorHessian line 22
Source documentation
The coefficient U^{ij} = det(D²u) (D²u)^{-1}_{ij}.
Also declared: ComparatorChallenges/AffineBernstein.lean:24 (same declaration text).
```
def cofactorHessian {n : ℕ} (u : Space n → ℝ) (x : Space n) :
    Matrix (Fin n) (Fin n) ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.affineWeight line 27
Source documentation
The classical determinant weight; in particular, this is not a generalized exponent.
Also declared: ComparatorChallenges/AffineBernstein.lean:29 (same declaration text).
```
def affineWeight {n : ℕ} (u : Space n → ℝ) (x : Space n) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.AffineMaximalOn line 30
Also declared: ComparatorChallenges/AffineBernstein.lean:32 (same declaration text).
def OAI.AffineBernstein.graphPathLength line 37
Source documentation
Length on [0,1] for g_x(v,v) = ‖v‖² + (Du_x v)², the metric induced by the Euclidean graph embedding x ↦ (x,u(x)). The product norm on Lean's ordinary product type is NOT used (it would be the maximum norm).
Also declared: ComparatorChallenges/AffineBernstein.lean:39 (same declaration text).
```
def graphPathLength {n : ℕ} (u : Space n → ℝ) (γ : ℝ → Space n) : ℝ≥0∞ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.graphEDist line 46
Source documentation
The intrinsic extended distance: infimum of lengths of C¹ paths in the domain. Using a single C¹ path gives the same intrinsic distance as piecewise C¹ paths, by smooth endpoint reparameterization and concatenation.
Also declared: ComparatorChallenges/AffineBernstein.lean:48 (same declaration text).
```
def graphEDist {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
    (x y : Space n) : ℝ≥0∞ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.EuclideanGraphComplete line 56
Source documentation
Sequential completeness for the induced Euclidean path metric. This states that every intrinsic Cauchy sequence of points in Ω has an intrinsic limit in Ω. It imposes no growth condition and no completeness condition on the affine metric.
Also declared: ComparatorChallenges/AffineBernstein.lean:58 (same declaration text).
```
def EuclideanGraphComplete {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ) : Prop :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.graph line 64
Source documentation
The graph, regarded as an affine subset of R^{n+1}.
Also declared: ComparatorChallenges/AffineBernstein.lean:66 (same declaration text).
```
def graph {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ) : Set (Space n × ℝ) :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.standardParaboloid line 67
Also declared: ComparatorChallenges/AffineBernstein.lean:69 (same declaration text).