avewright/proofwiki-math huggingface dataset:
Theorem: Holomorphic Function with Constant Imaginary Part is Constant

Let $D \subseteq \C$ be an open subset of the set of complex numbers $\C$.
Let $f: D \to \C$ be a holomorphic function such that $\map \Im f$ is constant.
Then $f$ is constant.

Proof:
Define $u : \R^2 \to \R$ and $v : \R^2 \to \R$ such that:
:$\map f {x + i y} = \map u {x, y} + i \map v {x, y}$ 
for each $x, y \in \R$.
By hypothesis, $v$ is constant.
Hence from Derivative of Constant, we have:
:$\ds \frac {\partial v} {\partial x} = 0$
and:
:$\ds \frac {\partial v} {\partial y} = 0$
Hence by the Cauchy-Riemann Equations, we have:
:$\ds \frac {\partial u} {\partial x} = 0$
and:
:$\ds \frac {\partial u} {\partial y} = 0$
Applying Zero Derivative implies Constant Function to the function $x \mapsto \map u {x, y}$ for fixed $y \in D$, we obtain:
:$\map u {x, y} = \map F y$ for some $\map F y \in \C$
from the first equation.
We can apply Zero Derivative implies Constant Function to the function $y \mapsto \map u {x, y}$ for fixed $x \in D$ to obtain:
:$\map u {x, y} = \map G x$ for some $\map G x \in \C$
from the second equation. 
We have $\map F y = \map G x$ for each $x, y \in D$. 
Fixing $x_0 \in D$ and setting $c = \map G {x_0}$, we have $\map F y = c$ for all $y \in \C$, and so $u$ is constant. 
Since both $u$ and $v$ are constant, $f$ is constant.
{{qed}}
Category:Holomorphic Functions
Category:Holomorphic Function with Constant Imaginary Part is Constant
2wd54z81wtj7l1cdzszgt9rvyhfu6r0
Theorem: Holomorphic Function with Constant Imaginary Part is Constant/Corollary

Let $D \subseteq \C$ be an open subset of the set of complex numbers $\C$.
Let $f: D \to \C$ be a holomorphic function such that $\map \Re f$ is constant.
Then $f$ is constant.

Proof:
From Combination Theorem for Complex Derivatives: Multiple Rule, $i f$ is holomorphic.
From Imaginary Part of Imaginary Unit times Element of *-Algebra, we have:
:$\map \Im {i f} = \map \Re f$ 
Hence $\map \Im {i f}$ is constant.
From Holomorphic Function with Constant Imaginary Part is Constant, there exists $c \in \C$ such that:
:$i \map f z = c$
for all $z \in D$.
Hence $\map f z = -i c$ for all $z \in D$.
So $f$ is constant.
{{qed}}
Category:Holomorphic Function with Constant Imaginary Part is Constant
jxudqmhrnto0cdiy4uspfy63h7xvo3d
Theorem: Holomorphic Function is Identified by Real or Imaginary Part

Let $D \subseteq \C$ be an open subset of the set of complex numbers $\C$.
Let $f, g : D \to \C$ be holomorphic functions such that either:
:$\map \Re f = \map \Re g$
or:
:$\map \Im f = \map \Im g$
Then $f = g$.

