fix: extended-real Jordan inner measure for Exercise 1.2.5

[teorth]

Fixes the defect reported in #679, in the direction the text calls for.

The problem

Lebesgue_outer_measure.of_open and Exercise 1.2.5 (Lebesgue_outer_measure.eq_Jordan_inner_of_boxes) were false as stated. Jordan_inner_measure is ℝ-valued — a sSup over a set of reals — while Lebesgue_outer_measure is EReal-valued. For an unbounded open set such as Set.univ in d ≥ 1, the left side is ⊤ while the right side is a supremum over a set with no upper bound, which Mathlib evaluates to the junk value 0.

Why not just add a boundedness hypothesis

That was the fix proposed in #679, and it compiles, but it contradicts the text. Exercise 1.2.5 reads:

Show that if a set $E \subset \R^d$ is expressible as the countable union of almost disjoint boxes, then the Lebesgue outer measure of $E$ is equal to the Jordan inner measure: $m^(E) = m_{,(J)}(E)$, where we extend the definition of Jordan inner measure to unbounded sets in the obvious manner.

The unbounded case is exactly what the exercise is asking for, and it is what makes the subsequent formula for the outer measure of an arbitrary open set work. Restricting to bounded sets would also weaken of_open below Lemma 1.2.10.

What this does instead

Supplies the extension the text asks for:

• Jordan_inner_measure' — the same supremum, taken in EReal.
• Jordan_inner_measure'_eq_coe — it agrees with Jordan_inner_measure on bounded sets, so it is genuinely an extension of Definition 1.1.4 rather than a different notion.
• Jordan_inner_measure'_univ — it is ⊤ on the whole space when d ≥ 1. This is the counterexample that refutes the old statements, recorded as a theorem rather than left as a remark.

Supporting API: Jordan_inner_nonempty, Jordan_inner_bddAbove, Jordan_inner_measure'_set_eq, EReal.sSup_image_coe (the real and EReal suprema agree for a nonempty set bounded above), and EuclideanSpace'.isBounded_of_dim_zero.

Exercise 1.2.5 and of_open are then restated with Jordan_inner_measure'. The exercise keeps its sorry. of_open keeps its existing proof: its two bounded branches — dimension zero, and the empty set — are routed through Jordan_inner_measure'_eq_coe, and the main branch is unchanged since it just applies the exercise.

The real-valued Jordan_inner_measure is untouched, so JordanMeasurable and everything built on it are unaffected.

lake build passes locally: 8310 jobs, no errors, no new warnings.

Closes #679.

🤖 Generated with Claude Code