Mountain Pass Theorem (Ambrosetti–Rabinowitz 1973)

mountain_pass

Submitter: Kim Morrison.

Notes: A C¹ functional f on a real Banach space E satisfying the Palais–Smale condition and having mountain-range geometry separating two points a, b — `f(a) = 0`, `f ≥ ε > 0` on the sphere S_r(a), `r < ‖b − a‖`, and `f(b) ≤ 0` — admits a critical point at the mini-max level `c = inf_γ sup_t f(γ t)` (over all continuous paths γ from a to b), with `c ≥ ε`. The faithful encoding fixes Knill's slip `|b| > ε` (the sphere has radius r, not ε) to the standard `r < ‖b − a‖`. The mini-max level is encoded as `⨅ γ : Path a b, ⨆ t : I, f (γ t)`. The theorem is listed as §119 in Knill's *Some Fundamental Theorems in Mathematics*.

Source: A. Ambrosetti and P.H. Rabinowitz, 'Dual variational methods in critical point theory and applications', J. Funct. Anal. 14 (1973) 349–381. Listed as §119 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The classical proof is by **contradiction via the deformation lemma / pseudo-gradient flow**. Suppose the mini-max level c has no critical point at value c. The (locally Lipschitz) pseudo-gradient field W on `{x : f'(x) ≠ 0}` satisfies `‖W(x)‖ ≤ 2 ‖f'(x)‖` and `⟨f'(x), W(x)⟩ ≥ ‖f'(x)‖²`. By Palais–Smale, `‖f'(x)‖` is bounded away from 0 on the sublevel `{f ≤ c + δ} \ {f ≤ c − δ}` for δ small enough. Integrating the pseudo-gradient flow `dη/dt = −W(η)` for time T moves the sublevel `{f ≤ c + δ}` into `{f ≤ c − δ}` (the deformation lemma). Choose a path γ with sup_t f(γ t) ≤ c + δ, using the definition of c as an infimum; the deformation produces a new path with sup ≤ c − δ, contradicting the same definition. Therefore some critical point lies at value c. The mountain-range hypothesis forces `c ≥ ε` because every path from a to b must cross the sphere S_r(a), where `f ≥ ε`. Mathlib has the C¹/Fréchet calculus, `Path` between two endpoints, Banach spaces, and conditionally-complete-lattice infimum, but no Palais–Smale condition, no pseudo-gradient field, no deformation lemma, no mini-max critical-value framework.

theorem declaration uses `sorry`mountain_pass (f : E → ℝ) (_hf : ContDiff ℝ 1 f) (_hps : LeanEval.Analysis.MountainPassProblem.PalaisSmale f)
    {a b : E} {ε r : ℝ} (_hmr : LeanEval.Analysis.MountainPassProblem.MountainRange f a b ε r) :
    ∃ x : E, LeanEval.Analysis.MountainPassProblem.IsCriticalPoint f x ∧
      f x = mountainPassLevel f a b ∧ ε ≤ mountainPassLevel f a b := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace Ef:E → ℝ_hf:ContDiff ℝ 1 f_hps:PalaisSmale fa:Eb:Eε:ℝr:ℝ_hmr:MountainRange f a b ε r⊢ ∃ x, IsCriticalPoint f x ∧ f x = mountainPassLevel f a b ∧ ε ≤ mountainPassLevel f a b
  sorryAll goals completed! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 5, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jun 5, 2026