Proof:
From Combination Theorem for Complex Derivatives: Combined Sum Rule, we have:
:$f - g$ is holomorphic.
Suppose first that:
:$\map \Re f = \map \Re g$
Then:
:$\map \Re {f - g} = 0$
Hence from {{Corollary|Holomorphic Function with Constant Imaginary Part is Constant}}, we have $f = g$. 
Suppose also that:
:$\map \Im f = \map \Im g$
Then:
:$\map \Im {f - g} = 0$
Hence from Holomorphic Function with Constant Imaginary Part is Constant, we have $f = g$. 
{{qed}}
Category:Holomorphic Functions
18c0mzugh4xyc6lisd377zd7zy8di7a
Theorem: Completely Prime Filter Induced by Frame Homomorphism Induced by Completely Prime Filter

Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\struct{\mathbf 2, \vee, \wedge, \preceq}$ denote the (Boolean Lattice) $\mathbf 2$.
For every completely prime filter $p$ of $L$, let:
:$\phi_p : L \to \mathbf 2$ be the frame homomorphism defined by:
::<nowiki>$\forall a \in L : \map {\phi_p} a = \begin{cases}
\top & : a \in p\\
\bot & : a \notin p 
\end{cases}$</nowiki>
For every frame homomorphism $\phi : L \to \mathbf 2$, let:
:$p_\phi = \map {\phi^{-1}} \top$ 
where 
:$\map {\phi^{-1}} \top$ denotes the preimage of $\top \in \mathbf 2$ under the mapping $\phi$
which is the completely prime filter of $L$ induced by $\phi$ 
Let $p$ be a completely prime filter of $L$.
Then:
:$p_{\phi_p} = p$

