Riemann integral

StructurePartition of an interval#✓fully proved

For real numbers \(a\) and \(b\), a partition of the closed interval \([a, b]\) consists of a natural number \(n\), the number of subintervals, together with \(n + 1\) points forming a strictly increasing sequence \(a = x_0 < x_1 < \dots < x_n = b\).

structure Partition (a b : ℝ) where
  n : ℕ
  points : Fin (n + 1) → ℝ
  ordered : StrictMono points
  first : points 0 = a
  last : points (Fin.last n) = b

Used by 61

Used byContinuity of P1 functions · Nodal vectors with zero boundary values · Quadratic form of the stiffness matrix · Slope of a P1 function on a mesh element · Element vector of the stiffness assembly · Weak form of the classical solution for P1 test functions · Stiffness matrix is the Gram matrix of the hat functions · Energy pairing with a P1 function via nodal differences · Energy form of two P1 functions · Best approximation · Energy error estimate · Interpolation estimate · Element-wise energy of a function minus a P1 function · Galerkin orthogonality · Derivative of a P1 function inside an element · Hat function of a mesh node · Interior hat functions lie in the P1 space · Integral over the unit interval as a sum over elements · L² error estimate · Nodal interpolant of a function · Solution of the Galerkin system · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution · Load vector of the P1 method · Characterization of membership in the P1 space · Continuous piecewise linear function with given nodal values · In one dimension the Galerkin solution is the nodal interpolant · P1 functions are linear on each element · Linear map from nodal values to P1 functions · P1 functions interpolate their nodal values · P1 finite element space with zero boundary values · Clamped ramp function of a mesh element · Energy error estimate for the P1 Galerkin solution · Assembled stiffness matrix of the P1 method · Off-diagonal stiffness entry of an element · Tridiagonality of the stiffness matrix · Diagonal stiffness entry at an interior node · Length of a mesh element · Element lengths are bounded by the mesh size · Mesh elements have positive length · Endpoints of a partition are ordered · Common refinement of two tagged partitions · Refinement of a partition · Tagged-refinement data · Subinterval lengths are at most the mesh · Mesh of a partition · The mesh is positive on a nondegenerate interval · A partition of a nondegenerate interval has a subinterval · Refinements carry tagged-refinement data · Points of a partition · Riemann sum · Riemann sum of a constant function · Riemann sum regrouped over a refinement · Riemann sum over a trivial partition · Riemann sums of two partitions with a common refinement · Riemann sums under refinement · Riemann sums under refinement, given refinement data · Subintervals of a partition have nonnegative length · Subinterval lengths of a partition telescope · Tags of a tagged partition lie in the interval · Tagged partition

StructureTagged partition#✓fully proved

A tagged partition of \([a, b]\) is a partition \(a = x_0 < x_1 < \cdots < x_n = b\) of \([a, b]\) together with a choice of a tag \(\xi_k \in [x_{k-1}, x_k]\) in each subinterval, for \(k = 1, \dots, n\).

structure TaggedPartition (a b : ℝ) extends Partition a b where
  tags : Fin n → ℝ
  tag_mem : ∀ i : Fin n, points i.castSucc ≤ tags i ∧ tags i ≤ points i.succ

Uses 1 · Used by 11

Statement usesPartition of an interval

Used byCommon refinement of two tagged partitions · Tagged-refinement data · Refinements carry tagged-refinement data · Riemann sum · Riemann sum of a constant function · Riemann sum regrouped over a refinement · Riemann sum over a trivial partition · Riemann sums of two partitions with a common refinement · Riemann sums under refinement · Riemann sums under refinement, given refinement data · Tags of a tagged partition lie in the interval

DefinitionMesh of a partition#✓fully proved

The mesh (also called the norm) of a partition \(a = x_0 < x_1 < \dots < x_n = b\) of \([a, b]\) is the maximum subinterval length \(\max_{1 \le k \le n} (x_k - x_{k-1})\) when \(n \ge 1\), and \(0\) when \(n = 0\).

noncomputable def Partition.mesh (P : Partition a b) : ℝ :=
  if h : P.n = 0 then 0
  else
    Finset.sup' (Finset.univ (α := Fin P.n))
      (Finset.univ_nonempty_iff.mpr ⟨⟨0, Nat.pos_of_ne_zero h⟩⟩)
      (fun i => P.points i.succ - P.points i.castSucc)

Uses 1 · Used by 10

Statement usesPartition of an interval

