Analysis
9.8. Monotone functions

Imports

import Mathlib.Tactic
import Analysis.Section_9_6

Analysis I, Section 9.8: Monotonic 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:

Review of Mathlib monotonicity concepts.

namespace Chapter9

Definition 9.8.1

theorem MonotoneOn.iff {X: Set ℝ} (f: ℝ → ℝ) : MonotoneOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x := byX:Set ℝf:ℝ → ℝ⊢ MonotoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ MonotoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x) → MonotoneOn f X
  .mpX:Set ℝf:ℝ → ℝ⊢ MonotoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x introsmpX:Set ℝf:ℝ → ℝa✝³:MonotoneOn f Xx✝:ℝa✝²:x✝ ∈ Xy✝:ℝa✝¹:y✝ ∈ Xa✝:y✝ > x✝⊢ f y✝ ≥ f x✝; solve_by_elim [le_of_lt]All goals completed! 🐙
  intro _ _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝ⊢ a✝ ∈ X → ∀ ⦃b : ℝ⦄, b ∈ X → a✝ ≤ b → f a✝ ≤ f b _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝:a✝ ∈ X⊢ ∀ ⦃b : ℝ⦄, b ∈ X → a✝ ≤ b → f a✝ ≤ f b _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝:a✝ ∈ Xb✝:ℝ⊢ b✝ ∈ X → a✝ ≤ b✝ → f a✝ ≤ f b✝ _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ X⊢ a✝ ≤ b✝ → f a✝ ≤ f b✝ hxymprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ Xhxy:a✝ ≤ b✝⊢ f a✝ ≤ f b✝; obtain hxy | rfl := le_iff_lt_or_eq.mp hxympr.inlX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ Xhxy✝:a✝ ≤ b✝hxy:a✝ < b✝⊢ f a✝ ≤ f b✝mpr.inrX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝¹:a✝ ∈ Xx✝:a✝ ∈ Xhxy:a✝ ≤ a✝⊢ f a✝ ≤ f a✝
  .mpr.inlX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ Xhxy✝:a✝ ≤ b✝hxy:a✝ < b✝⊢ f a✝ ≤ f b✝ solve_by_elimAll goals completed! 🐙
  simpAll goals completed! 🐙

theorem StrictMono.iff {X: Set ℝ} (f: ℝ → ℝ) : StrictMonoOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x := byX:Set ℝf:ℝ → ℝ⊢ StrictMonoOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ StrictMonoOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x) → StrictMonoOn f X <;>mpX:Set ℝf:ℝ → ℝ⊢ StrictMonoOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x) → StrictMonoOn f X introsmprX:Set ℝf:ℝ → ℝa✝:∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x⊢ StrictMonoOn f X <;>mpX:Set ℝf:ℝ → ℝa✝³:StrictMonoOn f Xx✝:ℝa✝²:x✝ ∈ Xy✝:ℝa✝¹:y✝ ∈ Xa✝:y✝ > x✝⊢ f y✝ > f x✝mprX:Set ℝf:ℝ → ℝa✝:∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x⊢ StrictMonoOn f X solve_by_elimAll goals completed! 🐙

theorem AntitoneOn.iff {X: Set ℝ} (f: ℝ → ℝ) : AntitoneOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x := byX:Set ℝf:ℝ → ℝ⊢ AntitoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ AntitoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x) → AntitoneOn f X
  .mpX:Set ℝf:ℝ → ℝ⊢ AntitoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x introsmpX:Set ℝf:ℝ → ℝa✝³:AntitoneOn f Xx✝:ℝa✝²:x✝ ∈ Xy✝:ℝa✝¹:y✝ ∈ Xa✝:y✝ > x✝⊢ f y✝ ≤ f x✝; solve_by_elim [le_of_lt]All goals completed! 🐙
  intro _ _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝ⊢ a✝ ∈ X → ∀ ⦃b : ℝ⦄, b ∈ X → a✝ ≤ b → f b ≤ f a✝ _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝:a✝ ∈ X⊢ ∀ ⦃b : ℝ⦄, b ∈ X → a✝ ≤ b → f b ≤ f a✝ _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝:a✝ ∈ Xb✝:ℝ⊢ b✝ ∈ X → a✝ ≤ b✝ → f b✝ ≤ f a✝ _mprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ X⊢ a✝ ≤ b✝ → f b✝ ≤ f a✝ hxymprX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ Xhxy:a✝ ≤ b✝⊢ f b✝ ≤ f a✝; obtain hxy | rfl := le_iff_lt_or_eq.mp hxympr.inlX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ Xhxy✝:a✝ ≤ b✝hxy:a✝ < b✝⊢ f b✝ ≤ f a✝mpr.inrX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝¹:a✝ ∈ Xx✝:a✝ ∈ Xhxy:a✝ ≤ a✝⊢ f a✝ ≤ f a✝
  .mpr.inlX:Set ℝf:ℝ → ℝa✝¹:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xa✝:ℝx✝¹:a✝ ∈ Xb✝:ℝx✝:b✝ ∈ Xhxy✝:a✝ ≤ b✝hxy:a✝ < b✝⊢ f b✝ ≤ f a✝ solve_by_elimAll goals completed! 🐙
  simpAll goals completed! 🐙

