Hessian estimates for the sigma-2 equation in dimension four
Loading leaderboard data…
Problem statement
Notes: The proof binders `smooth`, `bounded`, `positive_branch`, and `solution` are prefixed with `_` here. This is alpha-equivalent and suppresses unused-variable warnings in the generated `Solution.lean` delegation.
Source: R. Shankar and Y. Yuan, `Hessian estimates for the sigma-2 equation in dimension four`, Annals of Math, 201 (2) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-201-2-HessianEstimates.lean
Informal solution: Unavailable.
theorem declaration uses `sorry`theorem_1_1 : ∃ C : ℝ≥0∞ → ℝ, ∀ (u : ℝ⁴ → ℝ)
(_smooth : ContDiffOn ℝ ∞ u B₁(0))
(_bounded : ‖u‖_C¹(B₁(0)) < (∞ : ℝ≥0∞))
(_positive_branch : ∀ x ∈ B₁(0), (Δ u) x > 0)
(_solution : ∀ x ∈ B₁(0), σ₂ (H u B₁(0) x) = 1),
‖H u B₁(0) 0‖_F ≤ C (‖u‖_C¹(B₁(0))) := ⊢ ∃ C,
∀ (u : ℝ⁴ → ℝ),
ContDiffOn ℝ ∞ u B₁(0) →
‖u‖_C¹(B₁(0)) < ∞ →
(∀ x ∈ B₁(0), Δ u x > 0) → (∀ x ∈ B₁(0), σ₂ (H u B₁(0) x) = 1) → ‖H u B₁(0) 0‖_F ≤ C ‖u‖_C¹(B₁(0))
All goals completed! 🐙