fix: require boundedness for Lebesgue=Jordan-inner equalities

[Chessing234]

Summary

• Add (hbound : Bornology.IsBounded E) to Lebesgue_outer_measure.eq_Jordan_inner_of_boxes and Lebesgue_outer_measure.of_open.
• Thread hbound into the local call of eq_Jordan_inner_of_boxes inside of_open. Leave sorry bodies unchanged.

Why

Lebesgue_outer_measure is EReal (can be ⊤). Jordan_inner_measure is ℝ, defined as an sSup of elementary measures; for sets unbounded above that collection is unbounded in ℝ, and the junk sSup is 0.

So for an unbounded almost-disjoint union of unit cubes (or Set.univ in d ≥ 1), the claimed equality is false: LHS ⊤, RHS 0 via coercion. The book allows +∞ Jordan inner measure; the ℝ encoding here does not, so the statements need a boundedness hypothesis.

[teorth]

Thanks — you found a real problem, and the diagnosis is right: both statements are false as they stand. Jordan_inner_measure is ℝ-valued (sSup over a set of reals) while Lebesgue_outer_measure is EReal, so for an unbounded open set such as Set.univ in d ≥ 1 the left side is ⊤ and the right side is a supremum over a set with no upper bound, i.e. Mathlib's junk value 0. So of_open as written is refuted by E = univ.

Where I'd push back is on the direction of the fix. The book states Exercise 1.2.5 as:

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.

That last clause is deliberate — the unbounded case is exactly what the exercise asks for, and it is what makes the subsequent formula for the outer measure of an arbitrary open set work. Adding Bornology.IsBounded E makes the Lean compile, but it drops the generality the text explicitly calls out, and it propagates: Lebesgue_outer_measure.of_open becomes a statement about bounded open sets only, which is weaker than Lemma 1.2.10 in the book.

So I have gone the other way and supplied the extension the text asks for, in #685:

• Jordan_inner_measure', the same supremum taken in EReal;
• Jordan_inner_measure'_eq_coe, showing it agrees with Jordan_inner_measure on bounded sets, so it really is an extension of Definition 1.1.4;
• Jordan_inner_measure'_univ, showing it is ⊤ on the whole space for d ≥ 1 — your counterexample, recorded as a theorem.

Exercise 1.2.5 and of_open are restated with Jordan_inner_measure'; the exercise keeps its sorry, and of_open keeps its proof with the two bounded branches routed through the agreement lemma.

Closing this in favour of that PR — but the bug report is what prompted it, so thank you for it. The EReal junk-value trap is worth keeping in mind elsewhere in these files: it will bite anywhere a real-valued sSup/sInf meets an EReal-valued measure.