Model.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.WeakMTWTransport.Model line 12
Also declared: ComparatorChallenges/BiholderTransport.lean:12 (same declaration text).
def OAI.WeakMTWTransport.cost line 19
Source documentation
Squared-distance cost with factor one half.
Also declared: ComparatorChallenges/BiholderTransport.lean:19 (same declaration text).
```
def cost (x y : M) : ℝ := dist x y ^ 2 / 2
```
def OAI.WeakMTWTransport.euclideanVolumeFactor line 22
Source documentation
Calibration of Hausdorff measure to Euclidean volume.
Also declared: ComparatorChallenges/BiholderTransport.lean:22 (same declaration text).
```
def euclideanVolumeFactor (n : ℕ) : ℝ≥0∞ :=
…
```
def OAI.WeakMTWTransport.metricVolume line 30
Source documentation
Riemannian volume calibrated to Lebesgue measure in Euclidean space.
Also declared: ComparatorChallenges/BiholderTransport.lean:30 (same declaration text).
```
def metricVolume [BorelSpace M] (n : ℕ) : Measure M :=
…
```
def OAI.WeakMTWTransport.AdmissibleDensity line 34
Source documentation
Almost-everywhere measurable probability densities between fixed bounds.
Also declared: ComparatorChallenges/BiholderTransport.lean:34 (same declaration text).
```
def AdmissibleDensity (vol : Measure M) (lam cap : ℝ) (rho : M → ℝ) : Prop :=
…
```
def OAI.WeakMTWTransport.densityMeasure line 39
Source documentation
Multiplication by a density, ignoring exceptional negative values on null sets.
Also declared: ComparatorChallenges/BiholderTransport.lean:39 (same declaration text).
```
def densityMeasure (vol : Measure M) (rho : M → ℝ) : Measure M :=
…
```
def OAI.WeakMTWTransport.IsOptimalMap line 43
Source documentation
Optimality for the Monge minimization problem.
Also declared: ComparatorChallenges/BiholderTransport.lean:43 (same declaration text).
```
def IsOptimalMap (vol : Measure M) (rho0 rho1 : M → ℝ) (T : M → M) : Prop :=
…
```
def OAI.WeakMTWTransport.BiHolderEstimate line 51
Source documentation
The two global estimates have the very same exponent and constant.
Also declared: ComparatorChallenges/BiholderTransport.lean:51 (same declaration text).
```
def BiHolderEstimate (alpha C : ℝ) (T : M ≃ₜ M) : Prop :=
…
```
def OAI.WeakMTWTransport.IsGeodesicWithInitialData line 63
Source documentation
Complete affinely parametrized geodesic with prescribed initial tangent. Local metric minimization is an intrinsic definition of Riemannian geodesics.
Also declared: ComparatorChallenges/BiholderTransport.lean:65 (same declaration text).
```
def IsGeodesicWithInitialData (x : M) (v : TangentSpace 𝓘(ℝ, Model n) x)
    (gamma : ℝ → M) : Prop :=
…
```
Mentions: OAI.WeakMTWTransport.Model
def OAI.WeakMTWTransport.riemannianExp line 73
Source documentation
Evaluation at time one of the geodesic determined by initial data.
Also declared: ComparatorChallenges/BiholderTransport.lean:75 (same declaration text).
```
def riemannianExp (x : M) (v : TangentSpace 𝓘(ℝ, Model n) x) : M := by
…
```
Mentions: OAI.WeakMTWTransport.Model
def OAI.WeakMTWTransport.injectivityDomain line 78
Source documentation
The open injectivity domain, defined by extendible minimizing vectors.
Also declared: ComparatorChallenges/BiholderTransport.lean:80 (same declaration text).
```
def injectivityDomain (x : M) : Set (TangentSpace 𝓘(ℝ, Model n) x) :=
…
```
Mentions: OAI.WeakMTWTransport.Model
def OAI.WeakMTWTransport.mtw line 82
Source documentation
The Ma–Trudinger–Wang fourth derivative with factor -3/2.
Also declared: ComparatorChallenges/BiholderTransport.lean:84 (same declaration text).
```
def mtw (x : M) (p xi eta : TangentSpace 𝓘(ℝ, Model n) x) : ℝ :=
…
```
Mentions: OAI.WeakMTWTransport.Model
def OAI.WeakMTWTransport.WeakMTW line 89
Source documentation
Weak MTW only at interior velocities and only for orthogonal test vectors.
Also declared: ComparatorChallenges/BiholderTransport.lean:91 (same declaration text).
```
def WeakMTW : Prop :=
…
```