ThreePoints.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ArnoldCounterexample.ThreePoints.R3 line 13
abbrev OAI.ArnoldCounterexample.ThreePoints.Pair line 14
def OAI.ArnoldCounterexample.ThreePoints.sqNorm line 16
def OAI.ArnoldCounterexample.ThreePoints.sphereProduct line 18
def OAI.ArnoldCounterexample.ThreePoints.pole line 20
def OAI.ArnoldCounterexample.ThreePoints.east line 21
def OAI.ArnoldCounterexample.ThreePoints.f line 24
Source documentation
A polynomial with three constrained critical points.
```
def f (q : Pair) : ℝ :=
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair
def OAI.ArnoldCounterexample.ThreePoints.MultiplierCritical line 28
Source documentation
The constrained critical equations of the polynomial.
```
def MultiplierCritical (q : Pair) : Prop :=
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair
def OAI.ArnoldCounterexample.ThreePoints.qzero line 33
def OAI.ArnoldCounterexample.ThreePoints.qplus line 34
def OAI.ArnoldCounterexample.ThreePoints.qminus line 35

lemma OAI.ArnoldCounterexample.ThreePoints.classify_coordinates line 39

Source documentation

Algebraic elimination of every solution, without a nondegeneracy assumption. We eliminate using μ instead of t=|x-p|; μ²=t², so the remaining factor is μ²=3.

lemma classify_coordinates
    {x₀ x₁ x₂ y₀ y₁ y₂ lam μ : ℝ}
    (hx : x₀^2 + x₁^2 + x₂^2 = 1)
    (hy : y₀^2 + y₁^2 + y₂^2 = 1)
    (h₀ : 1 + y₀ = lam * x₀) (h₁ : y₁ = lam * x₁) (h₂ : y₂ = lam * x₂)
    (g₀ : x₀ = μ * y₀) (g₁ : x₁ = μ * y₁) (g₂ : x₂ - 1 = μ * y₂) :
    (x₀ = 0 ∧ x₁ = 0 ∧ x₂ = 1 ∧ y₀ = -1 ∧ y₁ = 0 ∧ y₂ = 0) ∨
    (μ^2 = 3 ∧ x₀ = μ/2 ∧ x₁ = 0 ∧ x₂ = -1/2 ∧
      y₀ = 1/2 ∧ y₁ = 0 ∧ y₂ = -μ/2) := by
…

lemma OAI.ArnoldCounterexample.ThreePoints.qzero_critical line 96
lemma OAI.ArnoldCounterexample.ThreePoints.qplus_critical line 100
lemma OAI.ArnoldCounterexample.ThreePoints.qminus_critical line 105
theorem OAI.ArnoldCounterexample.ThreePoints.multiplierCritical_iff line 111
Source documentation
Exhaustiveness includes the isolated degenerate point.
```
theorem multiplierCritical_iff (q : Pair) :
    MultiplierCritical q ↔ q = qzero ∨ q = qplus ∨ q = qminus := by
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair, OAI.ArnoldCounterexample.ThreePoints.MultiplierCritical, OAI.ArnoldCounterexample.ThreePoints.qzero, OAI.ArnoldCounterexample.ThreePoints.qplus, OAI.ArnoldCounterexample.ThreePoints.qminus
lemma OAI.ArnoldCounterexample.ThreePoints.qzero_ne_qplus line 133
lemma OAI.ArnoldCounterexample.ThreePoints.qzero_ne_qminus line 138
lemma OAI.ArnoldCounterexample.ThreePoints.qplus_ne_qminus line 143
theorem OAI.ArnoldCounterexample.ThreePoints.multiplierCritical_set line 150
theorem OAI.ArnoldCounterexample.ThreePoints.multiplierCritical_encard line 157
Source documentation
A finite cardinality assertion, not ncard's default zero for infinite sets.
```
theorem multiplierCritical_encard : {q : Pair | MultiplierCritical q}.encard = 3 := by
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair, OAI.ArnoldCounterexample.ThreePoints.MultiplierCritical
lemma OAI.ArnoldCounterexample.ThreePoints.f_qzero line 163
lemma OAI.ArnoldCounterexample.ThreePoints.f_qplus line 164
lemma OAI.ArnoldCounterexample.ThreePoints.f_qminus line 165
theorem OAI.ArnoldCounterexample.ThreePoints.f_contDiff line 168
Source documentation
Smoothness of the actual ambient polynomial, so its restriction is smooth.
```
theorem f_contDiff : ContDiff ℝ ∞ f := by unfold f; fun_prop
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.f
lemma OAI.ArnoldCounterexample.ThreePoints.dot_self line 172
lemma OAI.ArnoldCounterexample.ThreePoints.annihilator_sphere line 178
Source documentation
The elementary tangent-annihilator lemma supplies (rather than assumes) the Lagrange multipliers.
```
lemma annihilator_sphere {x a : R3} (hx : sqNorm x = 1) :
    (∀ u : R3, x ⬝ᵥ u = 0 → a ⬝ᵥ u = 0) ↔ ∃ lam : ℝ, a = lam • x := by
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.R3, OAI.ArnoldCounterexample.ThreePoints.sqNorm
def OAI.ArnoldCounterexample.ThreePoints.firstCoord line 196
def OAI.ArnoldCounterexample.ThreePoints.secondCoord line 199
def OAI.ArnoldCounterexample.ThreePoints.df line 203
Source documentation
The ambient differential of the polynomial.
```
def df (q : Pair) : Pair →L[ℝ] ℝ :=
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair
lemma OAI.ArnoldCounterexample.ThreePoints.df_apply line 207
lemma OAI.ArnoldCounterexample.ThreePoints.f_hasFDerivAt line 212
def OAI.ArnoldCounterexample.ThreePoints.TangentCritical line 226
Source documentation
dh vanishes on the full constrained tangent of S² × S².
```
def TangentCritical (q : Pair) : Prop :=
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair
lemma OAI.ArnoldCounterexample.ThreePoints.tangentCritical_iff_multiplierCritical line 230
theorem OAI.ArnoldCounterexample.ThreePoints.tangentCritical_iff line 263
Source documentation
The complete critical-point calculation in constrained tangent form.
```
theorem tangentCritical_iff (q : Pair) :
    TangentCritical q ↔ q = qzero ∨ q = qplus ∨ q = qminus := by
…
```
Mentions: OAI.ArnoldCounterexample.ThreePoints.Pair, OAI.ArnoldCounterexample.ThreePoints.TangentCritical, OAI.ArnoldCounterexample.ThreePoints.qzero, OAI.ArnoldCounterexample.ThreePoints.qplus, OAI.ArnoldCounterexample.ThreePoints.qminus
theorem OAI.ArnoldCounterexample.ThreePoints.tangentCritical_encard line 267