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 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 _ _ _ _ _ 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! 🐙 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

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! 🐙 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! 🐙 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 a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : MonotoneOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) 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 a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : StrictAntiOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) 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 a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : AntitoneOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) sorryAll goals completed! 🐙 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 end Chapter9