OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample
OpenThe theorem states that the defined proposition MainTarget holds, i.e. that there exist a smooth Riemannian metric g on the 5-manifold S⁴ × S¹ (the unit sphere in ℝ⁵ times the circle, modelled on ℝ⁴ × ℝ¹), a sequence of positive reals λₖ, and a sequence of smooth real functions uₖ on this manifold, each not identically zero, such that the following hold. At every point x, in the extended chart at x, the coordinate Laplacian of uₖ, namely (1/√det G) Σᵢ ∂ᵢ(√det G Σⱼ Gⁱʲ ∂ⱼ(uₖ∘chart⁻¹)), where G is the matrix of g in the chart's coordinate frame and Gⁱʲ its inverse, satisfies −Δ_g uₖ(x) = λₖ uₖ(x), so each uₖ is a Laplace eigenfunction with eigenvalue λₖ. Moreover λₖ → ∞, and the 4-dimensional Hausdorff measure (taken with respect to the distance induced by g) of the nodal set {uₖ = 0}, divided by √λₖ, tends to +∞ as k → ∞. Thus the nodal-set size grows faster than the order √λₖ, which is a counterexample to a Yau-type upper bound on nodal sets in this setting. The theorem is admitted in the source and not proved there.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/YauCounterexample.lean; bytes 2634..2709 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_YauCounterexample namespace OAI namespace Yau namespace Target open Bundle Manifold Matrix Filter open scoped ContDiff Topology ENNReal noncomputable section
theorem yau_nodal_set_upper_bound_counterexample : MainTarget := by sorry end end Target end Yau end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.