Riesz's rising sun lemma

rising_sun_lemma — a formalization challenge from the lean-eval benchmark.

Notes

Every continuous real function on a compact interval has the rising-sun property: the shadow set is open, empty iff the function is antitone, else a disjoint union of open intervals with f(c_n) ≤ f(d_n). Trusted helpers (risingSunSet, HasRisingSunDecomposition, HasRisingSunProperty) are non-holes. Mathlib has the monotone-a.e.-differentiable consequence but not the rising-sun lemma. Candidate from §163 of the Knill survey.

Formal statement

/-- **Riesz's rising sun lemma.** Every continuous real function on a compact
interval has the rising-sun property. -/
theorem rising_sun_lemma {a b : ℝ} (hab : a < b) {f : ℝ → ℝ}
    (hf : ContinuousOn f (Icc a b)) :
    HasRisingSunProperty a b f := by
  sorry

Source

F. Riesz (1932). Knill, §163.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: rising_sun_lemma
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.