Basic.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.HarmonicCounterexample.Space line 11
Also declared: ComparatorChallenges/HarmonicGrowth.lean:11 (same declaration text).
abbrev OAI.HarmonicCounterexample.Mat line 12
Also declared: ComparatorChallenges/HarmonicGrowth.lean:12 (same declaration text).
structure OAI.HarmonicCounterexample.SmoothMetric line 15
Source documentation
A genuine smooth positive definite covariant metric tensor on R^n.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:15 (same declaration text).
```
structure SmoothMetric (n : ℕ) where
…
```
def OAI.HarmonicCounterexample.coordDeriv line 21
Source documentation
The coordinate directional derivative.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:21 (same declaration text).
```
def coordDeriv {n : ℕ} (i : Fin n) (f : Space n → ℝ) (x : Space n) : ℝ :=
…
```
Mentions: OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.christoffel line 25
Source documentation
Levi-Civita connection in the single global Cartesian chart.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:25 (same declaration text).
```
def christoffel {n : ℕ} (g : SmoothMetric n) (x : Space n)
    (k i j : Fin n) : ℝ :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.ricci line 33
Source documentation
Ricci tensor, with the convention in which the round sphere has positive Ricci.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:33 (same declaration text).
```
def ricci {n : ℕ} (g : SmoothMetric n) (x : Space n) (i j : Fin n) : ℝ :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.RicciNonnegative line 39
Also declared: ComparatorChallenges/HarmonicGrowth.lean:39 (same declaration text).
def OAI.HarmonicCounterexample.laplaceBeltrami line 43
Source documentation
Trace of the covariant Hessian, i.e. the Laplace-Beltrami operator.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:43 (same declaration text).
```
def laplaceBeltrami {n : ℕ} (g : SmoothMetric n) (u : Space n → ℝ)
    (x : Space n) : ℝ :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.pathLength line 49
Source documentation
Riemannian length of a path on the unit parameter interval.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:49 (same declaration text).
```
def pathLength {n : ℕ} (g : SmoothMetric n) (γ : ℝ → Space n) : ℝ :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.distance line 54
Source documentation
Infimum of smooth path lengths, the intrinsic Riemannian distance.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:54 (same declaration text).
```
def distance {n : ℕ} (g : SmoothMetric n) (x y : Space n) : ℝ :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.Complete line 59
Source documentation
Sequential metric completeness, for the intrinsic distance, not the background one.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:59 (same declaration text).
```
def Complete {n : ℕ} (g : SmoothMetric n) : Prop :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric
def OAI.HarmonicCounterexample.EuclideanNearOrigin line 64
Also declared: ComparatorChallenges/HarmonicGrowth.lean:64 (same declaration text).
def OAI.HarmonicCounterexample.ballVolume line 68
Source documentation
Riemannian measure of the intrinsic open ball, retaining infinite values.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:68 (same declaration text).
```
def ballVolume {n : ℕ} (g : SmoothMetric n) (R : ℝ) : ℝ≥0∞ :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric
def OAI.HarmonicCounterexample.omega line 73
Source documentation
The ordinary Euclidean unit ball volume, in Cartesian Lebesgue measure.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:73 (same declaration text).
```
def omega (n : ℕ) : ℝ≥0∞ :=
…
```
def OAI.HarmonicCounterexample.PositiveSubunitAVR line 77
Source documentation
The volume-ratio limit is finite, positive, and strictly below one.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:77 (same declaration text).
```
def PositiveSubunitAVR {n : ℕ} (g : SmoothMetric n) : Prop :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric
def OAI.HarmonicCounterexample.HarmonicGrowth line 83
Source documentation
Membership in the actual space H_k, with the bound required at every point.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:83 (same declaration text).
```
def HarmonicGrowth {n : ℕ} (g : SmoothMetric n) (k : ℕ) (u : Space n → ℝ) : Prop :=
…
```
Mentions: OAI.HarmonicCounterexample.SmoothMetric, OAI.HarmonicCounterexample.Space
def OAI.HarmonicCounterexample.euclideanDimension line 88
Also declared: ComparatorChallenges/HarmonicGrowth.lean:88 (same declaration text).
def OAI.HarmonicCounterexample.MainClaim line 92
Source documentation
The manuscript's unconditional main existence claim.
Also declared: ComparatorChallenges/HarmonicGrowth.lean:92 (same declaration text).
```
def MainClaim : Prop :=
…
```