Skip to content

mathlib_issue_schaefer.md

Latest commit

 

History

History
75 lines (56 loc) · 2.68 KB

mathlib_issue_schaefer.md

File metadata and controls

75 lines (56 loc) · 2.68 KB

Feature Request: Schaefer's Fixed-Point Theorem

Mathematical Statement

Schaefer's Fixed-Point Theorem (Schaefer 1955; Deimling 1985, Thm 9.2):

Let E be a Banach space and T : E → E continuous, mapping bounded sets to relatively compact sets. If the Schaefer set S = {x ∈ E | ∃ τ ∈ [0,1], x = τ T(x)} is bounded, then T has a fixed point.

Current Mathlib State

  • IsCompactOperator for linear maps (Mathlib.Analysis.Normed.Operator.Compact)
  • Banach space infrastructure (Mathlib.Analysis.NormedSpace.Basic)
  • Sperner's lemma (#25231) on the Brouwer path
  • No Schaefer, Leray-Schauder, or Schauder fixed-point theorems

API Design Question

Schaefer applies to nonlinear operators. The compactness condition is that T maps bounded sets to relatively compact sets. Possible approaches (seeking guidance):

  1. IsCompactMap T — ∀ S, Bornology.IsBounded S → IsCompact (closure (T '' S)). Extends the concept to nonlinear maps.
  2. Continuous with relatively compact image — weaker, avoids the design question.
  3. Linear version first — slots into IsCompactOperator, doesn't cover the nonlinear PDE use case.

Proof Strategy

Standard route via truncation:

  1. Define Tₙ(x) = T(x) / max(1, ‖T(x)‖/n)
  2. Tₙ maps the ball of radius n to itself, is continuous, image relatively compact
  3. Schauder's theorem → Tₙ has fixed point xₙ
  4. Boundedness of S gives uniform bound → for large n, xₙ = T(xₙ)

Dependency chain: Brouwer (Sperner #25231) → Schauder → Schaefer

Downstream Use Case

We formalize existence theory for a nonlinear elliptic BVP on compact Riemannian manifolds (cd-formalization). The proof chain is verified in Lean 4 against Mathlib v4.28.0 except the Schaefer step, which is axiomatized in a PDEInfra typeclass:

schaefer :
  True →  -- placeholder for T continuous & compact
  (∃ K > 0, ∀ (u : M → ℝ) (τ : ℝ),
    0 ≤ τ → τ ≤ 1 →
    (∀ x, u x = τ * solOp.T u x) →
    ∀ x, |u x| ≤ K) →
  ∃ Φ : M → ℝ, solOp.T Φ = Φ

The project has zero sorry, zero sorryAx, CI with --wfail, and 11 axiom-checked theorems. Having Schaefer in Mathlib would replace this axiom with a real proof.

AI disclosure: Parts of the formalization use Claude (Anthropic) and Aristotle (theorem prover). All code is manually reviewed.

References

  • H. Schaefer, "Über die Methode der a priori-Schranken," Math. Ann. 129 (1955), 415–416.
  • K. Deimling, Nonlinear Functional Analysis, Springer, 1985, Thm 9.2.
  • L.C. Evans, Partial Differential Equations, 2nd ed., AMS, 2010, §9.2.2.