Descent.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ArnoldCounterexample.Descent.adaptive_step line 23

Source documentation

A second-derivative bound uniformly converts an infinitesimal descent -S into a strict smooth discrete descent using the step c*S. It works even when S vanishes to arbitrarily high order.

theorem adaptive_step {K : Set E} (hK : IsCompact K)
    (Φ : ℝ × E → ℝ) (hΦ : ContDiff ℝ ∞ Φ)
    (S : E → ℝ) (hS : Continuous S)
    (hSnon : ∀ z ∈ K, 0 ≤ S z)
    (hd0 : ∀ z ∈ K, fderiv ℝ Φ (0, z) (1, 0) = -S z) :
    ∃ c : ℝ, 0 < c ∧ ∀ z ∈ K,
      0 ≤ c * S z ∧ c * S z ≤ 1 ∧
      Φ (c * S z, z) ≤ Φ (0, z) ∧
      (S z ≠ 0 → Φ (c * S z, z) < Φ (0, z)) := by
…

lemma OAI.ArnoldCounterexample.Descent.iterate_le line 99
Source documentation
Values of a Lyapunov function are nonincreasing under iteration.
```
lemma iterate_le {D : X → X} {f : X → ℝ}
    (hdec : ∀ x, f (D x) ≤ f x) (n : ℕ) (x : X) : f (D^[n] x) ≤ f x := by
…
```

theorem OAI.ArnoldCounterexample.Descent.uniform_drop line 109

Source documentation

A compact band without stationary points is crossed in a uniform finite number of iterations. The conclusion is strict, as needed by the level-cover argument.

theorem uniform_drop {D : X → X} {f : X → ℝ}
    (hD : Continuous D) (hf : Continuous f)
    (hdec : ∀ x, f (D x) ≤ f x) (a b : ℝ)
    (hstrict : ∀ x, a ≤ f x → f x ≤ b → f (D x) < f x) :
    ∃ N : ℕ, ∀ x, f x ≤ b → f (D^[N] x) < a := by
…

theorem OAI.ArnoldCounterexample.Descent.thicken_sublevel line 148

Source documentation

Strict sublevel containment on the zero set of a continuous coordinate persists on a slightly larger closed sublevel.

theorem thicken_sublevel {f g : X → ℝ} {ℓ : X → ℂ}
    (hf : Continuous f) (hg : Continuous g) (hℓ : Continuous ℓ)
    (c a : ℝ) (h : ∀ x, f x ≤ c → ℓ x = 0 → g x < a) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ x, f x ≤ c + ε → ℓ x = 0 → g x < a := by
…

theorem OAI.ArnoldCounterexample.Descent.critical_level_cover line 171

Source documentation

The finite critical-value LS cover, expressed without manifold jargon. Every cover member is the inverse image of the same nonvanishing-coordinate chart under an iterate of a single strict Lyapunov descent.

theorem critical_level_cover {D : X → X} {f : X → ℝ} {ℓ : X → ℂ}
    (hD : Continuous D) (hf : Continuous f) (hℓ : Continuous ℓ)
    (hdec : ∀ x, f (D x) ≤ f x)
    (hchart : ∀ x, ℓ x = 0 → f (D x) < f x)
    (s : Finset ℝ) (a : ℝ)
    (hstationary : ∀ x, f x ≤ a → f (D x) = f x → f x ∈ s) :
    ∃ T : Finset ℕ, T.card ≤ s.card ∧
      ∀ x, f x ≤ a → ∃ n ∈ T, ℓ (D^[n] x) ≠ 0 := by
…