Used byEnergy error estimate · Interpolation estimate · L² error estimate · Energy error estimate for the P1 Galerkin solution · Element lengths are bounded by the mesh size · Subinterval lengths are at most the mesh · The mesh is positive on a nondegenerate interval · Riemann sums of two partitions with a common refinement · Riemann sums under refinement · Riemann sums under refinement, given refinement data

DefinitionPoints of a partition#✓fully proved

The point set of a partition \(a = x_0 < x_1 < \dots < x_n = b\) of \([a, b]\) is the set of its points \(x_0, x_1, \dots, x_n\).

def Partition.pointSet (P : Partition a b) : Set ℝ :=
  Set.range P.points

Uses 1 · Used by 1

Statement usesPartition of an interval

Used byRefinement of a partition

DefinitionRefinement of a partition#✓fully proved

For partitions \(P\) and \(Q\) of \([a, b]\), \(Q\) is a refinement of \(P\) when every point of \(P\) is a point of \(Q\), that is, when the point set of \(P\) is contained in the point set of \(Q\).

def Partition.IsRefinement (Q P : Partition a b) : Prop :=
  P.pointSet ⊆ Q.pointSet

Uses 2 · Used by 3

Statement usesPartition of an interval · Points of a partition

Used byCommon refinement of two tagged partitions · Refinements carry tagged-refinement data · Riemann sums under refinement

DefinitionRiemann sum#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and let \(T\) be a tagged partition of \([a, b]\), with points \(a = x_0 < x_1 < \cdots < x_n = b\) and tags \(\xi_k \in [x_{k-1}, x_k]\) for \(k = 1, \dots, n\). The Riemann sum of \(f\) with respect to \(T\) is \(S_f(x, \xi) = \sum_{k=1}^{n} f(\xi_k)\,(x_k - x_{k-1})\) (an empty sum, equal to \(0\), when \(n = 0\)).

noncomputable def riemannSum (f : ℝ → ℝ) (T : TaggedPartition a b) : ℝ :=
  ∑ i : Fin T.n, f (T.tags i) * (T.points i.succ - T.points i.castSucc)

Uses 2 · Used by 6

Statement usesPartition of an interval · Tagged partition

Used byRiemann sum of a constant function · Riemann sum regrouped over a refinement · Riemann sum over a trivial partition · Riemann sums of two partitions with a common refinement · Riemann sums under refinement · Riemann sums under refinement, given refinement data

LemmaEndpoints of a partition are ordered#✓fully proved

If \(a, b \in \mathbb{R}\) and the interval \([a, b]\) has a partition, then \(a \le b\).

lemma Partition.a_le_b (P : Partition a b) : a ≤ b

Uses 1

Statement usesPartition of an interval

LemmaA partition of a nondegenerate interval has a subinterval#✓fully proved

If \(a < b\), then every partition \(a = x_0 < x_1 < \dots < x_n = b\) of \([a, b]\) has at least one subinterval, that is, \(n \ge 1\).

lemma Partition.n_pos_of_lt (hab : a < b) (P : Partition a b) : 0 < P.n

Uses 1 · Used by 2

Statement usesPartition of an interval

Used byP1 functions interpolate their nodal values · The mesh is positive on a nondegenerate interval

LemmaThe mesh is positive on a nondegenerate interval#✓fully proved

If \(a < b\), then every partition of \([a, b]\) has strictly positive mesh.

lemma Partition.mesh_pos_of_lt (hab : a < b) (P : Partition a b) :
    0 < P.mesh

Uses 3 · Used by 1

Statement usesPartition of an interval · Mesh of a partition

Proof usesA partition of a nondegenerate interval has a subinterval

Used byEnergy error estimate for the P1 Galerkin solution

LemmaRiemann sum over a trivial partition#✓fully proved

For every function \(f : \mathbb{R} \to \mathbb{R}\) and every tagged partition of \([a, b]\) with no subintervals, the Riemann sum of \(f\) is \(0\), since it is an empty sum.

lemma riemannSum_eq_zero_of_n_eq_zero (f : ℝ → ℝ) (T : TaggedPartition a b)
    (h : T.n = 0) : riemannSum f T = 0

Uses 3

Statement usesPartition of an interval · Tagged partition · Riemann sum

LemmaSubintervals of a partition have nonnegative length#✓fully proved

If \(a = x_0 < x_1 < \cdots < x_n = b\) is a partition of \([a, b]\), then \(x_{i+1} - x_i \ge 0\) for every \(i\) with \(0 \le i < n\).

