Imports
import Mathlib.Tactic
import Analysis.Section_9_8
import Analysis.Section_11_5Analysis I, Section 11.6: Riemann integrability of monotone functions
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:
-
Riemann integrability of monotone functions.
namespace Chapter11open Chapter9 BoundedIntervalProposition 11.6.1
set_option maxHeartbeats 300000 intheorem integ_of_monotone {a b:ℝ} {f:ℝ → ℝ} (hf: MonotoneOn f (Icc a b)) :
IntegrableOn f (Icc a b) := a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b)
-- This proof is adapted from the structure of the original text.
a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:0 < b - a⊢ IntegrableOn f (Icc a b)a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:¬0 < b - a⊢ IntegrableOn f (Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:¬0 < b - a⊢ IntegrableOn f (Icc a b)a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:0 < b - a⊢ IntegrableOn f (Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:¬0 < b - a⊢ IntegrableOn f (Icc a b) a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:¬0 < b - a⊢ (Icc a b).length = 0; a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:¬0 < b - a⊢ Subsingleton ↑↑(Icc a b); All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)hab:0 < b - ahbound:BddOn f (Set.Icc a b)⊢ IntegrableOn f (Icc a b)
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑I⊢ IntegrableOn f I
have hab' : a ≤ b := a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b) All goals completed! 🐙
have (ε:ℝ) (hε: 0 < ε) : upper_integral f I - lower_integral f I ≤ ((f b - f a) * (b-a)) *ε := a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b)
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑N⊢ upper_integral f I - lower_integral f I ≤ (f b - f a) * (b - a) * ε
have hNpos : 0 < N := a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b) a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑N⊢ 0 < ↑N; linarith [show 0 < 1/ε a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b) All goals completed! 🐙]
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑N⊢ upper_integral f I - lower_integral f I ≤ (f b - f a) * (b - a) * ε
have hδpos : 0 < δ := a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b) All goals completed! 🐙
have hbeq : b = a + δ*N := a:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b) a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δ⊢ b = a + (b - a) / ↑N * ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δ⊢ b = a + (b - a); All goals completed! 🐙
set e : ℕ ↪ BoundedInterval := {
toFun j := Ico (a + δ*j) (a + δ*(j+1))
inj' j k hjk := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Nj:ℕk:ℕhjk:(fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1))) j = (fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1))) k⊢ j = k a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Nj:ℕk:ℕhjk:j = k ∨ δ = 0⊢ j = k; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Nj:ℕk:ℕh✝:j = k⊢ j = ka:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Nj:ℕk:ℕh✝:δ = 0⊢ j = k a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Nj:ℕk:ℕh✝:j = k⊢ j = ka:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Nj:ℕk:ℕh✝:δ = 0⊢ j = k All goals completed! 🐙
}
set P : Partition I := {
intervals := insert (Icc b b) (.map e (.range N))
exists_unique := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ ∀ x ∈ I, ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J
intro x a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ I⊢ ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ I⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ J; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = b⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ Ja:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:¬x = b⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ J
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = b⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ J a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = b⊢ (Icc b b = Icc b b ∨ ∃ a < N, e a = Icc b b) ∧ x ∈ Icc b ba:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = b⊢ ∀ (y : BoundedInterval), (y = Icc b b ∨ ∃ a < N, e a = y) ∧ x ∈ y → y = Icc b b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = b⊢ (Icc b b = Icc b b ∨ ∃ a < N, e a = Icc b b) ∧ x ∈ Icc b b All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bhJb:x ∈ Icc b b⊢ Icc b b = Icc b ba:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bj:ℕhA:j < NhJb:x ∈ e j⊢ e j = Icc b b; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bj:ℕhA:j < NhJb:x ∈ e j⊢ e j = Icc b b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bj:ℕhA:j < NhJb:δ * ↑j ≤ δ * ↑N ∧ δ * ↑N < δ * (↑j + 1)⊢ e j = Icc b b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bj:ℕhA:j < NhJb:δ * ↑N < δ * (↑j + 1)⊢ e j = Icc b b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bj:ℕhA:j < NhJb:↑N < ↑j + 1⊢ e j = Icc b b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhx:x ∈ Ihb:x = bj:ℕhA:j < NhJb:N < j + 1⊢ e j = Icc b b; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ b⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ J
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ J
have hxa : 0 ≤ x-a := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ ∀ x ∈ I, ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J All goals completed! 🐙
have hxaδ : 0 ≤ (x-a)/δ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ ∀ x ∈ I, ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ ∃! J, (J = Icc b b ∨ ∃ a < N, e a = J) ∧ x ∈ J
have hxj : x ∈ e j := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ ∀ x ∈ I, ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ a + δ * ↑⌊(x - a) / δ⌋₊ ≤ x ∧ x < a + δ * (↑⌊(x - a) / δ⌋₊ + 1); a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ a + δ * ↑⌊(x - a) / δ⌋₊ ≤ xa:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ x < a + δ * (↑⌊(x - a) / δ⌋₊ + 1)
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ a + δ * ↑⌊(x - a) / δ⌋₊ ≤ x calc
_ ≤ a + δ * ((x-a)/δ) := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ a + δ * ↑⌊(x - a) / δ⌋₊ ≤ a + δ * ((x - a) / δ) a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ ↑⌊(x - a) / δ⌋₊ ≤ (x - a) / δ; All goals completed! 🐙
_ = x := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ a + δ * ((x - a) / δ) = x All goals completed! 🐙
calc
_ = a + δ * ((x-a)/δ) := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ x = a + δ * ((x - a) / δ) a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ x = a + (x - a); All goals completed! 🐙
_ < _ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ a + δ * ((x - a) / δ) < a + δ * (↑⌊(x - a) / δ⌋₊ + 1) a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < b⊢ (x - a) / δ < ↑⌊(x - a) / δ⌋₊ + 1; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ (e j = Icc b b ∨ ∃ a < N, e a = e j) ∧ x ∈ e ja:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ ∀ (y : BoundedInterval), (y = Icc b b ∨ ∃ a < N, e a = y) ∧ x ∈ y → y = e j
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ (e j = Icc b b ∨ ∃ a < N, e a = e j) ∧ x ∈ e j a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ e j = Icc b b ∨ ∃ a < N, e a = e j; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ ∃ a < N, e a = e j; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ j < N ∧ e j = e j; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e j⊢ x - a < δ * ↑N; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e jhxJ:x ∈ Icc b b⊢ Icc b b = e ja:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e jk:ℕhk:k < NhxJ:x ∈ e k⊢ e k = e j
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e jhxJ:x ∈ Icc b b⊢ Icc b b = e j a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:x ∈ e jhxJ:x = b⊢ Icc b b = e j; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bk:ℕhk:k < NhxJ:a + δ * ↑k ≤ x ∧ x < a + δ * (↑k + 1)hxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)⊢ e k = e j
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bk:ℕhk:k < NhxJ:a + δ * ↑k ≤ x ∧ x < a + δ * (↑k + 1)hxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hjk:j < k⊢ e k = e ja:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hk:j < NhxJ:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)⊢ e j = e ja:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bk:ℕhk:k < NhxJ:a + δ * ↑k ≤ x ∧ x < a + δ * (↑k + 1)hxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hjk:k < j⊢ e k = e j
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bk:ℕhk:k < NhxJ:a + δ * ↑k ≤ x ∧ x < a + δ * (↑k + 1)hxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hjk:j < k⊢ e k = e j replace hjk : δ*((j:ℝ)+1) ≤ δ*(k:ℝ) := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ ∀ x ∈ I, ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bk:ℕhk:k < NhxJ:a + δ * ↑k ≤ x ∧ x < a + δ * (↑k + 1)hxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hjk:j < k⊢ ↑j + 1 ≤ ↑k; All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bhxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hk:j < NhxJ:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)⊢ e j = e j All goals completed! 🐙
replace hjk : δ*((k:ℝ)+1) ≤ δ*(j:ℝ) := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ ∀ x ∈ I, ∃! J, J ∈ insert (Icc b b) (Finset.map e (Finset.range N)) ∧ x ∈ J a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }x:ℝhb:¬x = bhx:a ≤ x ∧ x ≤ bj:ℕ := ⌊(x - a) / δ⌋₊hxa:0 ≤ x - ahxaδ:0 ≤ (x - a) / δhxb:x < bk:ℕhk:k < NhxJ:a + δ * ↑k ≤ x ∧ x < a + δ * (↑k + 1)hxj:a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)hjk:k < j⊢ ↑k + 1 ≤ ↑j; All goals completed! 🐙
All goals completed! 🐙
contains J hJ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }J:BoundedIntervalhJ:J ∈ insert (Icc b b) (Finset.map e (Finset.range N))⊢ J ⊆ I
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }J:BoundedIntervalhJ:J = Icc b b ∨ ∃ a < N, e a = J⊢ J ⊆ I; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ Icc b b ⊆ Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ e j ⊆ I a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ Icc b b ⊆ Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ e j ⊆ I a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ Set.Ico (a + δ * ↑j) (a + δ * (↑j + 1)) ⊆ Set.Icc a b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }⊢ a ≤ b All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ a ≤ a + δ * ↑ja:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ a + δ * (↑j + 1) ≤ b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ a ≤ a + δ * ↑j a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ 0 ≤ δ * ↑j; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ δ * (↑j + 1) ≤ δ * ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }j:ℕhj:j < N⊢ ↑j + 1 ≤ ↑N; All goals completed! 🐙
}
have hup := calc
upper_integral f I ≤ ∑ J ∈ P.intervals, (sSup (f '' (J:Set ℝ))) * |J|ₗ := upper_integ_le_upper_sum hbound P
_ = ∑ j ∈ .range N, (sSup (f '' (Ico (a + δ*j) (a + δ*(j+1))))) * |Ico (a + δ*j) (a + δ*(j+1))|ₗ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∑ J ∈ P.intervals, sSup (f '' ↑J) * J.length =
∑ j ∈ Finset.range N,
sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∑ x ∈ Finset.range N, sSup (f '' ↑(e x)) * (e x).length =
∑ x ∈ Finset.range N,
sSup (f '' Set.Ico (a + δ * ↑x) (a + δ * (↑x + 1))) * (Ico (a + δ * ↑x) (a + δ * (↑x + 1))).length; All goals completed! 🐙
_ ≤ ∑ j ∈ .range N, f (a + δ*(j+1)) * δ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∑ j ∈ Finset.range N,
sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≤
∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∀ i ∈ Finset.range N,
sSup (f '' ↑(Ico (a + δ * ↑i) (a + δ * (↑i + 1)))) * (Ico (a + δ * ↑i) (a + δ * (↑i + 1))).length ≤
f (a + δ * (↑i + 1)) * δ; intro j a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≤
f (a + δ * (↑j + 1)) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length = δa:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) ≤ f (a + δ * (↑j + 1))
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length = δ a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ max (δ * (↑j + 1) - δ * ↑j) 0 = δ; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ max δ 0 = δ; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))).Nonemptya:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ ∀ b ∈ f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1))), b ≤ f (a + δ * (↑j + 1))
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))).Nonempty a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range N⊢ δ * ↑j < δ * (↑j + 1); All goals completed! 🐙
intro y a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Ny:ℝhy:y ∈ f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))⊢ y ≤ f (a + δ * (↑j + 1)); a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Ny:ℝhy:∃ x, (a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)) ∧ f x = y⊢ y ≤ f (a + δ * (↑j + 1)); a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ f x ≤ f (a + δ * (↑j + 1))
have : a + δ*(j+1) ≤ b := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∑ j ∈ Finset.range N,
sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≤
∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ δ * (↑j + 1) ≤ δ * ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ ↑j + 1 ≤ ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ j + 1 ≤ N; All goals completed! 🐙
have hδj : 0 ≤ δ*j := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∑ j ∈ Finset.range N,
sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≤
∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ All goals completed! 🐙
have hδj1 : 0 ≤ δ*(j+1) := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }⊢ ∑ j ∈ Finset.range N,
sSup (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≤
∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ All goals completed! 🐙
apply hf _ _ (a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)this:a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ x ≤ a + δ * (↑j + 1) All goals completed! 🐙) a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)this:a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ x ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }j:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)this:a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ a + δ * (↑j + 1) ∈ ↑I All goals completed! 🐙; All goals completed! 🐙
have hdown := calc
lower_integral f I ≥ ∑ J ∈ P.intervals, (sInf (f '' (J:Set ℝ))) * |J|ₗ :=
lower_integ_ge_lower_sum hbound P
_ = ∑ j ∈ .range N, (sInf (f '' (Ico (a + δ*j) (a + δ*(j+1))))) * |Ico (a + δ*j) (a + δ*(j+1))|ₗ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∑ J ∈ P.intervals, sInf (f '' ↑J) * J.length =
∑ j ∈ Finset.range N,
sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∑ x ∈ Finset.range N, sInf (f '' ↑(e x)) * (e x).length =
∑ x ∈ Finset.range N,
sInf (f '' Set.Ico (a + δ * ↑x) (a + δ * (↑x + 1))) * (Ico (a + δ * ↑x) (a + δ * (↑x + 1))).length; All goals completed! 🐙
_ ≥ ∑ j ∈ .range N, f (a + δ*j) * δ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∑ j ∈ Finset.range N,
sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≥
∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∀ i ∈ Finset.range N,
f (a + δ * ↑i) * δ ≤ sInf (f '' ↑(Ico (a + δ * ↑i) (a + δ * (↑i + 1)))) * (Ico (a + δ * ↑i) (a + δ * (↑i + 1))).length; intro j a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ f (a + δ * ↑j) * δ ≤ sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length = δa:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ f (a + δ * ↑j) ≤ sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1))))
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length = δ a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ max (δ * (↑j + 1) - δ * ↑j) 0 = δ; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ max δ 0 = δ; All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))).Nonemptya:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ ∀ b ∈ f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1))), f (a + δ * ↑j) ≤ b
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))).Nonempty a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range N⊢ δ * ↑j < δ * (↑j + 1); All goals completed! 🐙
intro y a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Ny:ℝhy:y ∈ f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))⊢ f (a + δ * ↑j) ≤ y; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Ny:ℝhy:∃ x, (a + δ * ↑j ≤ x ∧ x < a + δ * (↑j + 1)) ∧ f x = y⊢ f (a + δ * ↑j) ≤ y; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ f (a + δ * ↑j) ≤ f x
have hajb': a + δ*(j+1) ≤ b := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∑ j ∈ Finset.range N,
sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≥
∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ δ * (↑j + 1) ≤ δ * ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ ↑j + 1 ≤ ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)⊢ j + 1 ≤ N; All goals completed! 🐙
have hδj : 0 ≤ δ*j := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∑ j ∈ Finset.range N,
sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≥
∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ All goals completed! 🐙
have hδj1 : 0 ≤ δ*(j+1) := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ⊢ ∑ j ∈ Finset.range N,
sInf (f '' ↑(Ico (a + δ * ↑j) (a + δ * (↑j + 1)))) * (Ico (a + δ * ↑j) (a + δ * (↑j + 1))).length ≥
∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ a + δ * ↑j ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ x ∈ ↑I a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ a + δ * ↑j ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ x ∈ ↑I a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ a ≤ x ∧ x ≤ b a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ a + δ * ↑j ≤ ba:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δj:ℕhj:j ∈ Finset.range Nx:ℝhx1:a + δ * ↑j ≤ xhx2:x < a + δ * (↑j + 1)hajb':a + δ * (↑j + 1) ≤ bhδj:0 ≤ δ * ↑jhδj1:0 ≤ δ * (↑j + 1)⊢ a ≤ x ∧ x ≤ b All goals completed! 🐙
calc
_ ≤ ∑ j ∈ .range N, f (a + δ*(j+1)) * δ - ∑ j ∈ .range N, f (a + δ*j) * δ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ upper_integral f I - lower_integral f I ≤
∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ - ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ All goals completed! 🐙
_ = (f b - f a) * δ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δ - ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ = (f b - f a) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ ∑ x ∈ Finset.range N, (f (a + δ * (↑x + 1)) * δ - f (a + δ * ↑x) * δ) = (f b - f a) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:∑ i ∈ Finset.range N, (f (a + δ * ↑(i + 1)) * δ - f (a + δ * ↑i) * δ) = f (a + δ * ↑N) * δ - f (a + δ * ↑0) * δ⊢ ∑ x ∈ Finset.range N, (f (a + δ * (↑x + 1)) * δ - f (a + δ * ↑x) * δ) = (f b - f a) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:∑ x ∈ Finset.range N, (f (a + δ * (↑x + 1)) * δ - f (a + δ * ↑x) * δ) = f (a + δ * ↑N) * δ - f (a + δ * ↑0) * δ⊢ ∑ x ∈ Finset.range N, (f (a + δ * (↑x + 1)) * δ - f (a + δ * ↑x) * δ) = (f b - f a) * δ
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:∑ x ∈ Finset.range N, (f (a + δ * (↑x + 1)) * δ - f (a + δ * ↑x) * δ) = f (a + δ * ↑N) * δ - f (a + δ * ↑0) * δ⊢ (f b - f a) * δ = f (a + δ * ↑N) * δ - f (a + δ * ↑0) * δ; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:∑ x ∈ Finset.range N, (f (a + δ * (↑x + 1)) * δ - f (a + δ * ↑x) * δ) = f (a + δ * ↑N) * δ - f (a + δ * ↑0) * δ⊢ (f (a + δ * ↑N) - f a) * δ = f (a + δ * ↑N) * δ - f a * δ; All goals completed! 🐙
_ ≤ _ := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ (f b - f a) * δ ≤ (f b - f a) * (b - a) * ε
have : 0 ≤ f b - f a := a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ (f b - f a) * δ ≤ (f b - f a) * (b - a) * ε a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ f a ≤ f b; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ a ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ b ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ a ≤ b a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ a ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ b ∈ ↑Ia:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δ⊢ a ≤ b All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ (f b - f a) * ((b - a) / ↑N) ≤ (f b - f a) * ((b - a) * ε); a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ (b - a) / ↑N ≤ (b - a) * ε
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ b - a ≤ (b - a) * (ε * ↑N)a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < ↑N
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ (b - a) * 1 ≤ (b - a) * (ε * ↑N)a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < ↑N
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 1 ≤ ε * ↑Na:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 1 / ε ≤ ↑Na:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < εa:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < ↑N; a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < εa:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bε:ℝhε:0 < εN:ℕhN:1 / ε < ↑NhNpos:0 < Nδ:ℝ := (b - a) / ↑Nhδpos:0 < δhbeq:b = a + δ * ↑Ne:ℕ ↪ BoundedInterval := { toFun := fun j ↦ Ico (a + δ * ↑j) (a + δ * (↑j + 1)), inj' := ⋯ }P:Partition I := { intervals := insert (Icc b b) (Finset.map e (Finset.range N)), exists_unique := ⋯, contains := ⋯ }hup:upper_integral f I ≤ ∑ j ∈ Finset.range N, f (a + δ * (↑j + 1)) * δhdown:lower_integral f I ≥ ∑ j ∈ Finset.range N, f (a + δ * ↑j) * δthis:0 ≤ f b - f a⊢ 0 < ↑N
all_goals All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bthis:∀ (ε : ℝ), 0 < ε → upper_integral f I - lower_integral f I ≤ (f b - f a) * (b - a) * ε⊢ lower_integral f I = upper_integral f I
a:ℝb:ℝf:ℝ → ℝhab:0 < b - ahbound:BddOn f (Set.Icc a b)I:BoundedInterval := Icc a bhf:MonotoneOn f ↑Ihab':a ≤ bthis:∀ (ε : ℝ), 0 < ε → upper_integral f I - lower_integral f I ≤ (f b - f a) * (b - a) * εlow_le_up:lower_integral f I ≤ upper_integral f I⊢ lower_integral f I = upper_integral f I
All goals completed! 🐙Proposition 11.6.1
theorem integ_of_antitone {a b:ℝ} {f:ℝ → ℝ} (hf: AntitoneOn f (Icc a b)) :
IntegrableOn f (Icc a b) := a:ℝb:ℝf:ℝ → ℝhf:AntitoneOn f ↑(Icc a b)⊢ IntegrableOn f (Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:AntitoneOn f ↑(Icc a b)⊢ IntegrableOn (- -f) (Icc a b); a:ℝb:ℝf:ℝ → ℝhf:AntitoneOn f ↑(Icc a b)⊢ MonotoneOn (-f) ↑(Icc a b); All goals completed! 🐙Corollary 11.6.3 / Exercise 11.6.1
theorem integ_of_bdd_monotone {I:BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I)
(hf: MonotoneOn f I) : IntegrableOn f I := I:BoundedIntervalf:ℝ → ℝhbound:BddOn f ↑Ihf:MonotoneOn f ↑I⊢ IntegrableOn f I
All goals completed! 🐙theorem integ_of_bdd_antitone {I:BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I)
(hf: AntitoneOn f I) : IntegrableOn f I := I:BoundedIntervalf:ℝ → ℝhbound:BddOn f ↑Ihf:AntitoneOn f ↑I⊢ IntegrableOn f I
All goals completed! 🐙Proposition 11.6.4 (Integral test)
theorem summable_iff_integ_of_antitone {f:ℝ → ℝ} (hnon: ∀ x ≥ 0, f x ≥ 0)
(hf: AntitoneOn f (.Ici 0)) :
Summable f ↔ ∃ M, ∀ N ≥ 0, integ f (Icc 0 N) ≤ M := f:ℝ → ℝhnon:∀ x ≥ 0, f x ≥ 0hf:AntitoneOn f (Set.Ici 0)⊢ Summable f ↔ ∃ M, ∀ N ≥ 0, integ f (Icc 0 N) ≤ M
All goals completed! 🐙-- Exercise 11.6.2: Formulate a reasonable notion of a piecewise monotone function, and then
-- show that all bounded piecewise monotone functions are Riemann integrable.
/-- Exercise 11.6.4 -/
example : ∃ (f:ℝ → ℝ) (hnon: ∀ x ≥ 0, f x ≥ 0), Summable f ∧ ¬ ∃ M, ∀ N ≥ 0, integ f (Icc 0 N) ≤ M := ⊢ ∃ f, ∃ (_ : ∀ x ≥ 0, f x ≥ 0), Summable f ∧ ¬∃ M, ∀ N ≥ 0, integ f (Icc 0 N) ≤ M
All goals completed! 🐙example : ∃ (f:ℝ → ℝ) (hnon: ∀ x ≥ 0, f x ≥ 0), ¬ Summable f ∧ ∃ M, ∀ N ≥ 0, integ f (Icc 0 N) ≤ M := ⊢ ∃ f, ∃ (_ : ∀ x ≥ 0, f x ≥ 0), ¬Summable f ∧ ∃ M, ∀ N ≥ 0, integ f (Icc 0 N) ≤ M
All goals completed! 🐙end Chapter11