Lebesgue積分講義ノート

1.1. Riemann和による定義🔗

Definition1.1.1
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 1.1.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

区間の分割. 区間[a,b]の分割\mathcal{P}は，区間[a,b]を有限個の区間へ分割したものであり，

\mathcal{P} : a = x_0 < x_1 < \cdots < x_n = b

と表される．分割の大きさを

|\mathcal{P}| := \max_{1 \leq i \leq n} (x_i - x_{i-1})

と定義する．

Lean code for Definition1.1.1●5 definitions
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.IsValidPointList (a b : ℝ) (points : List ℝ) : Prop
    def NoteKsk.Chapter01.IsValidPointList
  (a b : ℝ) (points : List ℝ) : Prop

    Definition body

    def IsValidPointList (a b : ℝ) (points : List ℝ) : Prop :=
  a ≤ b ∧ points.Pairwise (fun x y => x < y) ∧ ∀ x ∈ points, a < x ∧ x < b
    Interior points of a partition of `[a,b]`, strictly increasing and inside the interval.
  • structure(4 fields)defined in NoteKsk/«01riemann».lean
    complete
    structure NoteKsk.Chapter01.IntervalPartition : Type
    structure NoteKsk.Chapter01.IntervalPartition : Type
    A finite partition of `[a,b]`, stored by its interior division points.

    Fields

    a : ℝ
    b : ℝ
    points : List ℝ
    valid : NoteKsk.Chapter01.IsValidPointList self.a self.b self.points
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.IntervalPartition.vertices
  (P : NoteKsk.Chapter01.IntervalPartition) : List ℝ
    def NoteKsk.Chapter01.IntervalPartition.vertices
  (P :
    NoteKsk.Chapter01.IntervalPartition) :
  List ℝ

    Definition body

    def vertices (P : IntervalPartition) : List ℝ :=
  P.a :: (P.points ++ [P.b])
    Vertices of the partition, including the endpoints.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.IntervalPartition.subintervals
  (P : NoteKsk.Chapter01.IntervalPartition) : List (ℝ × ℝ)
    def NoteKsk.Chapter01.IntervalPartition.subintervals
  (P :
    NoteKsk.Chapter01.IntervalPartition) :
  List (ℝ × ℝ)

    Definition body

    def subintervals (P : IntervalPartition) : List (ℝ × ℝ) :=
  P.vertices.zip P.vertices.tail
    Adjacent subinterval endpoints of the partition.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.mesh (P : NoteKsk.Chapter01.IntervalPartition) : ℝ
    def NoteKsk.Chapter01.mesh
  (P :
    NoteKsk.Chapter01.IntervalPartition) :
  ℝ

    Definition body

    def mesh (P : IntervalPartition) : ℝ :=
  (P.subintervals.map (fun uv => |uv.2 - uv.1|)).foldl max 0
    Mesh size of a partition: the maximum adjacent interval length.
Definition1.1.2
uses 1used by 1✓L∃∀N
Tagsleanok

Riemann和. 関数f : [a,b] \to \mathbb{R}の区間[a,b]の分割\mathcal{P}に対するRiemann和は，分割\mathcal{P}の各区間[x_{i-1}, x_i]において，関数fの値を評価する点t_i \in [x_{i-1}, x_i]を選び，それらの値を足し合わせたものである． すなわち，

S(f,\mathcal{P},t) := \sum_{i=1}^n f(t_i)(x_i - x_{i-1}),

ここで，t = (t_1, t_2, \ldots, t_n)は分割\mathcal{P}に対する評価点の列である．

Lean code for Definition1.1.2●2 definitions
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.IntervalPartition.IsTagged
  (P : NoteKsk.Chapter01.IntervalPartition) (tags : ℕ → ℝ) : Prop
    def NoteKsk.Chapter01.IntervalPartition.IsTagged
  (P :
    NoteKsk.Chapter01.IntervalPartition)
  (tags : ℕ → ℝ) : Prop

    Definition body

    def IsTagged (P : IntervalPartition) (tags : ℕ → ℝ) : Prop :=
  ∀ item ∈ P.subintervals.zipIdx, tags item.2 ∈ Set.Icc item.1.1 item.1.2
    A tag function chooses one point in each subinterval, indexed from the left.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.riemannSum (f : ℝ → ℝ)
  (P : NoteKsk.Chapter01.IntervalPartition) (tags : ℕ → ℝ) : ℝ
    def NoteKsk.Chapter01.riemannSum (f : ℝ → ℝ)
  (P :
    NoteKsk.Chapter01.IntervalPartition)
  (tags : ℕ → ℝ) : ℝ

    Definition body

    def riemannSum (f : ℝ → ℝ) (P : IntervalPartition) (tags : ℕ → ℝ) : ℝ :=
  (P.subintervals.mapIdx fun i uv => f (tags i) * (uv.2 - uv.1)).sum
    Riemann sum for a tagged partition.
Definition1.1.3
uses 1
Used by 9
Reverse dependency previews
Preview
Theorem 1.2.4
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

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

|\mathcal P| < \delta \implies |S(f,\mathcal{P},t) - I| < \varepsilon

が成り立つことをいう．Iを関数fの区間[a,b]に対するRiemann積分と呼び， \int_a^b f(x) dx と表す．

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

    Definition body

    def HasRiemannIntegralOn (f : ℝ → ℝ) (a b I : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ P tags,
    P.a = a → P.b = b → P.IsTagged tags → mesh P < δ → |riemannSum f P tags - I| < ε
    `f` has Riemann integral `I` on `[a,b]`.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.RiemannIntegrableOn (f : ℝ → ℝ) (a b : ℝ) : Prop
    def NoteKsk.Chapter01.RiemannIntegrableOn
  (f : ℝ → ℝ) (a b : ℝ) : Prop

    Definition body

    def RiemannIntegrableOn (f : ℝ → ℝ) (a b : ℝ) : Prop :=
  ∃ I, HasRiemannIntegralOn f a b I
    Riemann integrability on `[a,b]`.
  • defdefined in NoteKsk/«01riemann».lean
    complete
    def NoteKsk.Chapter01.riemannIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ
    def NoteKsk.Chapter01.riemannIntegral
  (f : ℝ → ℝ) (a b : ℝ) : ℝ

    Definition body

    def riemannIntegral (f : ℝ → ℝ) (a b : ℝ) : ℝ :=
  by
    classical
    exact if h : ∃ I, HasRiemannIntegralOn f a b I then Classical.choose h else 0

/-! ## Darboux sums -/
    The Riemann integral, when it exists; `0` outside the integrable case.

つまり，関数fのRiemann積分とは，Riemann和S(f,\mathcal{P},t)の細分に関する極限である．

\lim_{|\mathcal{P}|\to 0} S(f,\mathcal{P},t) = \int_a^b f(x) dx.

特に，関数fが（区分的）連続である場合は，Riemann可積分であることが知られている． また，非有界な関数はRiemann可積分でないことも知られている（なぜか）．