theorem Chapter9.MonotoneOn.iff {X : Set ℝ} (f : ℝ → ℝ) : MonotoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x

Definition 9.8.1

theorem Chapter9.StrictMono.iff {X : Set ℝ} (f : ℝ → ℝ) : StrictMonoOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x

theorem Chapter9.AntitoneOn.iff {X : Set ℝ} (f : ℝ → ℝ) : AntitoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x

theorem Chapter9.StrictAntitone.iff {X : Set ℝ} (f : ℝ → ℝ) : StrictAntiOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x

theorem Chapter9.MonotoneOn.exist_inverse {a b : ℝ} (h : a < b) (f : ℝ → ℝ) (hcont : ContinuousOn f (Set.Icc a b)) (hmono : StrictMonoOn f (Set.Icc a b)) : f '' Set.Icc a b = Set.Icc (f a) (f b) ∧ ∃ (finv : ℝ → ℝ), ContinuousOn finv (Set.Icc (f a) (f b)) ∧ StrictMonoOn finv (Set.Icc (f a) (f b)) ∧ finv '' Set.Icc (f a) (f b) = Set.Icc a b ∧ (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧ ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y

Proposition 9.8.3 / Exercise 9.8.4

theorem Chapter9.IsMaxOn.of_monotone_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : MonotoneOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax

Exercise 9.8.1

theorem Chapter9.IsMaxOn.of_strictmono_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : StrictMonoOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax

theorem Chapter9.IsMaxOn.of_antitone_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : AntitoneOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax

theorem Chapter9.IsMaxOn.of_strictantitone_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : StrictAntiOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax

theorem Chapter9.BddOn.of_monotone {a b : ℝ} {f : ℝ → ℝ} (hf : MonotoneOn f (Set.Icc a b)) : BddOn f (Set.Icc a b)

theorem Chapter9.BddOn.of_antitone {a b : ℝ} {f : ℝ → ℝ} (hf : AntitoneOn f (Set.Icc a b)) : BddOn f (Set.Icc a b)

theorem Chapter9.no_strictmono_intermediate_value : ∃ (a : ℝ) (b : ℝ) (_ : a < b) (f : ℝ → ℝ) (_ : StrictMonoOn f (Set.Icc a b)) (y : ℝ), (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ ¬∃ c ∈ Set.Icc a b, f c = y

Exercise 9.8.2

theorem Chapter9.no_monotone_intermediate_value : ∃ (a : ℝ) (b : ℝ) (_ : a < b) (f : ℝ → ℝ) (_ : MonotoneOn f (Set.Icc a b)) (y : ℝ), (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ ¬∃ c ∈ Set.Icc a b, f c = y

theorem Chapter9.no_strictanti_intermediate_value : ∃ (a : ℝ) (b : ℝ) (_ : a < b) (f : ℝ → ℝ) (_ : StrictAntiOn f (Set.Icc a b)) (y : ℝ), (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ ¬∃ c ∈ Set.Icc a b, f c = y

theorem Chapter9.no_antitone_intermediate_value : ∃ (a : ℝ) (b : ℝ) (_ : a < b) (f : ℝ → ℝ) (_ : AntitoneOn f (Set.Icc a b)) (y : ℝ), (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ ¬∃ c ∈ Set.Icc a b, f c = y

theorem Chapter9.mono_of_continuous_inj {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hinj : Function.Injective fun (x : ↑(Set.Icc a b)) => f ↑x) : StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)

Exercise 9.8.3

def Chapter9.MonotoneOn.exist_inverse_without_continuity : Decidable (∀ (a b : ℝ), a < b → ∀ (f : ℝ → ℝ), StrictMonoOn f (Set.Icc a b) → f '' Set.Icc a b = Set.Icc (f a) (f b) ∧ ∃ (finv : ℝ → ℝ), ContinuousOn finv (Set.Icc (f a) (f b)) ∧ StrictMonoOn finv (Set.Icc (f a) (f b)) ∧ finv '' Set.Icc (f a) (f b) = Set.Icc a b ∧ (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧ ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y)

Exercise 9.8.4

Equations

• Chapter9.MonotoneOn.exist_inverse_without_continuity = sorry

def Chapter9.MonotoneOn.exist_inverse_without_strictmono : Decidable (∀ (a b : ℝ), a < b → ∀ (f : ℝ → ℝ), ContinuousOn f (Set.Icc a b) → MonotoneOn f (Set.Icc a b) → f '' Set.Icc a b = Set.Icc (f a) (f b) ∧ ∃ (finv : ℝ → ℝ), ContinuousOn finv (Set.Icc (f a) (f b)) ∧ StrictMonoOn finv (Set.Icc (f a) (f b)) ∧ finv '' Set.Icc (f a) (f b) = Set.Icc a b ∧ (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧ ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y)

Exercise 9.8.4

Equations

• Chapter9.MonotoneOn.exist_inverse_without_strictmono = sorry

@[reducible, inline]

noncomputable abbrev Chapter9.q_9_8_5 : ℕ ≃ ℚ

An equivalence between the natural numbers and the rationals.

Equations

• Chapter9.q_9_8_5 = Chapter9.q_9_8_5._proof_1.some

@[reducible, inline]

noncomputable abbrev Chapter9.g_9_8_5 : ℚ → ℝ

Equations

• Chapter9.g_9_8_5 q = 2 ^ (-↑(Chapter9.q_9_8_5.symm q))

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_8_5 : ℝ → ℝ

Equations

• Chapter9.f_9_8_5 x = ∑' (r : { r : ℚ // ↑r < x }), Chapter9.g_9_8_5 ↑r

theorem Chapter9.StrictMonoOn.of_f_9_8_5 : StrictMonoOn f_9_8_5 Set.univ

Exercise 9.8.5(a)

theorem Chapter9.ContinuousAt.of_f_9_8_5' (r : ℚ) : ¬ContinuousAt f_9_8_5 ↑r

Exercise 9.8.5(b)

theorem Chapter9.ContinuousAt.of_f_9_8_5 {x : ℝ} (hx : ¬∃ (r : ℚ), x = ↑r) : ContinuousAt f_9_8_5 x

Exercise 9.8.5(c)