theorem StrictAntitone.iff {X: Set ℝ} (f: ℝ → ℝ) : StrictAntiOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x := byX:Set ℝf:ℝ → ℝ⊢ StrictAntiOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ StrictAntiOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x) → StrictAntiOn f X <;>mpX:Set ℝf:ℝ → ℝ⊢ StrictAntiOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x) → StrictAntiOn f X introsmprX:Set ℝf:ℝ → ℝa✝:∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x⊢ StrictAntiOn f X <;>mpX:Set ℝf:ℝ → ℝa✝³:StrictAntiOn f Xx✝:ℝa✝²:x✝ ∈ Xy✝:ℝa✝¹:y✝ ∈ Xa✝:y✝ > x✝⊢ f y✝ < f x✝mprX:Set ℝf:ℝ → ℝa✝:∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x⊢ StrictAntiOn f X solve_by_elimAll goals completed! 🐙

/-- Examples 9.8.2 -/
declaration uses `sorry`example : StrictMonoOn (fun x:ℝ ↦ x^2) (.Ici 0) := by⊢ StrictMonoOn (fun x ↦ x ^ 2) (Set.Ici 0) sorryAll goals completed! 🐙

declaration uses `sorry`example : StrictAntiOn (fun x:ℝ ↦ x^2) (.Iic 0) := by⊢ StrictAntiOn (fun x ↦ x ^ 2) (Set.Iic 0) sorryAll goals completed! 🐙

declaration uses `sorry`example : ¬ MonotoneOn (fun x:ℝ ↦ x^2) .univ := by⊢ ¬MonotoneOn (fun x ↦ x ^ 2) Set.univ sorryAll goals completed! 🐙

declaration uses `sorry`example : ¬ AntitoneOn (fun x:ℝ ↦ x^2) .univ := by⊢ ¬AntitoneOn (fun x ↦ x ^ 2) Set.univ sorryAll goals completed! 🐙

declaration uses `sorry`example {X:Set ℝ} {f:ℝ → ℝ} (hf: StrictMonoOn f X) : MonotoneOn f X := byX:Set ℝf:ℝ → ℝhf:StrictMonoOn f X⊢ MonotoneOn f X sorryAll goals completed! 🐙

declaration uses `sorry`example (X:Set ℝ) : MonotoneOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝ⊢ MonotoneOn (fun x ↦ 6) X sorryAll goals completed! 🐙

declaration uses `sorry`example (X:Set ℝ) : AntitoneOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝ⊢ AntitoneOn (fun x ↦ 6) X sorryAll goals completed! 🐙

nontrivial_iff.{u_1} {α : Type u_1} : Nontrivial α ↔ ∃ x y, x ≠ y#check nontrivial_iff

nontrivial_iff.{u_1} {α : Type u_1} : Nontrivial α ↔ ∃ x y, x ≠ y

declaration uses `sorry`example {X:Set ℝ} (hX: Nontrivial X) : ¬ StrictMonoOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝhX:Nontrivial ↑X⊢ ¬StrictMonoOn (fun x ↦ 6) X sorryAll goals completed! 🐙

declaration uses `sorry`example (X:Set ℝ) (hX: Nontrivial X) : ¬ StrictAntiOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝhX:Nontrivial ↑X⊢ ¬StrictAntiOn (fun x ↦ 6) X sorryAll goals completed! 🐙