Proof:
From Frame Homomorphism Onto Two Induced by Completely Prime Filter:
:For every completely prime filter $p$ of $L$, $\phi_p : L \to \mathbf 2$ is a frame homomorphism
From Completely Prime Filter Induced by Frame Homomorphism Onto Two:
:For every frame homomorphism $\phi : L \to \mathbf 2$, $p_\phi = \map {\phi^{-1}} \top$ is a completely prime filter of $L$
We have:
{{begin-eqn}}
{{eqn | l = p_{\phi_p}
      | r = \map {\paren{\phi_p}^{-1} } \top
      | c = Definition of $p_{\phi_p}$
}}
{{eqn | r = \set{a \in L : \map {\phi_p} a = \top}
      | c = {{Defof|Inverse Image}}
}}
{{eqn | r = \set{a \in L : a \in p}
      | c = Definition of $\phi_p$
}}
{{eqn | r = p
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Category:Completely Prime Filters
Category:Two (Boolean Lattice)
Category:Frame Homomorphisms
341qtsll5htffl76l8h0ivk9sdqsy44
Theorem: Frame Homomorphism Induced by Completely Prime Filter Induced by Frame Homomorphism

Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\struct{\mathbf 2, \vee, \wedge, \preceq}$ denote the (Boolean Lattice) $\mathbf 2$.
For every frame homomorphism $\phi : L \to \mathbf 2$, let:
:$p_\phi = \map {\phi^{-1}} \top$ 
where 
:$\map {\phi^{-1}} \top$ denotes the preimage of $\top \in \mathbf 2$ under the mapping $\phi$
which is the completely prime filter of $L$ induced by $\phi$ 
For every completely prime filter $p$ of $L$, let:
:$\phi_p : L \to \mathbf 2$ be the frame homomorphism defined by:
::<nowiki>$\forall a \in L : \map {\phi_p} a = \begin{cases}
\top & : a \in p\\
\bot & : a \notin p 
\end{cases}$</nowiki>
Let $\phi : L \to \mathbf 2$ be a frame homomorphism of $L$ into $\mathbf 2$.
Then:
:$\phi_{p_\phi} = \phi$

Proof:
From Completely Prime Filter Induced by Frame Homomorphism Onto Two:
:For every frame homomorphism $\phi : L \to \mathbf 2$, $p_\phi = \map {\phi^{-1}} \top$ is a completely prime filter of $L$
From Frame Homomorphism Onto Two Induced by Completely Prime Filter:
:For every completely prime filter $p$ of $L$, $\phi_p : L \to \mathbf 2$ is a frame homomorphism
We have:
{{begin-eqn}}
{{eqn | q = \forall a \in L 
      | l = \map {\phi_{p_\phi} } a
      | r = \begin{cases} \top & : a \in p_\phi\\ \bot & : a \notin p_\phi \end{cases}
      | c = Definition of $\phi_{p_\phi}$
}}
{{eqn | r = \begin{cases} \top & : a \in \map {\phi^{-1} } \top\\ \bot & : a \notin \map {\phi^{-1} } \top \end{cases}
      | c = Definition of $p_\phi$
}}
{{eqn | r = \begin{cases} \top & : \map \phi a  = \top\\ \bot & : \map \phi a  \ne \top \end{cases}
      | c = {{Defof|Inverse Image}}
}}
{{eqn | r = \begin{cases} \top & : \map \phi a  = \top\\ \bot & : \map \phi a  = \bot \end{cases}
      | c = {{Defof|Two (Boolean Lattice)}}
}}
{{eqn | r = \map \phi a
}}
{{end-eqn}}
From Equality of Mappings:
:$\phi_{p_\phi} = \phi$
{{qed}}
Category:Completely Prime Filters
Category:Two (Boolean Lattice)
Category:Frame Homomorphisms
apm2x7hefeappi36r7n3ali7fw1kvse
Theorem: Completely Prime Filter Induced by Meet Irreducible Induced by Completely Prime Filter

Let $\struct{L, \preceq}$ be a frame.
Let $\top$ denote the greatest element of $L$.
For every completely prime filter $p$ of $L$, let:
:$b_p = \bigvee \set{a \in L : a \notin p}$
where:
:$\bigvee \set{a \in L : a \notin p}$ denotes the supremum of the set $\set{a \in L : a \notin p}$
which is a meet irreducible element not equal to $\top$
For every meet-irreducible element $b$ of $L$  not equal to $\top$, let:
:$p_b = \set{a \in L : a \npreceq b}$
where
:$p_b$ is a completely prime filter of $L$.
Let $p$ be a completely prime filter $p$ of $L$.
Then:
:$p_{b_p} = p$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = p_{b_p}
      | r = \set{a \in L : a \npreceq b_p}
      | c = Definition of $p_{b_p}$
}}
{{eqn | r = \set{a \in L : a \npreceq \bigvee \set{a' \in L : a' \notin p} }
      | c = Definition of $b_p$
}}
{{eqn | r = \set{a \in L : a \npreceq \bigvee \paren{L \setminus p} }
      | c = {{Defof|Set Difference}}
}}
{{eqn | r = \set{a \in L : a \in p}
      | c = Element of Completely Prime Filter iff Does not Precede Supremum of Relative Complement
}}
{{eqn | r = p
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Category:Completely Prime Filters
Category:Meet Irreducible Elements
isu2tssrdbgliffm1aago1cbmieb3hm
Theorem: Meet Irreducible Induced by Completely Prime Filter Induced by Meet Irreducible

Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\top$ denote the greatest element of $L$.
For every meet-irreducible element $b$ of $L$ not equal to $\top$, let:
:$p_b = \set{a \in L : a \npreceq b}$
where
:$p_b$ is a completely prime filter of $L$.
For every completely prime filter $p$ of $L$, let:
:$b_p = \bigvee \set{a \in L : a \notin p}$
where:
:$\bigvee \set{a \in L : a \notin p}$ denotes the supremum of the set $\set{a \in L : a \notin p}$
which is a meet irreducible element not equal to $\top$
Let $b$ be a meet-irreducible element of $L$ not equal to $\top$.
Then:
:$b_{p_b} = b$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = b_{p_b}
      | r = \bigvee \set{a \in L : a \notin p_b} 
      | c = Definition of $b_{p_b}$
}}
{{eqn | r = \bigvee \set{a \in L : a \notin \set{x \in L : x \npreceq b} } 
      | c = Definition of $p_b$
}}
{{eqn | r = \bigvee \set{a \in L : a \in \set{x \in L : x \preceq b} } 
      | c = {{Defof|Relative Complement}}
}}
{{eqn | r = \bigvee \set{a \in L : a \preceq b}
      | c = 
}}
{{eqn | r = b
      | c = Supremum of Lower Closure of Element
}}
{{end-eqn}}
{{qed}}
Category:Completely Prime Filters
Category:Meet Irreducible Elements
48rm8skpc4s8v1pqlykubsj5eoad7a0
Theorem: Existence of Schur Decomposition for Square Matrix

Let $\mathbf A$ be a square matrix.
Then there exists a '''Schur decomposition''' for $\mathbf A$.

