Documentation

Analysis.Section_9_8

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

Definition 9.8.1

source
theorem Chapter9.StrictMono.iff {X : Set ℝ} (f : ℝ → ℝ) :
StrictMonoOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x
source
theorem Chapter9.AntitoneOn.iff {X : Set ℝ} (f : ℝ → ℝ) :
AntitoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x
source
theorem Chapter9.StrictAntitone.iff {X : Set ℝ} (f : ℝ → ℝ) :
StrictAntiOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x
source
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

source
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

source
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
source
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
source
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
source
theorem Chapter9.BddOn.of_monotone {a b : ℝ} {f : ℝ → ℝ} (hf : MonotoneOn f (Set.Icc a b)) :
BddOn f (Set.Icc a b)
source
theorem Chapter9.BddOn.of_antitone {a b : ℝ} {f : ℝ → ℝ} (hf : AntitoneOn f (Set.Icc a b)) :
BddOn f (Set.Icc a b)
source
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

source
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
source
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
source
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
source
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

source
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 (without continuity)

Equations
Instances For
    source
    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 (without strict monotonicity)

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev Chapter9.q_9_8_5 :
      ℕ ≃ ℚ

      An equivalence between the natural numbers and the rationals.

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev Chapter9.g_9_8_5 :
        ℚ → ℝ
        Equations
        Instances For
          source
          @[reducible, inline]
          noncomputable abbrev Chapter9.f_9_8_5 :
          ℝ → ℝ
          Equations
          Instances For
            source
            theorem Chapter9.StrictMonoOn.of_f_9_8_5 :
            StrictMonoOn f_9_8_5 Set.univ

            Exercise 9.8.5(a)

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

            Exercise 9.8.5(b)

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

            Exercise 9.8.5(c)