Аналіз I, Глава 9.8

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

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

Визначення 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

Твердження 9.8.3 / Вправа 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

Вправа 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.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 a) (f b)

Вправа 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 a) (f b)

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 a) (f b)

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 a) (f b)

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)

Вправа 9.8.3

def Chapter9.MonotoneOn.exist_inverse_without_continuity {a b : ℝ} (h : a < b) (f : ℝ → ℝ) (hmono : StrictMonoOn f (Set.Icc a b)) : Decidable (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)

Вправа 9.8.4

Equations

• Chapter9.MonotoneOn.exist_inverse_without_continuity h f hmono = sorry

def Chapter9.MonotoneOn.exist_inverse_without_strictmono {a b : ℝ} (h : a < b) (f : ℝ → ℝ) (hcont : ContinuousOn f (Set.Icc a b)) (hmono : MonotoneOn f (Set.Icc a b)) : Decidable (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)

Вправа 9.8.4

Equations

• Chapter9.MonotoneOn.exist_inverse_without_strictmono h f hcont hmono = 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