Proof:
Proof by induction.
For all $n \in \N_{>0}$, let $\map P n$ represent the proposition:
:All square matrices of order $n$ are unitarily similar to an upper triangular matrix.
That is, they have a Schur decomposition.
{{expand|We need a note somewhere on Definition:Unitary Transformation probably to mention exactly what "unitary similarity" is}}
Theorem: Secant Method can be derived from Newton-Raphson Method

Let $f: \R \to \R$ be a real function which has a root which is to be found.
The '''secant method''' can be derived from the '''Newton-Raphson method'''.

Proof:
{{Recall|Secant Method}}
{{:Definition:Secant Method}}
{{Recall|Newton-Raphson Method}}
{{:Definition:Newton-Raphson Method}}
We note that:
:$\map {f'} {x_n} \approx \dfrac {\map f x - \map f {x_{n - 1} } } {x_n - x_{n - 1} }$
The result follows by substituting for $\map {f'} {x_n}$ in the definition of the Newton-Raphson method.
{{qed}}
Theorem: Complement of Countable Set in Topological Space where Open Neighborhood is Uncountable is Everywhere Dense

Let $\struct {X, \tau}$ be a topological space such that:
:every open set $U \in \tau$ is uncountable.
Let $A \subseteq X$ be countable.
Then $X \setminus A$ is everywhere dense in $\struct {X, \tau}$.

Proof:
Let $a \in X$. 
Let $U$ be an open neighborhood of $a$ in $\struct {X, \tau}$. 
Then $U$ is uncountable by hypothesis.
From Uncountable Set less Countable Set is Uncountable, $U \cap \paren {X \setminus A}$ is uncountable.
In particular, $U \cap \paren {X \setminus A} \ne \O$.
Hence we have $a \in \paren {X \setminus A}^-$, where $\paren {X \setminus A}^-$ denotes the closure of $X \setminus A$.
So $X \setminus \paren {X \setminus A}^-$.
Since we have $\paren {X \setminus A}^-$ automatically, we obtain $\paren {X \setminus A}^- = X$.
So $X \setminus A$ is everywhere dense in $\struct {X, \tau}$. 
{{qed}}
Category:Topological Spaces
Category:Complement of Countable Set in Topological Space where Open Neighborhood is Uncountable is Everywhere Dense
a9czh0c88nftg0gka1k42hbkhjvbl1p
Theorem: Ramanujan's Arctangent Sum

:$\ds \sum_{k \mathop = 0}^{r - 1} \map \arctan {\dfrac 2 {\paren {n + 2 k + 1}^2} } = \map \arctan {\dfrac {2 r} {\paren {n^2 + 2 n r + 1} } }$

Proof:
Recall the Difference of Arctangents:
{{:Difference of Arctangents}}
We first observe:
{{begin-eqn}}
{{eqn | l = \map \arctan {\frac 1 {\paren {n + 2 k} } } - \map \arctan {\frac 1 {\paren {n + 2 k + 2} } }
      | r = \map \arctan {\dfrac {\dfrac 1 {\paren {n + 2 k } } - \dfrac 1 {\paren {n + 2 k + 2} } } {1 + \dfrac 1 {\paren {n + 2 k} \paren {n + 2 k + 2} } } }
      | c = 
}}
{{eqn | r = \map \arctan {\dfrac 2 {\paren {n + 2 k} \paren {n + 2 k + 2} + 1} }
      | c = 
}}
{{eqn | r = \map \arctan {\dfrac 2 {\paren {n + 2 k + 1}^2} }
      | c = 
}}
{{end-eqn}}
We now sum both sides on $k$, from $0 \le k \le r - 1$. 
On the {{LHS}}, we obtain:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{r - 1} \paren {\map \arctan {\frac 1 {\paren {n + 2 k} } } - \map \arctan {\frac 1 {\paren {n + 2 k + 2} } } }
      | r = \map \arctan {\frac 1 n} - \map \arctan {\frac 1 {\paren {n + 2} } } + \map \arctan {\frac 1 {\paren {n + 2} } } - \map \arctan {\frac 1 {\paren {n + 4} } } + \cdots - \map \arctan {\frac 1 {\paren {n + 2 r} } }
      | c = 
}}
{{eqn | r = \map \arctan {\frac 1 n} - \map \arctan {\frac 1 {\paren {n + 2 r} } }
      | c = 
}}
{{end-eqn}}
Therefore:
:$\ds \map \arctan {\frac 1 n} - \map \arctan {\frac 1 {\paren {n + 2 r} } } = \sum_{k \mathop = 0}^{r - 1} \map \arctan {\dfrac 2 {\paren {n + 2 k + 1}^2} } $
Finally:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{r - 1} \map \arctan {\dfrac 2 {\paren {n + 2 k + 1}^2} }
      | r = \map \arctan {\frac 1 n } - \map \arctan {\frac 1 {\paren {n + 2 r} } }
      | c = 
}}
{{eqn | r = \map \arctan {\dfrac {\dfrac 1 n - \dfrac 1 {\paren {n + 2 r} } } {1 + \dfrac 1 n \dfrac 1 {\paren {n + 2 r} } } }
      | c = Difference of Arctangents
}}
{{eqn | r = \map \arctan {\dfrac {2 r} {n \paren {n + 2 r} + 1} }
      | c = simplifying
}}
{{eqn | r = \map \arctan {\dfrac {2 r} {\paren {n^2 + 2 n r + 1} } }
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Srinivasa Ramanujan|cat = Ramanujan}}
Theorem: Real-Valued Continuous Function with Compact Support is Uniformly Continuous

