From 3fc293579d9414630275d23da0b7393fa515ab13 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 12 May 2023 19:31:44 -0600 Subject: [PATCH] Add concept of glossary. --- Bookshelf/Apostol/Glossary.tex | 57 ++++++++++++++++++++++++++ Common/Set/Intervals/Partition.lean | 12 ++++++ Common/Set/Intervals/StepFunction.lean | 13 +++--- DocGen4/Output/Index.lean | 17 +++++--- preamble.tex | 17 +++----- 5 files changed, 93 insertions(+), 23 deletions(-) create mode 100644 Bookshelf/Apostol/Glossary.tex diff --git a/Bookshelf/Apostol/Glossary.tex b/Bookshelf/Apostol/Glossary.tex new file mode 100644 index 0000000..69ec110 --- /dev/null +++ b/Bookshelf/Apostol/Glossary.tex @@ -0,0 +1,57 @@ +\documentclass{article} + +\input{../../preamble} + +\newcommand{\lean}[2]{\leanref{../../#1.html\##2}{#2}} + +\begin{document} + +\tableofcontents + +\section{The Concepts of Integral Calculus}% +\label{sec:concepts-integral-calculus} + +\subsection{\defined{Partition}}% +\label{sub:partition} + +Let $[a, b]$ be a closed interval decomposed into $n$ subintervals by inserting + $n - 1$ points of subdivision, say $x_1$, $x_2$, $\ldots$, $x_{n-1}$, subject + only to the restriction + \begin{equation} + \label{sec:partition-eq1} + a < x_1 < x_2 < \cdots < x_{n-1} < b. + \end{equation} +It is convenient to denote the point $a$ itself by $x_0$ and the point $b$ by + $x_n$. +A collection of points satisfying \eqref{sec:partition-eq1} is called a + \textbf{partition} $P$ of $[a, b]$, and we use the symbol + $$P = \{x_0, x_1, \ldots, x_n\}$$ to designate this partition. + +\begin{definition} + + \lean{Common/Set/Intervals/Partition}{Set.Intervals.Partition} + +\end{definition} + +\subsection{\defined{Step Function}}% +\label{sub:step-function} + +A function $s$, whose domain is a closed interval $[a, b]$, is called a step + function if there is a \nameref{sub:partition} $P = \{x_0, x_1, \ldots, x_n\}$ + of $[a b]$ such that $s$ is constant on each open subinterval of $P$. +That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$ + such that $$s(x) = s_k \quad\text{if}\quad x_{k-1} < x < x_k.$$ +Step functions are sometimes called piecewise constant functions. + +\vspace{8pt} +\noindent +\textit{Note:} At each of the endpoints $x_{k-1}$ and $x_k$ the function must + have some well-defined value, but this need not be the same as $s_k$. + +\begin{definition} + + \lean{Common/Set/Intervals/StepFunction}{Set.Intervals.StepFunction} + +\end{definition} + +\end{document} diff --git a/Common/Set/Intervals/Partition.lean b/Common/Set/Intervals/Partition.lean index ca297bb..56a189a 100644 --- a/Common/Set/Intervals/Partition.lean +++ b/Common/Set/Intervals/Partition.lean @@ -69,6 +69,12 @@ theorem right_ge_mem_self [Preorder α] [@DecidableRel α LT.lt] (p : Partition α) : ∀ x ∈ p, x ≤ p.b := by sorry +/-- +The closed interval determined by the endpoints of the `Partition`. +-/ +abbrev toIcc [Preorder α] [@DecidableRel α LT.lt] + (p : Partition α) := Set.Icc p.a p.b + /- Return the closed subintervals determined by the `Partition`. -/ @@ -76,6 +82,12 @@ def closedSubintervals [Preorder α] [@DecidableRel α LT.lt] (p : Partition α) : List (Set α) := p.toList.pairwise (fun x₁ x₂ => Icc x₁ x₂) +/-- +The open interval determined by the endpoints of the `Partition`. +-/ +abbrev toIoo [Preorder α] [@DecidableRel α LT.lt] + (p : Partition α) := Set.Ioo p.a p.b + /- Return the open subintervals determined by the `Partition`. -/ diff --git a/Common/Set/Intervals/StepFunction.lean b/Common/Set/Intervals/StepFunction.lean index 0387616..53d33cc 100644 --- a/Common/Set/Intervals/StepFunction.lean +++ b/Common/Set/Intervals/StepFunction.lean @@ -8,20 +8,19 @@ Characterization of step functions. namespace Set.Intervals +open Partition + /-- A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction` if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is constant on each open subinterval of `P`. -/ structure StepFunction (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where - /- A partition of some closed interval `[a, b]`. -/ - partition : Partition α - /-- A function whose domain is a closed interval `[a, b]`. -/ - function : ∀ x ∈ Icc partition.a partition.b, α - /-- Ensure the function is constant on each open subinterval of `p`. -/ + p : Partition α + toFun : ∀ x ∈ p.toIcc, α const_open_subintervals : - ∀ (hI : I ∈ partition.openSubintervals), ∃ c : α, ∀ (hy : y ∈ I), - function y (Partition.mem_open_subinterval_mem_closed_interval hI hy) = c + ∀ (hI : I ∈ p.openSubintervals), ∃ c : α, ∀ (hy : y ∈ I), + toFun y (mem_open_subinterval_mem_closed_interval hI hy) = c namespace StepFunction diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index 24344f5..8bdf79d 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -37,13 +37,20 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <| status: