Lebesgue積分講義ノート

1.2. Darbouxの上積分と下積分による定義🔗

Definition1.2.1
uses 1used by 1✓L∃∀N
Tagsleanok

Darbouxの上和と下和. 関数f : [a,b] \to \RRの区間[a,b]の分割\mathcal{P}に対するDarbouxの上和と下和（過剰和と不足和）は，分割\mathcal{P}の各区間[x_{i-1}, x_i]におけるfの上限と下限を用いて定義される． すなわち，

\begin{aligned} U(f,\mathcal{P}) &:= \sum_{i=1}^n (x_i - x_{i-1}) \sup_{x \in [x_{i-1}, x_i]} f(x), \\ L(f,\mathcal{P}) &:= \sum_{i=1}^n (x_i - x_{i-1}) \inf_{x \in [x_{i-1}, x_i]} f(x). \end{aligned}

Lean code for Definition1.2.1●4 definitions
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.intervalSup (f : ℝ → ℝ) (u v : ℝ) : ℝ
    def NoteKsk.Chapter01.intervalSup (f : ℝ → ℝ)
  (u v : ℝ) : ℝ

    Definition body

    def intervalSup (f : ℝ → ℝ) (u v : ℝ) : ℝ :=
  sSup (f '' Set.Icc u v)
    Supremum of `f` on a closed subinterval.

This is intentionally an extended-real-free lecture definition using mathlib's
totalized `sSup`; theorem statements supply the boundedness hypotheses needed
for the usual Darboux interpretation.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.intervalInf (f : ℝ → ℝ) (u v : ℝ) : ℝ
    def NoteKsk.Chapter01.intervalInf (f : ℝ → ℝ)
  (u v : ℝ) : ℝ

    Definition body

    def intervalInf (f : ℝ → ℝ) (u v : ℝ) : ℝ :=
  sInf (f '' Set.Icc u v)
    Infimum of `f` on a closed subinterval.

As with `intervalSup`, boundedness hypotheses are supplied by theorem
statements rather than by the definition itself.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxUpperSum (f : ℝ → ℝ)
  (P : NoteKsk.Chapter01.IntervalPartition) : ℝ
    def NoteKsk.Chapter01.darbouxUpperSum
  (f : ℝ → ℝ)
  (P :
    NoteKsk.Chapter01.IntervalPartition) :
  ℝ

    Definition body

    def darbouxUpperSum (f : ℝ → ℝ) (P : IntervalPartition) : ℝ :=
  (P.subintervals.map fun uv => intervalSup f uv.1 uv.2 * (uv.2 - uv.1)).sum
    Darboux upper sum.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxLowerSum (f : ℝ → ℝ)
  (P : NoteKsk.Chapter01.IntervalPartition) : ℝ
    def NoteKsk.Chapter01.darbouxLowerSum
  (f : ℝ → ℝ)
  (P :
    NoteKsk.Chapter01.IntervalPartition) :
  ℝ

    Definition body

    def darbouxLowerSum (f : ℝ → ℝ) (P : IntervalPartition) : ℝ :=
  (P.subintervals.map fun uv => intervalInf f uv.1 uv.2 * (uv.2 - uv.1)).sum
    Darboux lower sum.

Darbouxの上和と下和は（上限と下限なので）必ずしもRiemann和と一致するわけではないが，常に

L(f,\mathcal{P}) \leq S(f,\mathcal{P},t) \leq U(f,\mathcal{P})

が成り立つ．

Definition1.2.2
uses 1used by 1✓L∃∀N
Tagsleanok

Darbouxの上積分と下積分. 関数f : [a,b] \to \mathbb{R}の区間[a,b]の分割\mathcal{P}に対するDarboux上積分（下積分）は，上和（下和）の分割\mathcal{P}に関する下限（上限）として定義される． すなわち，

\begin{aligned} \uint{a}{b} f(x) dx &:= \inf_{\mathcal{P}} U(f,\mathcal{P}), \\ \lint{a}{b} f(x) dx &:= \sup_{\mathcal{P}} L(f,\mathcal{P}). \end{aligned}

