Model.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.CubicTorus.Cover line 11
Also declared: ComparatorChallenges/CubicTorus.lean:11 (same declaration text).
abbrev OAI.CubicTorus.Torus line 12
Also declared: ComparatorChallenges/CubicTorus.lean:12 (same declaration text).
def OAI.CubicTorus.quotientMap line 15
Source documentation
The quotient R³ → R³/Z³ in orthonormal coordinates.
Also declared: ComparatorChallenges/CubicTorus.lean:15 (same declaration text).
```
def quotientMap (x : Cover) : Torus :=
…
```
Mentions: OAI.CubicTorus.Cover, OAI.CubicTorus.Torus
def OAI.CubicTorus.fundamentalCube line 19
Source documentation
One unit-volume fundamental domain; its boundary is immaterial to integration.
Also declared: ComparatorChallenges/CubicTorus.lean:19 (same declaration text).
```
def fundamentalCube : Set Cover := {x | ∀ i, 0 ≤ x i ∧ x i < 1}
```
Mentions: OAI.CubicTorus.Cover
def OAI.CubicTorus.torusVolume line 22
Source documentation
The Riemannian volume measure of the unit flat torus.
Also declared: ComparatorChallenges/CubicTorus.lean:22 (same declaration text).
```
def torusVolume : Measure Torus :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.latticeVector line 26
Source documentation
An integer lattice vector in the Euclidean cover.
Also declared: ComparatorChallenges/CubicTorus.lean:26 (same declaration text).
```
def latticeVector (n : Fin 3 → ℤ) : Cover := WithLp.toLp 2 (fun i => (n i : ℝ))
```
Mentions: OAI.CubicTorus.Cover
def OAI.CubicTorus.AdmissibleField line 31
Source documentation
The smooth vector fields on the flat torus with pointwise length at most one, expressed as Z³-periodic fields on its Euclidean cover. The explicit ℕ∞ index is C^∞; top of WithTop ℕ∞ would instead mean analytic in this Mathlib.
Also declared: ComparatorChallenges/CubicTorus.lean:31 (same declaration text).
```
def AdmissibleField (F : Cover → Cover) : Prop :=
…
```
Mentions: OAI.CubicTorus.Cover
def OAI.CubicTorus.divergence line 37
Source documentation
Euclidean divergence in the orthonormal coordinate frame.
Also declared: ComparatorChallenges/CubicTorus.lean:37 (same declaration text).
```
def divergence (F : Cover → Cover) (x : Cover) : ℝ :=
…
```
Mentions: OAI.CubicTorus.Cover
def OAI.CubicTorus.perimeter line 41
Source documentation
De Giorgi perimeter, allowed to be infinite; no regularity of E is imposed.
Also declared: ComparatorChallenges/CubicTorus.lean:41 (same declaration text).
```
def perimeter (E : Set Torus) : ℝ≥0∞ :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.FinitePerimeter line 46
Source documentation
Finite-perimeter measurable regions, including all null-set modifications.
Also declared: ComparatorChallenges/CubicTorus.lean:46 (same declaration text).
```
def FinitePerimeter (E : Set Torus) : Prop :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.IsMinimizerAt line 50
Source documentation
A global perimeter minimizer under the prescribed volume constraint.
Also declared: ComparatorChallenges/CubicTorus.lean:50 (same declaration text).
```
def IsMinimizerAt (V : ℝ) (E : Set Torus) : Prop :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.candidateProfile line 56
Source documentation
The candidate unit-torus isoperimetric profile.
Also declared: ComparatorChallenges/CubicTorus.lean:56 (same declaration text).
```
def candidateProfile (V : ℝ) : ℝ :=
…
```
def OAI.CubicTorus.canonicalBall line 62
Source documentation
Canonical centered ball. Its radius on the listed branch is below 1/2.
Also declared: ComparatorChallenges/CubicTorus.lean:62 (same declaration text).
```
def canonicalBall (V : ℝ) : Set Torus :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.canonicalTube line 66
Source documentation
Canonical tube around the shortest closed geodesic in coordinate direction 0.
Also declared: ComparatorChallenges/CubicTorus.lean:66 (same declaration text).
```
def canonicalTube (V : ℝ) : Set Torus :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.canonicalSlab line 70
Source documentation
Canonical slab of width V between two parallel coordinate tori.
Also declared: ComparatorChallenges/CubicTorus.lean:70 (same declaration text).
```
def canonicalSlab (V : ℝ) : Set Torus := {x | ‖x 0‖ < V / 2}
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.CongruentAE line 73
Source documentation
Equality of regions up to ambient flat isometry and a null set.
Also declared: ComparatorChallenges/CubicTorus.lean:73 (same declaration text).
```
def CongruentAE (E F : Set Torus) : Prop :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.SmallStandardRegion line 77
Source documentation
Exactly the closed phase ranges, so adjacent types are BOTH included at ties.
Also declared: ComparatorChallenges/CubicTorus.lean:77 (same declaration text).
```
def SmallStandardRegion (V : ℝ) (E : Set Torus) : Prop :=
…
```
Mentions: OAI.CubicTorus.Torus
def OAI.CubicTorus.StandardRegionAt line 83
Source documentation
The equality class at every interior volume, including complementation.
Also declared: ComparatorChallenges/CubicTorus.lean:83 (same declaration text).
```
def StandardRegionAt (V : ℝ) (E : Set Torus) : Prop :=
…
```
Mentions: OAI.CubicTorus.Torus