structure TaggedPartition (I : BoundedInterval) (n : ℕ) : Type

Definition 1.1.5. (Riemann integrability) The interval I should be closed, though we will not enforce this. We also permit the length to be 0. We index the tags and deltas starting from 0 rather than 1 in the text as this is slightly more convenient in Lean.

• x : Fin (n + 1) → ℝ
• x_tag : Fin n → ℝ
• x_start : self.x 0 = I.a
• x_end : self.x (Fin.last n) = I.b
• x_mono : StrictMono self.x
• x_tag_between (i : Fin n) : self.x i.castSucc ≤ self.x_tag i ∧ self.x_tag i ≤ self.x i.succ

theorem TaggedPartition.ext_iff {I : BoundedInterval} {n : ℕ} {x y : TaggedPartition I n} : x = y ↔ x.x = y.x ∧ x.x_tag = y.x_tag

theorem TaggedPartition.ext {I : BoundedInterval} {n : ℕ} {x y : TaggedPartition I n} : x.x = y.x → ∀ (x_tag : x.x_tag = y.x_tag), x = y

def TaggedPartition.delta {I : BoundedInterval} {n : ℕ} (P : TaggedPartition I n) (i : Fin n) : ℝ

Equations

• P.delta i = P.x i.succ - P.x i.castSucc

noncomputable def TaggedPartition.norm {I : BoundedInterval} {n : ℕ} (P : TaggedPartition I n) : ℝ

Equations

• P.norm = iSup P.delta

def TaggedPartition.RiemannSum {I : BoundedInterval} {n : ℕ} (f : ℝ → ℝ) (P : TaggedPartition I n) : ℝ

Equations

• TaggedPartition.RiemannSum f P = ∑ i : Fin n, f (P.x_tag i) * P.delta i

noncomputable def TaggedPartition.nhds_zero (I : BoundedInterval) : Filter (Sigma (TaggedPartition I))

Sigma (TaggedPartition I) is the type of all partitions of I with an unspecified number n of components. Here we define what it means to converge to zero in this type.

Equations

• TaggedPartition.nhds_zero I = Filter.comap (fun (P : Sigma (TaggedPartition I)) => P.snd.norm) (nhds 0)

def riemann_integral_eq (f : ℝ → ℝ) (I : BoundedInterval) (R : ℝ) : Prop

Equations

• riemann_integral_eq f I R = Filter.Tendsto (fun (P : Sigma (TaggedPartition I)) => TaggedPartition.RiemannSum f P.snd) (TaggedPartition.nhds_zero I) (nhds R)

noncomputable def TaggedPartition.uniform (I : BoundedInterval) (n : ℕ) (hn : n > 0) : I = BoundedInterval.Icc I.a I.b → (hab : I.a < I.b) → TaggedPartition I n

Construct a uniform partition of [a,b] into n equal pieces with left endpoint tags.

Equations

• One or more equations did not get rendered due to their size.

theorem TaggedPartition.uniform_norm (I : BoundedInterval) (n : ℕ) (hn : n > 0) (hI : I = BoundedInterval.Icc I.a I.b) (hab : I.a < I.b) : (uniform I n hn hI hab).norm = (I.b - I.a) / ↑n

The norm of a uniform partition is (b-a)/n.

theorem TaggedPartition.exists_norm_le (I : BoundedInterval) (hI : I = BoundedInterval.Icc I.a I.b) (hab : I.a < I.b) (δ : ℝ) (hδ : 0 < δ) : ∃ (n : ℕ) (P : TaggedPartition I n), P.norm ≤ δ

For any positive interval and δ > 0, there exists a tagged partition with norm ≤ δ.

instance TaggedPartition.nhds_zero_neBot (I : BoundedInterval) (hI : I = BoundedInterval.Icc I.a I.b) (hab : I.a < I.b) : (nhds_zero I).NeBot

The filter TaggedPartition.nhds_zero is non-trivial when the interval has positive length.

@[reducible, inline]

abbrev RiemannIntegrableOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

We enforce I to be closed and nonempty for the definition of Riemann integrability. The nonempty constraint ensures meaningful integration and excludes degenerate cases.

Equations

• RiemannIntegrableOn f I = (I = BoundedInterval.Icc I.a I.b ∧ (↑I).Nonempty ∧ ∃ (R : ℝ), riemann_integral_eq f I R)

noncomputable def riemannIntegral (f : ℝ → ℝ) (I : BoundedInterval) : ℝ

