A solvable Hamburger moment problem has a unique solution or infinitely many
ProvedHamburgerMoment.unique_or_infinite_solutionshankel-matrixmoment-problem
Let be a moment sequence, i.e. its Hamburger moment problem has at least one solution. Then at least one of the following holds:
- the problem has a unique solution ;
- the set of solutions is infinite.
Formalization Note The statement is the disjunction "unique solution or infinitely many solutions"; the two alternatives are automatically exclusive.
Preamble
import Mathlib import Definitions.Def_HamburgerMoment_Defs open MeasureTheory
Formal statement
namespace HamburgerMoment
theorem unique_or_infinite_solutions (m : ℕ → ℝ) (hm : IsMomentSequence m) :
(∃! μ : Measure ℝ, IsMomentMeasure m μ) ∨ {μ : Measure ℝ | IsMomentMeasure m μ}.Infinite := by sorry
end HamburgerMomentSource
Wikipedia, "Hamburger moment problem", revision oldid=1356180072, https://en.wikipedia.org/w/index.php?title=Hamburger_moment_problem&oldid=1356180072, section "Uniqueness of solutions", first sentence
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.