danabra.mov
My solutions to Tao's Analysis I, formalized in Lean
1import Mathlib.Tactic
2import Mathlib.Topology.Instances.Irrational
3import Analysis.Section_11_6
4
5/-!
6# Analysis I, Section 11.8: The Riemann-Stieltjes integral
7
8I have attempted to make the translation as faithful a paraphrasing as possible of the original
9text. When there is a choice between a more idiomatic Lean solution and a more faithful
10translation, I have generally chosen the latter. In particular, there will be places where the
11Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided
12doing so.
13
14Main constructions and results of this section:
15- Definition of α-length.
16- The piecewise constant Riemann-Stieltjes integral.
17- The full Riemann-Stieltjes integral.
18
19Technical notes:
20- In Lean it is more convenient to make definitions such as α-length and the Riemann-Stieltjes
21 integral totally defined, thus assigning "junk" values to the cases where the definition is
22 not intended to be applied. For the definition of α-length, the definition is intended to be
23 applied in contexts where left and right limits exist, and the function is extended by
24 constants to the left and right of its intended domain of definition; for instance, if a
25 function `f` is defined on `Icc 0 1`, then it is intended that `f x = f 1` for all `x ≥ 1`
26 and `f x = f 0` for all `x ≤ 0`; in particular, at a right endpoint, the value of a function
27 is intended to agree with its right limit, and similarly for the left endpoint, although we
28 do not enforce this in our definition of α-length. (For functions defined on open intervals,
29 the extension is immaterial.)
30- The notion of α-length and piecewise constant Riemann-Stieltjes integral is intended for
31 situations where left and right limits exist, such as for monotone functions or continuous
32 functions, though technically they make sense without these hypotheses. The full Riemann-Stieltjes
33 integral is intended for functions that are of bounded variation, though we shall restrict
34 attention to the special case of monotone increasing functions for the most part.
35-/
36
37namespace Chapter11
38
39open BoundedInterval Chapter9
40
41/-- Left and right limits. A junk value is assigned if the limit does not exist. -/
42noncomputable abbrev right_lim (f: ℝ → ℝ) (x₀:ℝ) : ℝ := lim ((nhdsWithin x₀ (.Ioi x₀)).map f)
43
44noncomputable abbrev left_lim (f: ℝ → ℝ) (x₀:ℝ) : ℝ := lim ((nhdsWithin x₀ (.Iio x₀)).map f)
45
46theorem right_lim_def {f: ℝ → ℝ} {x₀ L:ℝ} (h: Convergesto (.Ioi x₀) f L x₀) :
47 right_lim f x₀ = L := by
48 apply lim_eq; rwa [Convergesto.iff, ←nhdsWithin.eq_1, Filter.Tendsto.eq_1] at h
49
50theorem left_lim_def {f: ℝ → ℝ} {x₀ L:ℝ} (h: Convergesto (.Iio x₀) f L x₀) :
51 left_lim f x₀ = L := by
52 apply lim_eq; rwa [Convergesto.iff, ←nhdsWithin.eq_1, Filter.Tendsto.eq_1] at h
53
54noncomputable abbrev jump (f: ℝ → ℝ) (x₀:ℝ) : ℝ :=
55 right_lim f x₀ - left_lim f x₀
56
57/-- Right limits exist for continuous functions -/
58theorem right_lim_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ}
59 (h : ∃ ε>0, .Ico x₀ (x₀+ε) ⊆ X) (hf: ContinuousWithinAt f X x₀) :
60 right_lim f x₀ = f x₀ := by
61 obtain ⟨ ε, hε, hX ⟩ := h
62 apply right_lim_def
63 rw [ContinuousWithinAt.eq_1] at hf
64 replace hf : (nhdsWithin x₀ (.Ioo x₀ (x₀ + ε))).Tendsto f (nhds (f x₀)) :=
65 tendsto_nhdsWithin_mono_left (Set.Ioo_subset_Ico_self.trans hX) hf
66 rw [Convergesto.iff, ←nhdsWithin.eq_1]
67 convert hf using 1
68 have h1 : .Ioo x₀ (x₀ + ε) ∈ nhdsWithin x₀ (.Ioi x₀) := by
69 convert inter_mem_nhdsWithin (t := .Ioo (x₀-ε) (x₀+ε)) _ _
70 . ext; simp; intros; linarith
71 apply Ioo_mem_nhds <;> linarith
72 rw [←nhdsWithin_inter_of_mem h1]; congr 1; simp [Set.Ioo_subset_Ioi_self]
73
74/-- Left limits exist for continuous functions -/
75theorem left_lim_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ}
76 (h : ∃ ε>0, .Ioc (x₀-ε) x₀ ⊆ X) (hf: ContinuousWithinAt f X x₀) :
77 left_lim f x₀ = f x₀ := by
78 obtain ⟨ ε, hε, hX ⟩ := h
79 apply left_lim_def
80 rw [ContinuousWithinAt.eq_1] at hf
81 replace hf : (nhdsWithin x₀ (.Ioo (x₀ - ε) x₀)).Tendsto f (nhds (f x₀)) :=
82 tendsto_nhdsWithin_mono_left (Set.Ioo_subset_Ioc_self.trans hX) hf
83 rw [Convergesto.iff, ←nhdsWithin.eq_1]
84 convert hf using 1
85 have h1 : .Ioo (x₀-ε) x₀ ∈ nhdsWithin x₀ (.Iio x₀) := by
86 convert inter_mem_nhdsWithin (t := .Ioo (x₀-ε) (x₀+ε)) _ _
87 . ext; simp; exact ⟨ by intro ⟨ h1, h2 ⟩; simp [h1, h2]; linarith, by aesop ⟩
88 apply Ioo_mem_nhds <;> linarith
89 rw [←nhdsWithin_inter_of_mem h1]
90 congr 1; simp [Set.Ioo_subset_Iio_self]
91
92/-- No jump for continuous functions -/
93theorem jump_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ}
94 (h : X ∈ nhds x₀) (hf: ContinuousWithinAt f X x₀) :
95 jump f x₀ = 0 := by
96 rw [mem_nhds_iff_exists_Ioo_subset] at h
97 obtain ⟨ l, u, hx₀, hX ⟩ := h; simp at hx₀
98 have hl : ∃ ε>0, .Ioc (x₀-ε) x₀ ⊆ X :=
99 ⟨ x₀-l, by linarith, Set.Subset.trans (by intro _ _; simp_all; linarith) hX ⟩
100 have hu : ∃ ε>0, .Ico x₀ (x₀+ε) ⊆ X :=
101 ⟨ u-x₀, by linarith, Set.Subset.trans (by intro _ _; simp_all; linarith) hX ⟩
102 simp [jump, left_lim_of_continuous hl hf, right_lim_of_continuous hu hf]
103
104/-- Right limits exist for monotone functions -/
105theorem right_lim_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
106 Convergesto (.Ioi x₀) f (sInf (f '' .Ioi x₀)) x₀ := by
107 rw [Convergesto.iff, ←nhdsWithin.eq_1]
108 apply (hf.monotoneOn _).tendsto_nhdsGT
109 rw [bddBelow_def]; use f x₀; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
110
111theorem right_lim_of_monotone' {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
112 right_lim f x₀ = sInf (f '' .Ioi x₀) := right_lim_def (right_lim_of_monotone x₀ hf)
113
114/-- Left limits exist for monotone functions -/
115theorem left_lim_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
116 Convergesto (.Iio x₀) f (sSup (f '' .Iio x₀)) x₀ := by
117 rw [Convergesto.iff, ←nhdsWithin.eq_1]
118 apply (hf.monotoneOn _).tendsto_nhdsLT
119 rw [bddAbove_def]; use f x₀; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
120
121theorem left_lim_of_monotone' {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
122 left_lim f x₀ = sSup (f '' .Iio x₀) := left_lim_def (left_lim_of_monotone x₀ hf)
123
124theorem jump_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
125 0 ≤ jump f x₀ := by
126 simp [jump, left_lim_of_monotone' x₀ hf, right_lim_of_monotone' x₀ hf]
127 apply csSup_le (by simp); intro a ha
128 apply le_csInf (by simp); intro b hb; simp at ha hb
129 obtain ⟨ x, hx, rfl ⟩ := ha; obtain ⟨ y, hy, rfl ⟩ := hb
130 apply hf; linarith
131
132theorem right_lim_le_left_lim_of_monotone {f:ℝ → ℝ} {a b:ℝ} (hab: a < b)
133 (hf: Monotone f) :
134 right_lim f a ≤ left_lim f b := by
135 rw [left_lim_of_monotone' b hf, right_lim_of_monotone' a hf]
136 calc
137 _ ≤ f ((a+b)/2) := by
138 apply ConditionallyCompleteLattice.csInf_le
139 . rw [bddBelow_def]; use f a; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
140 simp; use (a+b)/2; simp; linarith
141 _ ≤ _ := by
142 apply ConditionallyCompleteLattice.le_csSup
143 . rw [bddAbove_def]; use f b; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
144 simp; use (a+b)/2; simp; linarith
145
146/-- Definition 11.8.1 -/
147noncomputable abbrev α_length (α: ℝ → ℝ) (I: BoundedInterval) : ℝ := match I with
148| Icc a b => if a ≤ b then (right_lim α b) - (left_lim α a) else 0
149| Ico a b => if a ≤ b then (left_lim α b) - (left_lim α a) else 0
150| Ioc a b => if a ≤ b then (right_lim α b) - (right_lim α a) else 0
151| Ioo a b => if a < b then (left_lim α b) - (right_lim α a) else 0
152
153notation3:max α"["I"]ₗ" => α_length α I
154
155theorem α_length_of_empty (α: ℝ → ℝ) {I: BoundedInterval} (hI: (I:Set ℝ) = ∅) : α[I]ₗ = 0 :=
156 match I with
157 | Icc _ _ => by simp [Set.Icc_eq_empty_iff] at *; intros; linarith
158 | Ico a b => by simp [Set.Ico_eq_empty_iff] at *; intros; simp [show a=b by linarith]
159 | Ioc a b => by simp [Set.Ioc_eq_empty_iff] at *; intros; simp [show a=b by linarith]
160 | Ioo _ _ => by simp [Set.Ioo_eq_empty_iff] at *; intros; linarith
161
162@[simp]
163theorem α_length_of_pt {α: ℝ → ℝ} (a:ℝ) : α[Icc a a]ₗ = jump α a := by simp [α_length, jump]
164
165theorem α_length_of_cts {α:ℝ → ℝ} {I: BoundedInterval} {a b: ℝ}
166 (haa: a < I.a) (hab: I.a ≤ I.b) (hbb: I.b < b)
167 (hI : I ⊆ Ioo a b) (hα: ContinuousOn α (Ioo a b)) :
168 α[I]ₗ = α I.b - α I.a := by
169 have ha_left : left_lim α I.a = α I.a := by
170 apply left_lim_of_continuous _ (hα.continuousWithinAt (by simp [haa]; linarith))
171 exact ⟨ I.a - a, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
172 have ha_right : right_lim α I.a = α I.a := by
173 apply right_lim_of_continuous _ (hα.continuousWithinAt (by simp [haa]; linarith))
174 exact ⟨ b - I.a, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
175 have hb_left : left_lim α I.b = α I.b := by
176 apply left_lim_of_continuous _ (hα.continuousWithinAt (by simp [hbb]; linarith))
177 exact ⟨ I.b - a, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
178 have hb_right : right_lim α I.b = α I.b := by
179 apply right_lim_of_continuous _ (hα.continuousWithinAt (by simp [hbb]; linarith))
180 exact ⟨ b - I.b, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
181 cases I with
182 | Icc _ _ => simp [α_length, hb_right, ha_left, hab]
183 | Ico _ _ => simp [α_length, hb_left, ha_left, hab]
184 | Ioc _ _ => simp [α_length, hb_right, ha_right, hab]
185 | Ioo a' b' => simp [α_length, hb_left, ha_right]; intros; simp [show a' = b' by linarith]
186
187/-- Example 11.8.2-/
188example : (fun x ↦ x^2)[Icc 2 3]ₗ = 5 := by
189 sorry
190
191example : (fun x ↦ x^2)[Icc 2 2]ₗ = 0 := by
192 sorry
193
194example : (fun x ↦ x^2)[Ioo 2 2]ₗ = 0 := by
195 sorry
196
197/-- Example 11.8.3-/
198@[simp]
199theorem α_len_of_id (I: BoundedInterval) : (fun x ↦ x)[I]ₗ = |I|ₗ := by
200 sorry
201
202/-- An improved version of BoundedInterval.joins that also controls α-length. -/
203abbrev BoundedInterval.joins' (K I J: BoundedInterval) : Prop := K.joins I J ∧ ∀ α:ℝ → ℝ, α[K]ₗ = α[I]ₗ + α[J]ₗ
204
205theorem BoundedInterval.join_Icc_Ioc' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins' (Icc a b) (Ioc b c) := by
206 refine ⟨ join_Icc_Ioc hab hbc, ?_ ⟩
207 simp [α_length, show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
208
209theorem BoundedInterval.join_Icc_Ioo' {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ico a c).joins' (Icc a b) (Ioo b c) := by
210 refine ⟨ join_Icc_Ioo hab hbc, ?_ ⟩
211 simp [α_length, show a ≤ b by linarith, show b < c by linarith, show a ≤ c by linarith]
212
213theorem BoundedInterval.join_Ioc_Ioc' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ioc a c).joins' (Ioc a b) (Ioc b c) := by
214 refine ⟨ join_Ioc_Ioc hab hbc, ?_ ⟩
215 simp [α_length, show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
216
217theorem BoundedInterval.join_Ioc_Ioo' {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ioo a c).joins' (Ioc a b) (Ioo b c) := by
218 refine ⟨ join_Ioc_Ioo hab hbc, ?_ ⟩
219 simp [α_length, show a ≤ b by linarith, show b < c by linarith, show a < c by linarith]
220
221theorem BoundedInterval.join_Ico_Icc' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins' (Ico a b) (Icc b c) := by
222 refine ⟨ join_Ico_Icc hab hbc, ?_ ⟩
223 simp [α_length, show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
224
225theorem BoundedInterval.join_Ico_Ico' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ico a c).joins' (Ico a b) (Ico b c) := by
226 refine ⟨ join_Ico_Ico hab hbc, ?_ ⟩
227 simp [α_length, show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
228
229theorem BoundedInterval.join_Ioo_Icc' {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioc a c).joins' (Ioo a b) (Icc b c) := by
230 refine ⟨ join_Ioo_Icc hab hbc, ?_ ⟩
231 simp [α_length, show a < b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
232
233theorem BoundedInterval.join_Ioo_Ico' {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioo a c).joins' (Ioo a b) (Ico b c) := by
234 refine ⟨ join_Ioo_Ico hab hbc, ?_ ⟩
235 simp [α_length, show a < b by linarith, show b ≤ c by linarith, show a < c by linarith]
236
237/-- Theorem 11.8.4 / Exercise 11.8.1 -/
238theorem Partition.sum_of_α_length {I: BoundedInterval} (P: Partition I) (α: ℝ → ℝ) :
239 ∑ J ∈ P.intervals, α[J]ₗ = α[I]ₗ := by
240 sorry
241
242/-- Definition 11.8.5 (Piecewise constant RS integral)-/
243noncomputable abbrev PiecewiseConstantWith.RS_integ (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) (α: ℝ → ℝ) :
244 ℝ := ∑ J ∈ P.intervals, constant_value_on f (J:Set ℝ) * α[J]ₗ
245
246/-- Example 11.8.6 -/
247noncomputable abbrev f_11_8_6 (x:ℝ) : ℝ := if x < 2 then 4 else 2
248
249noncomputable abbrev P_11_8_6 : Partition (Icc 1 3) :=
250 (⊥: Partition (Ico 1 2)).join (⊥ : Partition (Icc 2 3))
251 (join_Ico_Icc (by norm_num) (by norm_num) )
252
253theorem f_11_8_6_RS_integ : PiecewiseConstantWith.RS_integ f_11_8_6 P_11_8_6 (fun x ↦ x) = 22 := by
254 sorry
255
256/-- Example 11.8.7 -/
257theorem PiecewiseConstantWith.RS_integ_eq_integ {f:ℝ → ℝ} {I: BoundedInterval} (P: Partition I) :RS_integ f P (fun x ↦ x) = integ f P := by
258 sorry
259
260/-- Analogue of Proposition 11.2.13 -/
261theorem PiecewiseConstantWith.RS_integ_eq {f:ℝ → ℝ} {I: BoundedInterval} {P P': Partition I}
262 (hP: PiecewiseConstantWith f P) (hP': PiecewiseConstantWith f P') (α:ℝ → ℝ): RS_integ f P α = RS_integ f P' α := by
263 sorry
264
265open Classical in
266noncomputable abbrev PiecewiseConstantOn.RS_integ (f:ℝ → ℝ) (I: BoundedInterval) (α:ℝ → ℝ):
267 ℝ := if h: PiecewiseConstantOn f I then PiecewiseConstantWith.RS_integ f h.choose α else 0
268
269theorem PiecewiseConstantOn.RS_integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
270 (h: PiecewiseConstantWith f P) (α:ℝ → ℝ) : RS_integ f I α = PiecewiseConstantWith.RS_integ f P α := by
271 have h' : PiecewiseConstantOn f I := by use P
272 simp [RS_integ, h']; exact PiecewiseConstantWith.RS_integ_eq h'.choose_spec h α
273
274/-- α-length non-negative when α monotone -/
275theorem α_length_nonneg_of_monotone {α:ℝ → ℝ} (hα: Monotone α) (I: BoundedInterval):
276 0 ≤ α[I]ₗ := by
277 sorry
278
279/-- Analogue of Theorem 11.2.16 (a) (Laws of integration) / Exercise 11.8.3 -/
280theorem PiecewiseConstantOn.RS_integ_add {f g: ℝ → ℝ} {I: BoundedInterval}
281 (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) {α:ℝ → ℝ} (hα: Monotone α):
282 RS_integ (f + g) I α = RS_integ f I α + RS_integ g I α := by
283 sorry
284
285/-- Analogue of Theorem 11.2.16 (b) (Laws of integration) / Exercise 11.8.3 -/
286theorem PiecewiseConstantOn.RS_integ_smul {f: ℝ → ℝ} {I: BoundedInterval} (c:ℝ)
287 (hf: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α) :
288 RS_integ (c • f) I α = c * RS_integ f I α
289 := by
290 sorry
291
292/-- Theorem 11.8.8 (c) (Laws of RS integration) / Exercise 11.8.8 -/
293theorem PiecewiseConstantOn.RS_integ_sub {f g: ℝ → ℝ} {I: BoundedInterval}
294 {α:ℝ → ℝ} (hα: Monotone α)
295 (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
296 RS_integ (f - g) I α = RS_integ f I α - RS_integ g I α := by
297 sorry
298
299/-- Theorem 11.8.8 (d) (Laws of RS integration) / Exercise 11.8.8 -/
300theorem PiecewiseConstantOn.RS_integ_of_nonneg {f: ℝ → ℝ} {I: BoundedInterval}
301 {α:ℝ → ℝ} (hα: Monotone α)
302 (h: ∀ x ∈ I, 0 ≤ f x) (hf: PiecewiseConstantOn f I) :
303 0 ≤ RS_integ f I α := by
304 sorry
305
306/-- Theorem 11.8.8 (e) (Laws of RS integration) / Exercise 11.8.8 -/
307theorem PiecewiseConstantOn.RS_integ_mono {f g: ℝ → ℝ} {I: BoundedInterval}
308 {α:ℝ → ℝ} (hα: Monotone α)
309 (h: ∀ x ∈ I, f x ≤ g x) (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
310 RS_integ f I α ≤ RS_integ g I α := by
311 sorry
312
313/-- Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.8 -/
314theorem PiecewiseConstantOn.RS_integ_const (c: ℝ) (I: BoundedInterval) {α:ℝ → ℝ} (hα: Monotone α) :
315 RS_integ (fun _ ↦ c) I α = c * α[I]ₗ := by
316 sorry
317
318/-- Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.8 -/
319theorem PiecewiseConstantOn.RS_integ_const' {f:ℝ → ℝ} {I: BoundedInterval}
320 {α:ℝ → ℝ} (hα: Monotone α) (h: ConstantOn f I) :
321 RS_integ f I α = (constant_value_on f I) * α[I]ₗ := by
322 sorry
323
324open Classical in
325/-- Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8 -/
326theorem PiecewiseConstantOn.RS_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J)
327 {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α):
328 PiecewiseConstantOn (fun x ↦ if x ∈ I then f x else 0) J := by
329 sorry
330
331open Classical in
332/-- Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8 -/
333theorem PiecewiseConstantOn.RS_integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J)
334 {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α):
335 RS_integ (fun x ↦ if x ∈ I then f x else 0) J α = RS_integ f I α := by
336 sorry
337
338/-- Theorem 11.8.8 (h) (Laws of RS integration) / Exercise 11.8.8 -/
339theorem PiecewiseConstantOn.RS_integ_of_join {I J K: BoundedInterval} (hIJK: K.joins' I J)
340 {f: ℝ → ℝ} (h: PiecewiseConstantOn f K) {α:ℝ → ℝ} (hα: Monotone α):
341 RS_integ f K α = RS_integ f I α + RS_integ f J α := by
342 sorry
343
344/-- Analogue of Definition 11.3.2 (Uppper and lower Riemann integrals )-/
345noncomputable abbrev upper_RS_integral (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ): ℝ :=
346 sInf ((PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
347
348noncomputable abbrev lower_RS_integral (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ): ℝ :=
349 sSup ((PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
350
351lemma RS_integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval}
352 (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα:Monotone α)
353 : M * α[I]ₗ ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := by
354 simp; refine ⟨ fun _ ↦ M, ⟨ ⟨ ?_, ?_ ⟩, PiecewiseConstantOn.RS_integ_const M I hα ⟩ ⟩
355 . peel h with _ _ _; simp_all [abs_le']
356 exact (ConstantOn.of_const (c := M) (by simp)).piecewiseConstantOn
357
358
359lemma RS_integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα:Monotone α)
360 : -M * α[I]ₗ ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := by
361 simp; refine ⟨ fun _ ↦ -M, ⟨ ⟨ ?_, ?_ ⟩, by convert PiecewiseConstantOn.RS_integ_const _ _ hα using 1; simp ⟩ ⟩
362 . peel h with _ _ _; simp [abs_le'] at *; linarith
363 exact (ConstantOn.of_const (c := -M) (by simp)).piecewiseConstantOn
364
365
366lemma RS_integral_bound_upper_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
367 {α:ℝ → ℝ} (hα: Monotone α) :
368 ((PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
369 obtain ⟨ M, h ⟩ := h; exact Set.nonempty_of_mem (RS_integral_bound_upper_of_bounded h hα)
370
371lemma RS_integral_bound_lower_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
372 {α:ℝ → ℝ} (hα: Monotone α) :
373 ((PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
374 obtain ⟨ M, h ⟩ := h; exact Set.nonempty_of_mem (RS_integral_bound_lower_of_bounded h hα)
375
376lemma RS_integral_bound_lower_le_upper {f:ℝ → ℝ} {I: BoundedInterval} {a b:ℝ}
377 {α:ℝ → ℝ} (hα: Monotone α)
378 (ha: a ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
379 (hb: b ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
380 : b ≤ a:= by
381 obtain ⟨ g, ⟨ ⟨ hmaj, hgp⟩, hgi ⟩ ⟩ := ha
382 obtain ⟨ h, ⟨ ⟨ hmin, hhp⟩, hhi ⟩ ⟩ := hb
383 rw [←hgi, ←hhi]; apply hhp.RS_integ_mono hα _ hgp; intro _ hx; linarith [hmin _ hx, hmaj _ hx]
384
385lemma RS_integral_bound_below {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
386 {α:ℝ → ℝ} (hα: Monotone α) :
387 BddBelow ((PiecewiseConstantOn.RS_integ · I α) ''
388 {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
389 rw [bddBelow_def]; use (RS_integral_bound_lower_nonempty h hα).some
390 intro a ha; exact RS_integral_bound_lower_le_upper hα ha (RS_integral_bound_lower_nonempty h hα).some_mem
391
392lemma RS_integral_bound_above {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
393 {α:ℝ → ℝ} (hα: Monotone α):
394 BddAbove ((PiecewiseConstantOn.RS_integ · I α) ''
395 {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
396 rw [bddAbove_def]; use (RS_integral_bound_upper_nonempty h hα).some
397 intro b hb; exact RS_integral_bound_lower_le_upper hα (RS_integral_bound_upper_nonempty h hα).some_mem hb
398
399lemma le_lower_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M)
400 {α:ℝ → ℝ} (hα: Monotone α) :
401 -M * α[I]ₗ ≤ lower_RS_integral f I α :=
402 ConditionallyCompleteLattice.le_csSup _ _
403 (RS_integral_bound_above (BddOn.of_bounded h) hα) (RS_integral_bound_lower_of_bounded h hα)
404
405lemma lower_RS_integral_le_upper {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
406 {α:ℝ → ℝ} (hα: Monotone α) :
407 lower_RS_integral f I α ≤ upper_RS_integral f I α := by
408 apply ConditionallyCompleteLattice.csSup_le _ _ (RS_integral_bound_lower_nonempty h hα) _
409 rw [mem_upperBounds]; intros
410 apply ConditionallyCompleteLattice.le_csInf _ _ (RS_integral_bound_upper_nonempty h hα) _
411 rw [mem_lowerBounds]; intros; solve_by_elim [RS_integral_bound_lower_le_upper]
412
413lemma RS_upper_integral_le {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M)
414 {α:ℝ → ℝ} (hα: Monotone α) :
415 upper_RS_integral f I α ≤ M * α[I]ₗ :=
416 ConditionallyCompleteLattice.csInf_le _ _
417 (RS_integral_bound_below (.of_bounded h) hα) (RS_integral_bound_upper_of_bounded h hα)
418
419lemma upper_RS_integral_le_integ {f g:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
420 (hfg: MajorizesOn g f I) (hg: PiecewiseConstantOn g I)
421 {α:ℝ → ℝ} (hα: Monotone α) :
422 upper_RS_integral f I α ≤ PiecewiseConstantOn.RS_integ g I α :=
423 ConditionallyCompleteLattice.csInf_le _ _ (RS_integral_bound_below hf hα) ⟨ g, by simpa [hg] ⟩
424
425lemma integ_le_lower_RS_integral {f h:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
426 (hfh: MinorizesOn h f I) (hg: PiecewiseConstantOn h I)
427 {α:ℝ → ℝ} (hα: Monotone α) :
428 PiecewiseConstantOn.RS_integ h I α ≤ lower_RS_integral f I α :=
429 ConditionallyCompleteLattice.le_csSup _ _ (RS_integral_bound_above hf hα) ⟨ h, by simpa [hg] ⟩
430
431lemma lt_of_gt_upper_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
432 {α: ℝ → ℝ} (hα: Monotone α) {X:ℝ} (hX: upper_RS_integral f I α < X ) :
433 ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X := by
434 have ⟨ Y, hY, hYX ⟩ := exists_lt_of_csInf_lt (RS_integral_bound_upper_nonempty hf hα) hX
435 simp at hY; obtain ⟨ g, ⟨ hmaj, hgp ⟩, hgi ⟩ := hY; exact ⟨ g, hmaj, hgp, by rwa [hgi] ⟩
436
437lemma gt_of_lt_lower_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
438 {α:ℝ → ℝ} (hα: Monotone α) {X:ℝ} (hX: X < lower_RS_integral f I α) :
439 ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α := by
440 have ⟨ Y, hY, hYX ⟩ := exists_lt_of_lt_csSup (RS_integral_bound_lower_nonempty hf hα) hX
441 simp at hY; obtain ⟨ h, ⟨ hmin, hhp ⟩, hhi ⟩ := hY; exact ⟨ h, hmin, hhp, by rwa [hhi] ⟩
442
443/-- Analogue of Definition 11.3.4 -/
444noncomputable abbrev RS_integ (f:ℝ → ℝ) (I: BoundedInterval) (α:ℝ → ℝ) : ℝ := upper_RS_integral f I α
445
446noncomputable abbrev RS_IntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ) : Prop :=
447 BddOn f I ∧ lower_RS_integral f I α = upper_RS_integral f I α
448
449/-- Analogue of various components of Lemma 11.3.3 -/
450theorem upper_RS_integral_eq_upper_integral (f:ℝ → ℝ) (I: BoundedInterval) :
451 upper_RS_integral f I (fun x ↦ x) = upper_integral f I := by
452 sorry
453
454theorem lower_RS_integral_eq_lower_integral (f:ℝ → ℝ) (I: BoundedInterval) :
455 lower_RS_integral f I (fun x ↦ x) = lower_integral f I := by
456 sorry
457
458theorem RS_integ_eq_integ (f:ℝ → ℝ) (I: BoundedInterval) :
459 RS_integ f I (fun x ↦ x) = integ f I := by
460 sorry
461
462theorem RS_IntegrableOn_iff_IntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) :
463 RS_IntegrableOn f I (fun x ↦ x) ↔ IntegrableOn f I := by
464 sorry
465
466/-- Exercise 11.8.4 -/
467theorem RS_integ_of_uniform_cts {I: BoundedInterval} {f:ℝ → ℝ} (hf: UniformContinuousOn f I)
468 {α:ℝ → ℝ} (hα: Monotone α):
469 RS_IntegrableOn f I α := by
470 sorry
471
472/-- Exercise 11.8.5 -/
473theorem RS_integ_with_sign (f:ℝ → ℝ) (hf: ContinuousOn f (.Icc (-1) 1)) : RS_IntegrableOn f (Icc (-1) 1) Real.sign ∧ RS_integ f (Icc (-1) 1) (fun x ↦ -Real.sign x) = 2 * f 0 := by
474 sorry
475
476/-- Analogue of Lemma 11.3.7 -/
477theorem RS_integ_of_piecewise_const {f:ℝ → ℝ} {I: BoundedInterval} (hf: PiecewiseConstantOn f I)
478 {α: ℝ → ℝ} (hα: Monotone α):
479 RS_IntegrableOn f I α ∧ RS_integ f I α = PiecewiseConstantOn.RS_integ f I α := by
480 sorry
481
482end Chapter11