Equations

• riemannIntegral f I = if h : RiemannIntegrableOn f I then ⋯.choose else 0

theorem riemann_sum_eq_zero_of_zero_length {f : ℝ → ℝ} {I : BoundedInterval} (h_len : I.length = 0) {n : ℕ} (P : TaggedPartition I n) : TaggedPartition.RiemannSum f P = 0

When an interval has zero length, all Riemann sums equal zero.

theorem riemann_integral_eq_zero_of_zero_length {f : ℝ → ℝ} {I : BoundedInterval} {R : ℝ} (h_eq : I.a = I.b) (h_len : I.length = 0) (hR : riemann_integral_eq f I R) : R = 0

When an interval has zero length and Riemann sums converge to R, then R = 0. This requires that the filter is non-trivial (Filter.NeBot), which holds when I.a = I.b.

theorem eq_of_length_zero_of_Icc {I : BoundedInterval} (hI : I = BoundedInterval.Icc I.a I.b) (h_len : I.length = 0) (h_nonempty : (↑I).Nonempty) : I.a = I.b

When a nonempty closed interval [a,b] has zero length, then a = b.

theorem riemann_integral_of_integrable {f : ℝ → ℝ} {I : BoundedInterval} (h : RiemannIntegrableOn f I) : riemann_integral_eq f I (riemannIntegral f I)

Definition 1.1.15 (Riemann integrability, Riemann sums converge)

theorem riemann_integral_eq_iff_of_integrable {f : ℝ → ℝ} {I : BoundedInterval} (h : RiemannIntegrableOn f I) (R : ℝ) : riemann_integral_eq f I R ↔ R = riemannIntegral f I

Definition 1.1.15 (Riemann integrability, characterization)

theorem riemann_integral_eq_iff {f : ℝ → ℝ} {I : BoundedInterval} (R : ℝ) : riemann_integral_eq f I R ↔ ∀ ε > 0, ∃ δ > 0, ∀ (n : ℕ) (P : TaggedPartition I n), P.norm ≤ δ → |TaggedPartition.RiemannSum f P - R| ≤ ε

Definition 1.1.15 (Riemann integrability).

theorem RiemannIntegrable.of_zero_length (f : ℝ → ℝ) {I : BoundedInterval} {a : ℝ} (h : I = BoundedInterval.Icc a a) : RiemannIntegrableOn f I ∧ riemannIntegral f I = 0

Definition 1.1.15. (Riemann integrability)

def TaggedPartition.changeTag {I : BoundedInterval} {n : ℕ} (P : TaggedPartition I n) (k : Fin n) (t : ℝ) (ht : P.x k.castSucc ≤ t ∧ t ≤ P.x k.succ) : TaggedPartition I n

Helper: Modify a tagged partition by changing one tag

Equations

• P.changeTag k t ht = { x := P.x, x_tag := Function.update P.x_tag k t, x_start := ⋯, x_end := ⋯, x_mono := ⋯, x_tag_between := ⋯ }

theorem TaggedPartition.RiemannSum_changeTag_sub {I : BoundedInterval} {n : ℕ} (P : TaggedPartition I n) (f : ℝ → ℝ) (k : Fin n) (t : ℝ) (ht : P.x k.castSucc ≤ t ∧ t ≤ P.x k.succ) : RiemannSum f (P.changeTag k t ht) - RiemannSum f P = (f t - f (P.x_tag k)) * P.delta k

The Riemann sum difference when changing one tag

theorem TaggedPartition.uniform_delta {I : BoundedInterval} {n : ℕ} (hn : n > 0) (hI : I = BoundedInterval.Icc I.a I.b) (hab : I.a < I.b) (i : Fin n) : (uniform I n hn hI hab).delta i = (I.b - I.a) / ↑n

For a uniform partition, delta is constant

noncomputable def findSubintervalIndex (lo hi : ℝ) (n : ℕ) (hn : n > 0) (x : ℝ) (_hx : lo ≤ x ∧ x ≤ hi) : Fin n

For any x in [a,b], find the subinterval index containing x

Equations

• findSubintervalIndex lo hi n hn x _hx = ⟨min ⌊(x - lo) / ((hi - lo) / ↑n)⌋₊ (n - 1), ⋯⟩

