Model.lean`

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ArnoldCounterexample.CV line 10
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:10 (same declaration text).
def OAI.ArnoldCounterexample.quadricPolynomial line 12
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:12 (same declaration text).
def OAI.ArnoldCounterexample.normSquared line 14
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:14 (same declaration text).
def OAI.ArnoldCounterexample.IsUnitQuadric line 16
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:16 (same declaration text).
abbrev OAI.ArnoldCounterexample.UnitQuadric line 19
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:19 (same declaration text).
lemma OAI.ArnoldCounterexample.unitQuadric_ne_zero line 21
def OAI.ArnoldCounterexample.Q3 line 27
Source documentation
The literal projective quadric sum z_j^2 = 0 in CP^4.
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:22 (same declaration text).
```
def Q3 := {q : Projectivization ℂ CV //
…
```
Mentions: OAI.ArnoldCounterexample.CV
def OAI.ArnoldCounterexample.project line 31
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:26 (same declaration text).
def OAI.ArnoldCounterexample.Horizontal line 39
Source documentation
Horizontal lifts of the real tangent of Q3 at [z].
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:34 (same declaration text).
```
def Horizontal (z v : CV) : Prop :=
…
```
Mentions: OAI.ArnoldCounterexample.CV
def OAI.ArnoldCounterexample.omega line 43
Source documentation
The restricted Fubini--Study form, evaluated on horizontal lifts.
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:38 (same declaration text).
```
def omega (v w : CV) : ℝ := 2 * (∑ j, star (v j) * w j).im
```
Mentions: OAI.ArnoldCounterexample.CV
def OAI.ArnoldCounterexample.LocalFunctionLift line 46
Source documentation
A local smooth extension of the pullback of h to the unit isotropic cone.
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:41 (same declaration text).
```
def LocalFunctionLift (h : Q3 → ℝ) (z : UnitQuadric)
    (U : Set CV) (g : CV → ℝ) : Prop :=
…
```
Mentions: OAI.ArnoldCounterexample.Q3, OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.CV
def OAI.ArnoldCounterexample.IsSmoothFunction line 51
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:46 (same declaration text).
structure OAI.ArnoldCounterexample.SmoothFunction line 54
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:49 (same declaration text).
def OAI.ArnoldCounterexample.IsCritical line 59
Source documentation
dh_q = 0, expressed using all local lifts, independent of normal extensions.
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:54 (same declaration text).
```
def IsCritical (h : Q3 → ℝ) (q : Q3) : Prop :=
…
```
Mentions: OAI.ArnoldCounterexample.Q3
def OAI.ArnoldCounterexample.criticalSet line 64
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:59 (same declaration text).
def OAI.ArnoldCounterexample.criticalNumber line 67
Source documentation
The minimum critical number, including degenerate functions (ENat allows infinity).
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:62 (same declaration text).
```
def criticalNumber : ℕ∞ := ⨅ h : SmoothFunction, (criticalSet h).encard
```
Mentions: OAI.ArnoldCounterexample.SmoothFunction, OAI.ArnoldCounterexample.criticalSet
structure OAI.ArnoldCounterexample.HamiltonianPath line 71
Source documentation
An explicit smooth lift of a Hamiltonian isotopy, with inverse and generator. The Hamiltonian equation uses i_X omega = dH.
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:66 (same declaration text).
```
structure HamiltonianPath (φ : Q3 ≃ Q3) where
…
```
Mentions: OAI.ArnoldCounterexample.Q3
def OAI.ArnoldCounterexample.IsHamiltonian line 100
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:95 (same declaration text).
def OAI.ArnoldCounterexample.fixedSet line 102
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:97 (same declaration text).
def OAI.ArnoldCounterexample.HasDegenerateFixedPoint line 106
Source documentation
Eigenvalue 1 in the derivative on the quotient tangent, not an ambient spurious vertical eigenvector. v is nonzero and horizontal.
Also declared: ComparatorChallenges/ArnoldCounterexample.lean:101 (same declaration text).
```
def HasDegenerateFixedPoint (φ : Q3 ≃ Q3) : Prop :=
…
```
Mentions: OAI.ArnoldCounterexample.Q3