Documentation

Analysis.Section_11_3

Аналіз I, Глава 11.3 #

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.

source
@[reducible, inline]
abbrev Chapter11.MajorizesOn (g f : ℝ → ℝ) (I : BoundedInterval) :
Prop

Визначення 11.3.1 (Majorization of functions)

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Chapter11.MinorizesOn (g f : ℝ → ℝ) (I : BoundedInterval) :
    Prop
    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev Chapter11.upper_integral (f : ℝ → ℝ) (I : BoundedInterval) :
      ℝ

      Визначення 11.3.2 (Uppper and lower Riemann integrals )

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev Chapter11.lower_integral (f : ℝ → ℝ) (I : BoundedInterval) :
        ℝ
        Equations
        Instances For
          source
          theorem Chapter11.integral_bounds {f : ℝ → ℝ} {I : BoundedInterval} {M : ℝ} (h : ∀ x ∈ match I with | BoundedInterval.Ioo a b => Set.Ioo a b | BoundedInterval.Icc a b => Set.Icc a b | BoundedInterval.Ioc a b => Set.Ioc a b | BoundedInterval.Ico a b => Set.Ico a b, |f x| ≤ M) :
          -M * I.length ≤ lower_integral f I ∧ lower_integral f I ≤ upper_integral f I ∧ upper_integral f I ≤ M * I.length ∧ (∀ (g : ℝ → ℝ), MajorizesOn g f I ∧ PiecewiseConstantOn g I → upper_integral f I ≤ PiecewiseConstantOn.integ g I) ∧ ∀ (h : ℝ → ℝ), MinorizesOn h f I ∧ PiecewiseConstantOn h I → PiecewiseConstantOn.integ h I ≤ lower_integral f I

          Лема 11.3.3, augmented with some additional useful facts

          source
          @[reducible, inline]
          noncomputable abbrev Chapter11.integ (f : ℝ → ℝ) (I : BoundedInterval) :
          ℝ

          Визначення 11.3.4 (Riemann integral) As we permit junk values, the simplest definition for the Riemann integral is the upper integral.

          Equations
          Instances For
            source
            @[reducible, inline]
            noncomputable abbrev Chapter11.integrable (f : ℝ → ℝ) (I : BoundedInterval) :
            Prop
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Chapter11.integ_of_piecewise_const {f : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) :
              integrable f I ∧ integ f I = PiecewiseConstantOn.integ f I

              Лема 11.3.7 / Вправа 11.3.3

              source
              theorem Chapter11.integ_on_subsingleton {f : ℝ → ℝ} {I : BoundedInterval} (hI : I.length = 0) :
              integrable f I ∧ integ f I = 0

              Ремарка 11.3.8

              source
              @[reducible, inline]
              noncomputable abbrev Chapter11.upper_riemann_sum (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) :
              ℝ

              Визначення 11.3.9 (Riemann sums). The restriction to positive length J is not needed thanks to various junk value conventions.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[reducible, inline]
                noncomputable abbrev Chapter11.lower_riemann_sum (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) :
                ℝ
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Chapter11.upper_riemann_sum_le {f g : ℝ → ℝ} {I : BoundedInterval} (P : Partition I) (hf : Chapter9.BddOn f (match I with | BoundedInterval.Ioo a b => Set.Ioo a b | BoundedInterval.Icc a b => Set.Icc a b | BoundedInterval.Ioc a b => Set.Ioc a b | BoundedInterval.Ico a b => Set.Ico a b)) (hgf : MajorizesOn g f I) (hg : PiecewiseConstantOn g I) :
                  upper_riemann_sum f P ≤ integ g I

                  Лема 11.3.11 / Вправа 11.3.4

                  source
                  theorem Chapter11.lower_riemann_sum_ge {f h : ℝ → ℝ} {I : BoundedInterval} (P : Partition I) (hf : Chapter9.BddOn f (match I with | BoundedInterval.Ioo a b => Set.Ioo a b | BoundedInterval.Icc a b => Set.Icc a b | BoundedInterval.Ioc a b => Set.Ioc a b | BoundedInterval.Ico a b => Set.Ico a b)) (hfh : MinorizesOn h f I) (hg : PiecewiseConstantOn h I) :
                  integ h I ≤ lower_riemann_sum f P
                  source
                  theorem Chapter11.upper_integ_eq_inf_upper_sum {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f (match I with | BoundedInterval.Ioo a b => Set.Ioo a b | BoundedInterval.Icc a b => Set.Icc a b | BoundedInterval.Ioc a b => Set.Ioc a b | BoundedInterval.Ico a b => Set.Ico a b)) :
                  upper_integral f I = sInf (Set.range fun (P : Partition I) => upper_riemann_sum f P)

                  Твердження 11.3.12 / Вправа 11.3.5

                  source
                  theorem Chapter11.lower_integ_eq_sup_lower_sum {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f (match I with | BoundedInterval.Ioo a b => Set.Ioo a b | BoundedInterval.Icc a b => Set.Icc a b | BoundedInterval.Ioc a b => Set.Ioc a b | BoundedInterval.Ico a b => Set.Ico a b)) :
                  lower_integral f I = sSup (Set.range fun (P : Partition I) => lower_riemann_sum f P)
                  source
                  theorem Chapter11.MajorizesOn.trans {f g h : ℝ → ℝ} {I : BoundedInterval} (hfg : MajorizesOn f g I) (hgh : MajorizesOn g h I) :
                  MajorizesOn f h I

                  Вправа 11.3.1

                  source
                  theorem Chapter11.MajorizesOn.anti_symm {f g : ℝ → ℝ} {I : BoundedInterval} (x : ℝ) :
                  (x ∈ match I with | BoundedInterval.Ioo a b => Set.Ioo a b | BoundedInterval.Icc a b => Set.Icc a b | BoundedInterval.Ioc a b => Set.Ioc a b | BoundedInterval.Ico a b => Set.Ico a b) → (f x = g x ↔ MajorizesOn f g I ∧ MajorizesOn g f I)

                  Вправа 11.3.1

                  source
                  def Chapter11.MajorizesOn.of_add :
                  Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f + h) (g + h) I)

                  Вправа 11.3.2

                  Equations
                  Instances For
                    source
                    def Chapter11.MajorizesOn.of_mul :
                    Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f * h) (g * h) I)
                    Equations
                    Instances For
                      source
                      def Chapter11.MajorizesOn.of_smul :
                      Decidable (∀ (f g : ℝ → ℝ) (c : ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (c • f) (c • g) I)
                      Equations
                      Instances For