theorem findSubintervalIndex_spec (lo hi : ℝ) (n : ℕ) (hn : n > 0) (hlohi : lo < hi) (x : ℝ) (hx : lo ≤ x ∧ x ≤ hi) : have k := findSubintervalIndex lo hi n hn x hx; have Δ := (hi - lo) / ↑n; lo + ↑↑k * Δ ≤ x ∧ x ≤ lo + (↑↑k + 1) * Δ

The found index correctly brackets x

theorem RiemannIntegrable.bounded {f : ℝ → ℝ} {I : BoundedInterval} (h : RiemannIntegrableOn f I) : ∃ (M : ℝ), ∀ x ∈ I, |f x| ≤ M

Definition 1.1.15

structure PiecewiseConstantFunction (I : BoundedInterval) : Type

• f : ℝ → ℝ
• T : Finset BoundedInterval
• c : ↥self.T → ℝ
• disjoint : (↑self.T).PairwiseDisjoint BoundedInterval.toSet
• cover : ↑I = ⋃ J ∈ self.T, ↑J
• const (J : ↥self.T) (x : ℝ) : x ∈ ↑J → self.f x = self.c J

theorem PiecewiseConstantFunction.ext_iff {I : BoundedInterval} {x y : PiecewiseConstantFunction I} : x = y ↔ x.f = y.f ∧ x.T = y.T ∧ x.c ≍ y.c

theorem PiecewiseConstantFunction.ext {I : BoundedInterval} {x y : PiecewiseConstantFunction I} (f : x.f = y.f) (T : x.T = y.T) (c : x.c ≍ y.c) : x = y

@[reducible, inline]

abbrev PiecewiseConstantFunction.agreesWith {I : BoundedInterval} (F : PiecewiseConstantFunction I) (f : ℝ → ℝ) : Prop

Equations

• F.agreesWith f = Set.EqOn f F.f ↑I

def PiecewiseConstantOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

Equations

• PiecewiseConstantOn f I = ∃ (F : PiecewiseConstantFunction I), F.agreesWith f

def PiecewiseConstantFunction.integral {I : BoundedInterval} (g : PiecewiseConstantFunction I) : ℝ

Equations

• g.integral = ∑ J : ↥g.T, g.c J * (↑J).length

theorem PiecewiseConstantFunction.integral_eq (f : ℝ → ℝ) {I : BoundedInterval} (F F' : PiecewiseConstantFunction I) (hF : F.agreesWith f) (hF' : F'.agreesWith f) : F.integral = F'.integral

Exercise 1.1.20 (Piecewise constant functions, integral well-defined)

noncomputable def PiecewiseConstantOn.integral (f : ℝ → ℝ) {I : BoundedInterval} (h : PiecewiseConstantOn f I) : ℝ

Equations

• PiecewiseConstantOn.integral f h = (Exists.choose h).integral

theorem PiecewiseConstantOn.integral_eq (f : ℝ → ℝ) {I : BoundedInterval} (h : PiecewiseConstantOn f I) (F : PiecewiseConstantFunction I) (hF : F.agreesWith f) : integral f h = F.integral

Exercise 1.1.20 (Piecewise constant functions, integral of a representation)

theorem PiecewiseConstantOn.smul {I : BoundedInterval} (c : ℝ) {f : ℝ → ℝ} (h : PiecewiseConstantOn f I) : PiecewiseConstantOn (c • f) I

Exercise 1.1.21 (a) (Linearity, scalar multiple is piecewise constant)

theorem PiecewiseConstantFunction.integral_smul {I : BoundedInterval} (c : ℝ) {f : ℝ → ℝ} (h : PiecewiseConstantOn f I) : PiecewiseConstantOn.integral (c • f) ⋯ = c • PiecewiseConstantOn.integral f h

Exercise 1.1.21 (a) (Linearity, integral of a scalar multiple)

theorem PiecewiseConstantOn.add {I : BoundedInterval} {f g : ℝ → ℝ} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn (f + g) I

Exercise 1.1.21 (a) (Linearity, sum is piecewise constant)

theorem PiecewiseConstantFunction.integral_add {I : BoundedInterval} {f g : ℝ → ℝ} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn.integral (f + g) ⋯ = PiecewiseConstantOn.integral f hf + PiecewiseConstantOn.integral g hg

Exercise 1.1.21 (a) (Linearity, integral of a sum)

theorem PiecewiseConstantFunction.integral_mono {I : BoundedInterval} {f g : ℝ → ℝ} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) (hmono : ∀ x ∈ ↑I, f x ≤ g x) : PiecewiseConstantOn.integral f hf ≤ PiecewiseConstantOn.integral g hg