Lean code for Definition1.2.2●4 definitions
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxUpperValues (f : ℝ → ℝ) (a b : ℝ) : Set ℝ
    def NoteKsk.Chapter01.darbouxUpperValues
  (f : ℝ → ℝ) (a b : ℝ) : Set ℝ

    Definition body

    def darbouxUpperValues (f : ℝ → ℝ) (a b : ℝ) : Set ℝ :=
  {U | ∃ P : IntervalPartition, P.a = a ∧ P.b = b ∧ U = darbouxUpperSum f P}
    Upper Darboux sums over all partitions of `[a,b]`.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxLowerValues (f : ℝ → ℝ) (a b : ℝ) : Set ℝ
    def NoteKsk.Chapter01.darbouxLowerValues
  (f : ℝ → ℝ) (a b : ℝ) : Set ℝ

    Definition body

    def darbouxLowerValues (f : ℝ → ℝ) (a b : ℝ) : Set ℝ :=
  {L | ∃ P : IntervalPartition, P.a = a ∧ P.b = b ∧ L = darbouxLowerSum f P}
    Lower Darboux sums over all partitions of `[a,b]`.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxUpperIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ
    def NoteKsk.Chapter01.darbouxUpperIntegral
  (f : ℝ → ℝ) (a b : ℝ) : ℝ

    Definition body

    def darbouxUpperIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ :=
  sInf (darbouxUpperValues f a b)
    Darboux upper integral: the infimum of upper sums.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxLowerIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ
    def NoteKsk.Chapter01.darbouxLowerIntegral
  (f : ℝ → ℝ) (a b : ℝ) : ℝ

    Definition body

    def darbouxLowerIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ :=
  sSup (darbouxLowerValues f a b)
    Darboux lower integral: the supremum of lower sums.
Definition1.2.3
uses 1used by 1✓L∃∀N
Tagsleanok

Darboux可積分. 関数f : [a,b] \to \mathbb{R}が区間[a,b]上でDarboux可積分であるとは，任意の\varepsilon > 0に対して，区間[a,b]の分割\mathcal{P}が存在して，

U(f,\mathcal{P}) - L(f,\mathcal{P}) < \varepsilon

が成り立つことをいう．このとき，Darboux上積分と下積分は等しくなり，この値を関数fの区間[a,b]に対するDarboux積分と呼び， \dint_a^b f(x) dx と表す．

Lean code for Definition1.2.3●2 definitions
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.DarbouxIntegrableOn (f : ℝ → ℝ) (a b : ℝ) : Prop
    def NoteKsk.Chapter01.DarbouxIntegrableOn
  (f : ℝ → ℝ) (a b : ℝ) : Prop

    Definition body

    def DarbouxIntegrableOn (f : ℝ → ℝ) (a b : ℝ) : Prop :=
  darbouxUpperIntegral f a b = darbouxLowerIntegral f a b
    Darboux integrability on `[a,b]`.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.darbouxIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ
    def NoteKsk.Chapter01.darbouxIntegral
  (f : ℝ → ℝ) (a b : ℝ) : ℝ

    Definition body

    def darbouxIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ :=
  darbouxUpperIntegral f a b

/-! ## Auxiliary predicates for deferred statements -/
    Darboux integral, represented by the upper integral.

単にDarboux上積分と下積分が等しくなることをもってDarboux可積分と定義することもある．

Theorem1.2.4
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1!L∃∀N
Tagsnotready

Darboux. 関数f:[a,b] \to \mathbb{R}が区間[a,b]上でRiemann可積分であることとDarboux可積分であることは同値である． さらに，このときRiemann積分とDarboux積分は等しい．

\int_a^b f(x) dx = \uint{a}{b} f(x) dx = \lint{a}{b} f(x) dx = \dint_a^b f(x) dx.

Lean code for Theorem1.2.4●2 declarations, 2 missing