lemma Partition.succ_sub_castSucc_nonneg (P : Partition a b) (i : Fin P.n) :
    0 ≤ P.points i.succ - P.points i.castSucc

Uses 1 · Used by 1

Statement usesPartition of an interval

Used byRiemann sums under refinement, given refinement data

LemmaSubinterval lengths are at most the mesh#✓fully proved

Let \(a = x_0 < x_1 < \dots < x_n = b\) be a partition of \([a, b]\). Then for every \(i\) with \(0 \le i < n\), the subinterval length \(x_{i+1} - x_i\) is at most the mesh of the partition.

lemma Partition.le_mesh (P : Partition a b) (i : Fin P.n) :
    P.points i.succ - P.points i.castSucc ≤ P.mesh

Uses 2 · Used by 1

Statement usesPartition of an interval · Mesh of a partition

Used byRiemann sums under refinement, given refinement data

LemmaSubinterval lengths of a partition telescope#✓fully proved

If \(a = x_0 < x_1 < \cdots < x_n = b\) is a partition of \([a, b]\), then the lengths of its subintervals sum to the length of the interval: \(\sum_{i=0}^{n-1} (x_{i+1} - x_i) = b - a\).

lemma Partition.sum_sub_eq (P : Partition a b) :
    ∑ i : Fin P.n, (P.points i.succ - P.points i.castSucc) = b - a

Uses 1 · Used by 2

Statement usesPartition of an interval

Used byRiemann sum of a constant function · Riemann sums under refinement, given refinement data

LemmaTags of a tagged partition lie in the interval#✓fully proved

Every tag \(\xi_k\) of a tagged partition of \([a, b]\) lies in \([a, b]\).

lemma TaggedPartition.tag_mem_Icc (T : TaggedPartition a b) (i : Fin T.n) :
    T.tags i ∈ Set.Icc a b

Uses 2 · Used by 1

Statement usesPartition of an interval · Tagged partition

Used byRiemann sums under refinement, given refinement data

LemmaRiemann sum of a constant function#✓fully proved

For every real constant \(c\) and every tagged partition of \([a, b]\), the Riemann sum of the constant function \(x \mapsto c\) equals \(c(b - a)\).

lemma riemannSum_const (c : ℝ) (T : TaggedPartition a b) :
    riemannSum (fun _ => c) T = c * (b - a)

Uses 4

Statement usesTagged partition · Riemann sum

Proof usesPartition of an interval · Subinterval lengths of a partition telescope

LemmaTelescoping over the fibers of an assignment#✓fully proved

Let \(y_0, \dots, y_N\) be real numbers, let \(\varphi : \{0, \dots, m\} \to \{0, \dots, N\}\) be strictly increasing, and let \(\sigma : \{0, \dots, N-1\} \to \{0, \dots, m-1\}\) satisfy \(\varphi(\sigma(j)) \le j < \varphi(\sigma(j) + 1)\) for every \(j < N\). Then for every \(k < m\),

\[\sum_{j < N,\ \sigma(j) = k} (y_{j+1} - y_j) = y_{\varphi(k+1)} - y_{\varphi(k)}.\]

lemma telescope_sum_of_embedding {n'' m : ℕ} (pts : Fin (n'' + 1) → ℝ)
    (φ : Fin (m + 1) → Fin (n'' + 1)) (hφ_strict : StrictMono φ)
    (assign : Fin n'' → Fin m)
    (hassign_spec : ∀ j : Fin n'', (φ (assign j).castSucc).val ≤ j.val ∧
      j.val < (φ (assign j).succ).val)
    (k : Fin m) :
    ∑ j ∈ Finset.univ.filter (fun j => assign j = k),
      (pts j.succ - pts j.castSucc) = pts (φ k.succ) - pts (φ k.castSucc)

Used by 1

Used byRefinements carry tagged-refinement data

StructureTagged-refinement data#✓fully proved