Let $f : \R \to \R$ be a continuous function such that:
:the support $\map \supp f$ is compact.
Then $f$ is uniformly continuous.

Proof:
Since $\map \supp f$ is compact, we can take $\alpha > 0$ such that:
:$\map \supp f \subseteq \closedint {-\alpha} \alpha$
and $\map f x = 0$ for $\cmod x \ge \alpha$. 
From the Heine-Cantor Theorem, $f$ is uniformly continuous on $\closedint {-\alpha - 1} {\alpha + 1}$.
Let $\epsilon > 0$.
Then there exists $\delta' > 0$ such that for $x, y \in \closedint {-\alpha - 1} {\alpha + 1}$ with $\size {x - y} < \delta$ we have:
:$\size {\map f x - \map f y} < \epsilon$ 
Take $\delta = \min \set {\delta', 1/2}$.
Take $x, y \in \R$ with $\size {x - y} < \delta'$. 
If $x, y \in \closedint {-\alpha - 1} {\alpha + 1}$, we have $\size {\map f x - \map f y} < \epsilon$ since $\size {x - y} < \delta' \le \delta$. 
Suppose that $x \in \closedint {-\alpha - 1} {\alpha + 1}$ but $y \in \R \setminus \closedint {-\alpha - 1} {\alpha + 1}$.
Then either $y > \alpha + 1$, in which case $x > \alpha + 1/2$ since $\size {x - y} > 1/2$.
Similarly, if $y < -\alpha - 1$, then $x < -\alpha - 1/2$. 
In either case, $x \in \R \setminus \closedint {-\alpha} \alpha$, so $\map f x = 0$.
Then $\map f x = \map f y = 0$, so $\size {\map f x - \map f y} = 0 < \epsilon$ in this case. 
Hence for all $x, y \in \R$ with $\size {x - y} < \delta$, we have $\size {\map f x - \map f y} < \epsilon$.
So $f$ is uniformly continuous.
{{qed}}
Category:Uniformly Continuous Real Functions
9ujvdxn1m4vj59gpkxzrsy3qu9vw3ta
Theorem: Shannon's Theorem

Let $T$ be a transmission channel subject to random errors.
Then there exists an effective error-correcting code for $T$.

Proof:
{{ProofWanted}}
{{Namedfor|Claude Elwood Shannon|cat = Shannon}}
Theorem: Completely Prime Ideal is Dual of Completely Prime Filter

Let $\struct{L, \preceq}$ be a complete lattice.
Let $K \subseteq L$.
The following are dual statements:
:$K$ is a completely prime filter of $\struct {L, \preceq}$
:$K$ is a completely prime ideal of $\struct {L, \preceq}$

Proof:
By definition of completely prime filter:
:$K$ is a completely prime filter of $\struct {L, \preceq}$
{{iff}}:
:$(1)\quad K$ is a proper filter
:$(2)\quad \forall A \subseteq L: \paren{\wedge A \in K \implies A \cap K \ne \O}$
where $\wedge A$ denotes the infimum of $A$
By the duality principle, the dual of this statement is:
:$(1')\quad K$ is a proper ideal
:$(2')\quad \forall A \subseteq L: \paren{\vee A \in K \implies A \cap K \ne \O}$
where $\vee A$ denotes the supremum of $A$
By definition of completely prime ideal:
:$K$ is a completely prime ideal of $\struct {L, \preceq}$
{{qed}}
Category:Dual Pairs (Order Theory)
Category:Completely Prime Filters
Category:Completely Prime Ideals
gmrui3z1jbxzjlvelpltgpzritbk6ln
Theorem: Ideal is Dual of Filter (Order Theory)

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ be a subset of $S$.
The following are dual statements:
:$T$ is a filter of $\struct {S, \preceq}$
:$T$ is an ideal of $\struct {S, \preceq}$

Proof:
By definition of filter:
:$T$ is a filter of $\struct {S, \preceq}$
{{iff}}:
{{begin-axiom}}
{{axiom | n = 1
        | m = T \ne \O
}}
{{axiom | n = 2
        | m = x, y \in T \implies \exists z \in T: z \preccurlyeq x, z \preccurlyeq y
}}
{{axiom | n = 3
        | m = \forall x \in T: \forall y \in S: x \preccurlyeq y \implies y \in T
}}
{{end-axiom}}
By the duality principle, the dual of this statement is:
{{begin-axiom}}
{{axiom | n = 1'
        | m = T \ne \O
}}
{{axiom | n = 2'
        | m = x, y \in T \implies \exists z \in T: x \preccurlyeq z, y \preccurlyeq z
}}
{{axiom | n = 3'
        | m = \forall x \in T: \forall y \in S: y \preccurlyeq x \implies y \in T
}}
{{end-axiom}}
By definition of ideal:
:$T$ is an ideal of $\struct {S, \preceq}$
{{qed}}
Category:Dual Pairs (Order Theory)
Category:Order Theory
ohxnqxzisl64jj4nruhcks7mtst2yb2
Theorem: Characterization of Completely Prime Ideal in Complete Lattice

Let $\struct{L, \vee, \wedge, \preceq}$ be a complete lattice.
Let $I \subseteq L$.
Then:
:$I$ is a completely prime ideal
{{iff}}
:$(1)\quad\forall A \subseteq L : \bigwedge A \in I \iff \paren{\exists a \in A : a \in I}$
:$(2)\quad\forall $ finite $A \subseteq L : \bigvee A \in I \iff \paren{\forall a \in A : a \in I}$
where:
:* $\bigwedge A$ denotes the infimum of $A$ in $L$
:* $\bigvee A$ denotes the supremum of $A$ in $L$

Proof:
This is the dual statement of Characterization of Completely Prime Filter in Complete Lattice by Dual Pairs (Order Theory).
The result follows from the Duality Principle.
{{qed}}
Category:Complete Lattices
Category:Completely Prime Ideals
kljmrxbby0m3t3jw55dcp3nczxjatig
Theorem: Simpson's Rule/Repeated

Let $f$ be a real function which is integrable on the closed interval $\closedint a b$.
Let $P = \set {x_0, x_1, x_2, \ldots, x_{n - 1}, x_n}$ form a normal subdivision of $\closedint a b$:
:$\forall r \in \set {1, 2, \ldots, n}: x_r - x_{r - 1} = \dfrac {b - a} n$
where $n$ is even.
Then the definite integral of $f$ {{WRT|Integration}} $x$ from $a$ to $b$ can be approximated as:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f x \rd x
      | o = \approx
      | r = \dfrac h 3 \paren {y_0 + \sum_{r \mathop = 1}^{n / 2 - 1} 4 y_{2 r - 1} + \sum_{r \mathop = 1}^{n / 2 - 1} 2 y_{2 r} + y_n}
      | c = 
}}
{{eqn | r = \dfrac h 3 \paren {y_0 + 4 y_1 + 2 y_2 + 4 y_3 + 2 y_4 + \cdots + 2 y_{n - 2} + 4 y_{n - 1} + y_n}
      | c = 
}}
{{end-eqn}}
where:
:$\forall i \in \set {0, 1, 2, \ldots, n}: y_i = \map f {x_i}$
:$h = \dfrac {b - a} n$
This is known as the '''repeated Simpson's rule'''.

Proof:
{{ProofWanted|Graphical approach based on approximating the area under the curve as a series of parabolas.}}
Theorem: Element of Completely Prime Filter iff Does not Precede Supremum of Relative Complement

Let $\struct{L, \preceq}$ be a complete lattice.
Let $p$ be a completely prime filter $p$ of $L$.
Let $a \in L$.
Then:
:$a \in p$
{{iff}}:
:$a \npreceq \bigvee \paren{L \setminus p}$
where:
:$L \setminus p$ denotes the relative complement of $p$ in $L$
:$\bigvee \paren{L \setminus p}$ denotes the supremum of $L \setminus p$

Proof:
=== Necessary Condition ===
We show the contrapositive statement:
:$a \preceq \bigvee \paren{L \setminus p} \implies a \notin p$
Let:
:$a \preceq \bigvee \paren{L \setminus p}$
By definition of completely prime filter:
:$\bigvee \paren{L \setminus p} \in L \setminus p$ 
By definition of relative complement:
:$\bigvee \paren{L \setminus p} \notin p$ 
By definition of filter:
:$a \notin p$
{{qed|lemma}}
Theorem: Monotone Real Function is Measurable

Let $I \subseteq \R$ be an open interval.
Let $\map \BB I$ and $\map \BB \R$ be the Borel $\sigma$-algebras of $I$ and $\R$ respectively.
Let $F : \R \to \R$ be a monotone function.
Then $F$ is $\map \BB I/\map \BB \R$-measurable.

Proof:
We first assume that $F$ is increasing.
From Borel Sigma-Algebra of Subset is Trace Sigma-Algebra, $\map \BB I$ is the trace $\sigma$-algebra of $I$ in $\map \BB \R$. 
From Characterization of Measurable Functions, it is enough to show that:
:$J_t = \set {x \in I : \map F x \le t} \in \map \BB I$ for each $t \in \R$. 
From Measure of Interval is Length and the definition of the trace $\sigma$-algebra, it is enough to show that $J_t$ is an interval for each $t \in \R$.
Fix $t \in \R$. 
Suppose that $x \in J_t$ and $y \in \R$ with $y \le z$. 
Since $F$ is increasing, we have:
:$\map F z \le \map F y \le t$. 
In particular, $\map F z \le t$ and $z \in J_t$.
Hence $J_t$ is a real interval that is unbounded below.
Hence $J_t \in \map \BB I$ from Measure of Interval is Length and the definition of the trace $\sigma$-algebra.
Hence by Characterization of Measurable Functions, $F$ is $\map \BB I/\map \BB \R$-measurable.
Now suppose that $F$ is decreasing.
Then $-F$ is increasing.
Hence from the previous case, $-F$ is $\map \BB I/\map \BB \R$-measurable.
From Pointwise Scalar Multiple of Measurable Function is Measurable, $F$ is $\map \BB I/\map \BB \R$-measurable.
{{qed}}
Category:Measurable Functions
Category:Monotone Real Functions
rvyzhszszx7w0zjz4zsifgfpldyi69h