Exercise 1.1.21 (b) (Monotonicity of the piecewise constant integral)

theorem PiecewiseConstantOn.indicator_of_elem (I : BoundedInterval) {E : Set ℝ} (hE : IsElementary (⇑Real.equiv_EuclideanSpace' '' E)) : PiecewiseConstantOn E.indicator' I

Exercise 1.1.21 (c) (Indicator functions, indicator is piecewise constant)

theorem PiecewiseConstantFunction.integral_of_elem {I : BoundedInterval} {E : Set ℝ} (hE : IsElementary (⇑Real.equiv_EuclideanSpace' '' E)) (hsub : E ⊆ ↑I) : PiecewiseConstantOn.integral E.indicator' ⋯ = hE.measure

Exercise 1.1.21 (c) (Indicator functions, integral of an indicator)

noncomputable def LowerDarbouxIntegral (f : ℝ → ℝ) (I : BoundedInterval) : ℝ

Definition 1.1.6 (Darboux integral, lower)

Equations

• LowerDarbouxIntegral f I = sSup {R : ℝ | ∃ (g : PiecewiseConstantFunction I), g.integral = R ∧ ∀ x ∈ ↑I, g.f x ≤ f x}

noncomputable def UpperDarbouxIntegral (f : ℝ → ℝ) (I : BoundedInterval) : ℝ

Definition 1.1.6 (Darboux integral, upper)

Equations

• UpperDarbouxIntegral f I = sInf {R : ℝ | ∃ (h : PiecewiseConstantFunction I), h.integral = R ∧ ∀ x ∈ ↑I, f x ≤ h.f x}

def PiecewiseConstantFunction.mkConst (I : BoundedInterval) (c : ℝ) : PiecewiseConstantFunction I

Helper: Construct a constant piecewise constant function with a given value

Equations

• PiecewiseConstantFunction.mkConst I c = { f := fun (x : ℝ) => c, T := {I}, c := fun (x : ↥{I}) => c, disjoint := ⋯, cover := ⋯, const := ⋯ }

theorem PiecewiseConstantFunction.integral_mkConst (I : BoundedInterval) (c : ℝ) : (mkConst I c).integral = c * I.length

Helper: The integral of a constant piecewise constant function

def PiecewiseConstantFunction.neg {I : BoundedInterval} (g : PiecewiseConstantFunction I) : PiecewiseConstantFunction I

Helper: Construct the negation of a piecewise constant function

Equations

• g.neg = { f := fun (x : ℝ) => -g.f x, T := g.T, c := fun (J : ↥g.T) => -g.c J, disjoint := ⋯, cover := ⋯, const := ⋯ }

theorem PiecewiseConstantFunction.integral_neg {I : BoundedInterval} (g : PiecewiseConstantFunction I) : g.neg.integral = -g.integral

Helper: The integral of a negated piecewise constant function

theorem PiecewiseConstantFunction.to_PiecewiseConstantOn {I : BoundedInterval} (g : PiecewiseConstantFunction I) : ∃ (h : PiecewiseConstantOn g.f I), PiecewiseConstantOn.integral g.f h = g.integral

Helper: Convert a PiecewiseConstantFunction to PiecewiseConstantOn and relate integrals

theorem PiecewiseConstantFunction.integral_mono' {I : BoundedInterval} (g h : PiecewiseConstantFunction I) (h_pointwise : ∀ x ∈ ↑I, g.f x ≤ h.f x) : g.integral ≤ h.integral

Helper: Apply PiecewiseConstantFunction.integral_mono between two PiecewiseConstantFunctions via PiecewiseConstantOn.

theorem LowerDarbouxIntegral.bddAbove {f : ℝ → ℝ} {I : BoundedInterval} (M : ℝ) (hM : ∀ x ∈ I, |f x| ≤ M) : BddAbove {R : ℝ | ∃ (g : PiecewiseConstantFunction I), g.integral = R ∧ ∀ x ∈ ↑I, g.f x ≤ f x}

Helper: The lower Darboux set is bounded above

theorem UpperDarbouxIntegral.bddBelow {f : ℝ → ℝ} {I : BoundedInterval} (M : ℝ) (hM : ∀ x ∈ I, |f x| ≤ M) : BddBelow {R : ℝ | ∃ (h : PiecewiseConstantFunction I), h.integral = R ∧ ∀ x ∈ ↑I, f x ≤ h.f x}

Helper: The upper Darboux set is bounded below

theorem lower_darboux_le_upper_darboux {f : ℝ → ℝ} {I : BoundedInterval} (hbound : ∃ (M : ℝ), ∀ x ∈ I, |f x| ≤ M) : LowerDarbouxIntegral f I ≤ UpperDarbouxIntegral f I

Definition 1.1.6 (Darboux integral, lower is at most upper)

noncomputable def DarbouxIntegrableOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

Definition 1.1.6 (Darboux integral, integrability)

Equations

• DarbouxIntegrableOn f I = (I = BoundedInterval.Icc I.a I.b ∧ (↑I).Nonempty ∧ (∃ (M : ℝ), ∀ x ∈ I, |f x| ≤ M) ∧ LowerDarbouxIntegral f I = UpperDarbouxIntegral f I)

noncomputable def darbouxIntegral (f : ℝ → ℝ) (I : BoundedInterval) : ℝ

We give the Darboux integral the "junk" value of the lower Darboux integral when the function is not integrable.

Equations

• darbouxIntegral f I = LowerDarbouxIntegral f I

theorem UpperDarbouxIntegral.bddBelow_neg {f : ℝ → ℝ} {I : BoundedInterval} (M : ℝ) (hM : ∀ x ∈ I, |f x| ≤ M) : BddBelow {R : ℝ | ∃ (h : PiecewiseConstantFunction I), h.integral = R ∧ ∀ x ∈ ↑I, (-f) x ≤ h.f x}

Helper: The upper Darboux set for -f is bounded below

theorem UpperDarbouxIntegral.neg {f : ℝ → ℝ} {I : BoundedInterval} (hbound : ∃ (M : ℝ), ∀ x ∈ I, |f x| ≤ M) : UpperDarbouxIntegral (-f) I = -LowerDarbouxIntegral f I

Definition 1.1.6 (Darboux integral, negation)

theorem RiemannIntegrableOn.iff_darbouxIntegrable {f : ℝ → ℝ} {I : BoundedInterval} (hbound : ∃ (M : ℝ), ∀ x ∈ I, |f x| ≤ M) : RiemannIntegrableOn f I ↔ DarbouxIntegrableOn f I

Exercise 1.1.22 (Riemann and Darboux integrability agree)

theorem riemann_integral_eq_darboux_integral {f : ℝ → ℝ} {I : BoundedInterval} (hf : RiemannIntegrableOn f I) : riemannIntegral f I = darbouxIntegral f I

Exercise 1.1.22 (the two integrals agree)

theorem RiemannIntegrableOn.continuous {f : ℝ → ℝ} {I : BoundedInterval} (hI : I = BoundedInterval.Icc I.a I.b) (hnonempty : (↑I).Nonempty) (hcont : ContinuousOn f ↑I) : RiemannIntegrableOn f I

Exercise 1.1.23

theorem RiemannIntegrableOn.piecewise_continuous {f : ℝ → ℝ} {I : BoundedInterval} (hI : I = BoundedInterval.Icc I.a I.b) (hnonempty : (↑I).Nonempty) (hbound : ∃ (M : ℝ), ∀ x ∈ I, |f x| ≤ M) (T : Finset BoundedInterval) (hdisjoint : (↑T).PairwiseDisjoint BoundedInterval.toSet) (hcover : ↑I = ⋃ J ∈ T, ↑J) (hcont : ∀ J ∈ T, ContinuousOn f ↑J) : RiemannIntegrableOn f I

Exercise 1.1.23'

theorem RiemannIntegrableOn.smul {I : BoundedInterval} (c : ℝ) {f : ℝ → ℝ} (h : RiemannIntegrableOn f I) : RiemannIntegrableOn (c • f) I

Exercise 1.1.24 (a) (scalar multiple, integrability).

theorem riemann_integral_smul {I : BoundedInterval} (c : ℝ) {f : ℝ → ℝ} (h : RiemannIntegrableOn f I) : riemannIntegral (c • f) I = c • riemannIntegral f I

Exercise 1.1.24 (a) (scalar multiple, integral).

theorem RiemannIntegrableOn.add {I : BoundedInterval} {f g : ℝ → ℝ} (hf : RiemannIntegrableOn f I) (hg : RiemannIntegrableOn g I) : RiemannIntegrableOn (f + g) I

Exercise 1.1.24 (a) (sum, integrability).

theorem riemann_integral_add {I : BoundedInterval} {f g : ℝ → ℝ} (hf : RiemannIntegrableOn f I) (hg : RiemannIntegrableOn g I) : riemannIntegral (f + g) I = riemannIntegral f I + riemannIntegral g I

Exercise 1.1.24 (a) (sum, integral).

theorem riemann_integral_mono {I : BoundedInterval} {f g : ℝ → ℝ} (hf : RiemannIntegrableOn f I) (hg : RiemannIntegrableOn g I) (hmono : ∀ x ∈ ↑I, f x ≤ g x) : riemannIntegral f I ≤ riemannIntegral g I

Exercise 1.1.24 (b) (Monotonicity of the piecewise constant integral)

theorem RiemannIntegrableOn.indicator_of_elem {I : BoundedInterval} (hI : I = BoundedInterval.Icc I.a I.b) (hnonempty : (↑I).Nonempty) {E : Set ℝ} (hE : JordanMeasurable (⇑Real.equiv_EuclideanSpace' '' E)) : RiemannIntegrableOn E.indicator' I

Exercise 1.1.24 (c) (Indicator functions)

theorem riemann_integral_of_elem {I : BoundedInterval} (hI : I = BoundedInterval.Icc I.a I.b) (hnonempty : (↑I).Nonempty) {E : Set ℝ} (hE : JordanMeasurable (⇑Real.equiv_EuclideanSpace' '' E)) (hsub : E ⊆ ↑I) : riemannIntegral E.indicator' I = hE.measure

Exercise 1.1.24 (c) (Piecewise constant integral of indicator functions)

theorem riemann_integral_unique {I : BoundedInterval} (integ : (ℝ → ℝ) → ℝ) (hsmul : ∀ (c : ℝ) (f : ℝ → ℝ), RiemannIntegrableOn f I → integ (c • f) = c • integ f) (hadd : ∀ (f g : ℝ → ℝ), RiemannIntegrableOn f I → RiemannIntegrableOn g I → integ (f + g) = integ f + integ g) (hmono : ∀ (f g : ℝ → ℝ), RiemannIntegrableOn f I → RiemannIntegrableOn g I → (∀ x ∈ ↑I, f x ≤ g x) → integ f ≤ integ g) (hindicator : ∀ (E : Set ℝ) (hE : JordanMeasurable (⇑Real.equiv_EuclideanSpace' '' E)), E ⊆ ↑I → integ E.indicator' = hE.measure) (f : ℝ → ℝ) : RiemannIntegrableOn f I → integ f = riemannIntegral f I

Exercise 1.1.24 (Uniqueness)

theorem RiemannIntegrableOn.measurable_upper {I : BoundedInterval} {f : ℝ → ℝ} (hfint : RiemannIntegrableOn f I) : JordanMeasurable {p : EuclideanSpace' 2 | p.ofLp 0 ∈ ↑I ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ f (p.ofLp 0)}

Exercise 1.1.25 (Area interpretation, region under the graph)

theorem RiemannIntegrableOn.measurable_lower {I : BoundedInterval} {f : ℝ → ℝ} (hfint : RiemannIntegrableOn f I) : JordanMeasurable {p : EuclideanSpace' 2 | p.ofLp 0 ∈ ↑I ∧ f (p.ofLp 0) ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 0}

Exercise 1.1.25 (Area interpretation, region below the graph)

theorem JordanMeasurable.iff_integrable {I : BoundedInterval} (hI : I = BoundedInterval.Icc I.a I.b) {f : ℝ → ℝ} (hf : ∃ (M : ℝ), ∀ x ∈ ↑I, |f x| ≤ M) : RiemannIntegrableOn f I ↔ JordanMeasurable {p : EuclideanSpace' 2 | p.ofLp 0 ∈ ↑I ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ f (p.ofLp 0)} ∧ JordanMeasurable {p : EuclideanSpace' 2 | p.ofLp 0 ∈ ↑I ∧ f (p.ofLp 0) ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 0}

Exercise 1.1.25 (Area interpretation, integrability criterion)

theorem RiemannIntegrableOn.eq_measure {I : BoundedInterval} {f : ℝ → ℝ} (hfint : RiemannIntegrableOn f I) : riemannIntegral f I = ⋯.measure - ⋯.measure

Exercise 1.1.25 (Area interpretation, integral as a difference of measures)