declaration uses `sorry`example : ∃ (X:Set ℝ) (f:ℝ → ℝ), ContinuousOn f X ∧ ¬ MonotoneOn f X ∧ ¬ AntitoneOn f X := by⊢ ∃ X f, ContinuousOn f X ∧ ¬MonotoneOn f X ∧ ¬AntitoneOn f X sorryAll goals completed! 🐙

declaration uses `sorry`example : ∃ (X:Set ℝ) (f:ℝ → ℝ), MonotoneOn f X ∧ ¬ ContinuousOn f X := by⊢ ∃ X f, MonotoneOn f X ∧ ¬ContinuousOn f X sorryAll goals completed! 🐙

Proposition 9.8.3 / Exercise 9.8.4

theorem declaration uses `sorry`MonotoneOn.exist_inverse {a b:ℝ} (h: a < b) (f: ℝ → ℝ) (hcont: ContinuousOn f (.Icc a b)) (hmono: StrictMonoOn f (.Icc a b)) :
  f '' (.Icc a b) = .Icc (f a) (f b) ∧
  ∃ finv: ℝ → ℝ, ContinuousOn finv (.Icc (f a) (f b)) ∧ StrictMonoOn finv (.Icc (f a) (f b)) ∧
  finv '' (.Icc (f a) (f b)) = .Icc a b ∧
  (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧
  ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y
   := bya:ℝb:ℝh:a < bf:ℝ → ℝ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
  sorryAll goals completed! 🐙

/-- Example 9.8.4 -/
example {R :ℝ} (hR: R > 0) {n:ℕ} (hn: n > 0) : ∃ g : ℝ → ℝ, ∀ x ∈ Set.Icc 0 (R^n), (g x)^n = x := byR:ℝhR:R > 0n:ℕhn:n > 0⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
  set f : ℝ → ℝ := fun x ↦ x^nR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ n⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
  have hcont : ContinuousOn f (.Icc 0 R) := byR:ℝhR:R > 0n:ℕhn:n > 0⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x fun_propAll goals completed! 🐙
  have hmono : StrictMonoOn f (.Icc 0 R) := byR:ℝhR:R > 0n:ℕhn:n > 0⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
    intro _ hxR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ nhcont:ContinuousOn f (Set.Icc 0 R)a✝:ℝhx:a✝ ∈ Set.Icc 0 R⊢ ∀ ⦃b : ℝ⦄, b ∈ Set.Icc 0 R → a✝ < b → f a✝ < f b _R:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ nhcont:ContinuousOn f (Set.Icc 0 R)a✝:ℝhx:a✝ ∈ Set.Icc 0 Rb✝:ℝ⊢ b✝ ∈ Set.Icc 0 R → a✝ < b✝ → f a✝ < f b✝ _R:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ nhcont:ContinuousOn f (Set.Icc 0 R)a✝:ℝhx:a✝ ∈ Set.Icc 0 Rb✝:ℝx✝:b✝ ∈ Set.Icc 0 R⊢ a✝ < b✝ → f a✝ < f b✝ hxyR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ nhcont:ContinuousOn f (Set.Icc 0 R)a✝:ℝhx:a✝ ∈ Set.Icc 0 Rb✝:ℝx✝:b✝ ∈ Set.Icc 0 Rhxy:a✝ < b✝⊢ f a✝ < f b✝; simp_all [f]R:ℝn:ℕf:ℝ → ℝ := fun x ↦ x ^ na✝:ℝb✝:ℝhR:0 < Rhn:0 < nhcont:ContinuousOn (fun x ↦ x ^ n) (Set.Icc 0 R)hx:0 ≤ a✝ ∧ a✝ ≤ Rx✝:0 ≤ b✝ ∧ b✝ ≤ Rhxy:a✝ < b✝⊢ a✝ ^ n < b✝ ^ n
    apply pow_lt_pow_left₀ hxyhaR:ℝn:ℕf:ℝ → ℝ := fun x ↦ x ^ na✝:ℝb✝:ℝhR:0 < Rhn:0 < nhcont:ContinuousOn (fun x ↦ x ^ n) (Set.Icc 0 R)hx:0 ≤ a✝ ∧ a✝ ≤ Rx✝:0 ≤ b✝ ∧ b✝ ≤ Rhxy:a✝ < b✝⊢ 0 ≤ a✝aR:ℝn:ℕf:ℝ → ℝ := fun x ↦ x ^ na✝:ℝb✝:ℝhR:0 < Rhn:0 < nhcont:ContinuousOn (fun x ↦ x ^ n) (Set.Icc 0 R)hx:0 ≤ a✝ ∧ a✝ ≤ Rx✝:0 ≤ b✝ ∧ b✝ ≤ Rhxy:a✝ < b✝⊢ n ≠ 0 <;>haR:ℝn:ℕf:ℝ → ℝ := fun x ↦ x ^ na✝:ℝb✝:ℝhR:0 < Rhn:0 < nhcont:ContinuousOn (fun x ↦ x ^ n) (Set.Icc 0 R)hx:0 ≤ a✝ ∧ a✝ ≤ Rx✝:0 ≤ b✝ ∧ b✝ ≤ Rhxy:a✝ < b✝⊢ 0 ≤ a✝aR:ℝn:ℕf:ℝ → ℝ := fun x ↦ x ^ na✝:ℝb✝:ℝhR:0 < Rhn:0 < nhcont:ContinuousOn (fun x ↦ x ^ n) (Set.Icc 0 R)hx:0 ≤ a✝ ∧ a✝ ≤ Rx✝:0 ≤ b✝ ∧ b✝ ≤ Rhxy:a✝ < b✝⊢ n ≠ 0 grindAll goals completed! 🐙
  obtain ⟨ g, ⟨ _, _, _, _, hg⟩ ⟩ := (MonotoneOn.exist_inverse (byR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ nhcont:ContinuousOn f (Set.Icc 0 R)hmono:StrictMonoOn f (Set.Icc 0 R)⊢ 0 < R positivityAll goals completed! 🐙) f hcont hmono).2
  simp only [f, zero_pow (by positivity)] at hgR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x ↦ x ^ nhcont:ContinuousOn f (Set.Icc 0 R)hmono:StrictMonoOn f (Set.Icc 0 R)g:ℝ → ℝleft✝³:ContinuousOn g (Set.Icc (f 0) (f R))left✝²:StrictMonoOn g (Set.Icc (f 0) (f R))left✝¹:g '' Set.Icc (f 0) (f R) = Set.Icc 0 Rleft✝:∀ x ∈ Set.Icc 0 R, g (f x) = xhg:∀ y ∈ Set.Icc 0 (R ^ n), g y ^ n = y⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x; use gAll goals completed! 🐙

Exercise 9.8.1

theorem declaration uses `sorry`IsMaxOn.of_monotone_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: MonotoneOn f (.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:MonotoneOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax sorryAll goals completed! 🐙

              theorem declaration uses `sorry`IsMaxOn.of_strictmono_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: StrictMonoOn f (.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:StrictMonoOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax sorryAll goals completed! 🐙theorem declaration uses `sorry`IsMaxOn.of_antitone_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: AntitoneOn f (.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:AntitoneOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax sorryAll goals completed! 🐙theorem declaration uses `sorry`IsMaxOn.of_strictantitone_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: StrictAntiOn f (.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:StrictAntiOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
  sorryAll goals completed! 🐙theorem declaration uses `sorry`BddOn.of_monotone {a b:ℝ} {f:ℝ → ℝ} (hf: MonotoneOn f (.Icc a b)) :
  BddOn f (.Icc a b) := bya:ℝb:ℝf:ℝ → ℝhf:MonotoneOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b)
  sorryAll goals completed! 🐙theorem declaration uses `sorry`BddOn.of_antitone {a b:ℝ} {f:ℝ → ℝ} (hf: AntitoneOn f (.Icc a b)) :
  BddOn f (.Icc a b) := bya:ℝb:ℝf:ℝ → ℝhf:AntitoneOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b)
  sorryAll goals completed! 🐙

Exercise 9.8.2

theorem declaration uses `sorry`no_strictmono_intermediate_value :
    ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictMonoOn f (.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 := by⊢ ∃ 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 sorryAll goals completed! 🐙

              theorem declaration uses `sorry`no_monotone_intermediate_value :
    ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: MonotoneOn f (.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 := by⊢ ∃ 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 sorryAll goals completed! 🐙theorem declaration uses `sorry`no_strictanti_intermediate_value :
    ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictAntiOn f (.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 := by⊢ ∃ 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 sorryAll goals completed! 🐙theorem declaration uses `sorry`no_antitone_intermediate_value :
    ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: AntitoneOn f (.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 := by⊢ ∃ 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 sorryAll goals completed! 🐙

Exercise 9.8.3

theorem declaration uses `sorry`mono_of_continuous_inj {a b:ℝ} (h: a < b) {f:ℝ → ℝ}
  (hf: ContinuousOn f (.Icc a b))
  (hinj: Function.Injective (fun x: Set.Icc a b ↦ f x )) :
  StrictMonoOn f (.Icc a b) ∨ StrictAntiOn f (.Icc a b) := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hinj:Function.Injective fun x ↦ f ↑x⊢ StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)
  sorryAll goals completed! 🐙

Exercise 9.8.4 (without continuity)

def declaration uses `sorry`MonotoneOn.exist_inverse_without_continuity :
    Decidable (∀ (a b : ℝ) (_ : a < b) (f : ℝ → ℝ) (_ : StrictMonoOn f (.Icc a b)),
      f '' (.Icc a b) = .Icc (f a) (f b) ∧
      ∃ finv : ℝ → ℝ, ContinuousOn finv (.Icc (f a) (f b)) ∧ StrictMonoOn finv (.Icc (f a) (f b)) ∧
        finv '' (.Icc (f a) (f b)) = .Icc a b ∧
        (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧
        ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y) := by⊢ 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)
  -- apply isFalse: strict mono alone doesn't guarantee a continuous inverse
  sorryAll goals completed! 🐙

Exercise 9.8.4 (without strict monotonicity)

def declaration uses `sorry`MonotoneOn.exist_inverse_without_strictmono :
    Decidable (∀ (a b : ℝ) (_ : a < b) (f : ℝ → ℝ) (_ : ContinuousOn f (.Icc a b))
        (_ : MonotoneOn f (.Icc a b)),
      f '' (.Icc a b) = .Icc (f a) (f b) ∧
      ∃ finv : ℝ → ℝ, ContinuousOn finv (.Icc (f a) (f b)) ∧ StrictMonoOn finv (.Icc (f a) (f b)) ∧
        finv '' (.Icc (f a) (f b)) = .Icc a b ∧
        (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧
        ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y) := by⊢ 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)
  -- apply isFalse: e.g. a constant monotone f on [a,b] has no strict inverse
  sorryAll goals completed! 🐙

An equivalence between the natural numbers and the rationals.

/-
Exercise 9.8.4: state and prove an analogue of `MonotoneOn.exist_inverse` for `Antitone`
functions.
-/
-- theorem AntitoneOn.exist_inverse {a b:ℝ} (h: a < b) (f: ℝ → ℝ) (hcont: ContinuousOn f (.Icc a b)) (hmono: StrictAntiOn f (.Icc a b)) : sorry := by sorry

noncomputable abbrev q_9_8_5 : ℕ ≃ ℚ := nonempty_equiv_of_countable.some

noncomputable abbrev g_9_8_5 : ℚ → ℝ := fun q ↦ (2:ℝ)^(-q_9_8_5.symm q:ℤ)noncomputable abbrev f_9_8_5 : ℝ → ℝ := fun x ↦ ∑' r : {r:ℚ // (r:ℝ) < x}, g_9_8_5 r

Exercise 9.8.5(a)

theorem declaration uses `sorry`StrictMonoOn.of_f_9_8_5 : StrictMonoOn f_9_8_5 .univ := by⊢ StrictMonoOn f_9_8_5 Set.univ
  sorryAll goals completed! 🐙

Exercise 9.8.5(b)

theorem declaration uses `sorry`ContinuousAt.of_f_9_8_5' (r:ℚ) : ¬ ContinuousAt f_9_8_5 r := byr:ℚ⊢ ¬ContinuousAt f_9_8_5 ↑r
  sorryAll goals completed! 🐙

Exercise 9.8.5(c)

theorem declaration uses `sorry`ContinuousAt.of_f_9_8_5 {x:ℝ} (hx: ¬ ∃ r:ℚ, x = r) : ContinuousAt f_9_8_5 x := byx:ℝhx:¬∃ r, x = ↑r⊢ ContinuousAt f_9_8_5 x
  sorryAll goals completed! 🐙

end Chapter9