Analysis I, Section 11.7: A non-Riemann integrable function

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• An example of a bounded function on a compact interval that is not Riemann integrable.

theorem Chapter11.not_integrable : Chapter9.BddOn Chapter9.f_9_3_21 ↑(BoundedInterval.Icc 0 1) ∧ ¬IntegrableOn Chapter9.f_9_3_21 (BoundedInterval.Icc 0 1)

Proposition 11.7.1