Let \(T\) and \(T'\) be tagged partitions of \([a, b]\) with points \(a = x_0 < \dots < x_n = b\) and \(a = x'_0 < \dots < x'_{n'} = b\) respectively. Tagged-refinement data from \(T\) to \(T'\) consist of a map \(\sigma\) assigning to each index \(j < n'\) an index \(\sigma(j) < n\) such that \(x_{\sigma(j)} \le x'_j\) and \(x'_{j+1} \le x_{\sigma(j)+1}\) for every \(j < n'\) (so the \(j\)-th subinterval of \(T'\) lies in the \(\sigma(j)\)-th subinterval of \(T\)), and such that for every \(k < n\) the lengths assigned to \(k\) add up to its length: \(\sum_{j < n',\ \sigma(j) = k} (x'_{j+1} - x'_j) = x_{k+1} - x_k\). The tags of \(T\) and \(T'\) play no role.

Such data exist whenever every point of \(T\) is a point of \(T'\).

structure TaggedPartition.IsTaggedRefinement (T T' : TaggedPartition a b) where
  assign : Fin T'.n → Fin T.n
  contained_left : ∀ j : Fin T'.n, T.points (assign j).castSucc ≤ T'.points j.castSucc
  contained_right : ∀ j : Fin T'.n, T'.points j.succ ≤ T.points (assign j).succ
  telescope : ∀ k : Fin T.n,
    ∑ j ∈ Finset.univ.filter (fun j => assign j = k),
      (T'.points j.succ - T'.points j.castSucc) = T.points k.succ - T.points k.castSucc

Uses 2 · Used by 6

Statement usesPartition of an interval · Tagged partition

Used byCommon refinement of two tagged partitions · Refinements carry tagged-refinement data · Riemann sum regrouped over a refinement · Riemann sums of two partitions with a common refinement · Riemann sums under refinement · Riemann sums under refinement, given refinement data

TheoremRefinements carry tagged-refinement data#✓fully proved

Let \(T\) and \(T'\) be tagged partitions of \([a, b]\) such that every point of \(T\) is a point of \(T'\). Then tagged-refinement data from \(T\) to \(T'\) exist: an assignment of each subinterval of \(T'\) to a subinterval of \(T\) that contains it, such that for each subinterval of \(T\) the lengths of the subintervals of \(T'\) assigned to it add up to its length.

theorem TaggedPartition.nonempty_isTaggedRefinement_of_isRefinement
    (T T' : TaggedPartition a b) (href : T'.toPartition.IsRefinement T.toPartition) :
    Nonempty (T.IsTaggedRefinement T')

Uses 5 · Used by 2

Statement usesPartition of an interval · Refinement of a partition · Tagged partition · Tagged-refinement data

Proof usesTelescoping over the fibers of an assignment

Used byCommon refinement of two tagged partitions · Riemann sums under refinement

LemmaRiemann sum regrouped over a refinement#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(T\) be a tagged partition of \([a, b]\) with points \(x_0 < \dots < x_n\) and tags \(\xi_0, \dots, \xi_{n-1}\), and let \(T'\) be a tagged partition of \([a, b]\) with points \(x'_0 < \dots < x'_{n'}\), together with tagged-refinement data from \(T\) to \(T'\) assigning to each \(j < n'\) an index \(\sigma(j) < n\). Then the Riemann sum \(S_f(T)\) of \(f\) over \(T\) satisfies

\[S_f(T) = \sum_{j=0}^{n'-1} f(\xi_{\sigma(j)}) \, (x'_{j+1} - x'_j).\]

lemma riemannSum_eq_fiber (f : ℝ → ℝ) (T T' : TaggedPartition a b)
    (href : T.IsTaggedRefinement T') :
    riemannSum f T = ∑ j : Fin T'.n,
      f (T.tags (href.assign j)) * (T'.points j.succ - T'.points j.castSucc)

Uses 4 · Used by 1

Statement usesPartition of an interval · Tagged partition · Tagged-refinement data · Riemann sum

Used byRiemann sums under refinement, given refinement data

TheoremRiemann sums under refinement, given refinement data#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(T\) and \(T'\) be tagged partitions of \([a, b]\) together with tagged-refinement data from \(T\) to \(T'\), and let \(\omega \in \mathbb{R}\) satisfy \(|f(x) - f(y)| \le \omega\) for all \(x, y \in [a, b]\) with \(|x - y| \le \|T\|\), where \(\|T\|\) is the mesh of \(T\). Writing \(S_f(T)\) for the Riemann sum of \(f\) over \(T\), we have \(|S_f(T) - S_f(T')| \le \omega (b - a)\).

theorem riemannSum_sub_le_of_isTaggedRefinement
    (f : ℝ → ℝ) (T T' : TaggedPartition a b) {ω : ℝ}
    (hω : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b,
      |x - y| ≤ T.toPartition.mesh → |f x - f y| ≤ ω)
    (href : T.IsTaggedRefinement T') :
    |riemannSum f T - riemannSum f T'| ≤ ω * (b - a)

Uses 10 · Used by 2

Statement usesPartition of an interval · Mesh of a partition · Tagged partition · Tagged-refinement data · Riemann sum

Proof usesSubinterval lengths are at most the mesh · Subintervals of a partition have nonnegative length · Subinterval lengths of a partition telescope · Tags of a tagged partition lie in the interval · Riemann sum regrouped over a refinement

Used byRiemann sums of two partitions with a common refinement · Riemann sums under refinement

TheoremRiemann sums under refinement#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(T\) and \(T'\) be tagged partitions of \([a, b]\) such that every point of \(T\) is a point of \(T'\), and let \(\omega \in \mathbb{R}\) satisfy \(|f(x) - f(y)| \le \omega\) for all \(x, y \in [a, b]\) with \(|x - y| \le \|T\|\), where \(\|T\|\) is the mesh of \(T\). Writing \(S_f(T)\) for the Riemann sum of \(f\) over \(T\), we have \(|S_f(T) - S_f(T')| \le \omega (b - a)\).

This is Theorem II of the Riemann integral section in oscillation form: an explicit bound \(\omega\) replaces the modulus of continuity, so \(f\) need not be continuous.

theorem riemannSum_sub_le_of_isRefinement
    (f : ℝ → ℝ) (T T' : TaggedPartition a b) {ω : ℝ}
    (hω : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b,
      |x - y| ≤ T.toPartition.mesh → |f x - f y| ≤ ω)
    (href : T'.toPartition.IsRefinement T.toPartition) :
    |riemannSum f T - riemannSum f T'| ≤ ω * (b - a)

Uses 8

Statement usesPartition of an interval · Refinement of a partition · Mesh of a partition · Tagged partition · Riemann sum

Proof usesTagged-refinement data · Refinements carry tagged-refinement data · Riemann sums under refinement, given refinement data

TheoremRiemann sums of two partitions with a common refinement#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and let \(T_1\), \(T_2\) be tagged partitions of \([a, b]\) with meshes \(\|T_1\|\) and \(\|T_2\|\). Suppose \(\omega_1, \omega_2 \in \mathbb{R}\) satisfy, for \(i = 1, 2\), \(|f(x) - f(y)| \le \omega_i\) for all \(x, y \in [a, b]\) with \(|x - y| \le \|T_i\|\). Let \(T''\) be a tagged partition of \([a, b]\) together with tagged-refinement data from \(T_1\) to \(T''\) and from \(T_2\) to \(T''\). Writing \(S_f(T)\) for the Riemann sum of \(f\) over \(T\), we have \(|S_f(T_1) - S_f(T_2)| \le (\omega_1 + \omega_2)(b - a)\).

This is Theorem III of the Riemann integral section in oscillation form: explicit bounds \(\omega_i\) replace the modulus of continuity, so \(f\) need not be continuous.

theorem riemannSum_sub_le_of_commonRefinement
    (f : ℝ → ℝ) (T₁ T₂ : TaggedPartition a b) {ω₁ ω₂ : ℝ}
    (hω₁ : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b,
      |x - y| ≤ T₁.toPartition.mesh → |f x - f y| ≤ ω₁)
    (hω₂ : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b,
      |x - y| ≤ T₂.toPartition.mesh → |f x - f y| ≤ ω₂)
    (T'' : TaggedPartition a b)
    (href₁ : T₁.IsTaggedRefinement T'')
    (href₂ : T₂.IsTaggedRefinement T'') :
    |riemannSum f T₁ - riemannSum f T₂| ≤ (ω₁ + ω₂) * (b - a)

Uses 6

Statement usesPartition of an interval · Mesh of a partition · Tagged partition · Tagged-refinement data · Riemann sum

Proof usesRiemann sums under refinement, given refinement data

TheoremCommon refinement of two tagged partitions#✓fully proved

Let \(a, b\) be real numbers. For any two tagged partitions \(T_1\) and \(T_2\) of \([a, b]\), there is a tagged partition \(T''\) of \([a, b]\) that is a tagged refinement of both \(T_1\) and \(T_2\).

The proof takes for \(T''\) the partition whose points are the union of the points of \(T_1\) and \(T_2\), with each tag at the left endpoint of its subinterval.

theorem TaggedPartition.exists_commonRefinement (T₁ T₂ : TaggedPartition a b) :
    ∃ T'' : TaggedPartition a b,
      Nonempty (T₁.IsTaggedRefinement T'') ∧ Nonempty (T₂.IsTaggedRefinement T'')

Uses 5

Statement usesTagged partition · Tagged-refinement data

Proof usesPartition of an interval · Refinement of a partition · Refinements carry tagged-refinement data

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.