avewright/proofwiki-math huggingface dataset:
Theorem: Canonical Bijection from Completely Prime Filters to Meet Irreducible Elements

Let $\struct{L, \preceq}$ be a locale.
Let $\map {\operatorname{Sp}} L = \struct{\map {\operatorname{pt}} L, \set{\Sigma_a : a \in L}}$ be the spectrum of $L$ as completely prime filters where:
:*$\quad\map {\operatorname{pt}} L$ denotes the set of points as completely prime filters of $L$.
:*$\quad$for each $a \in L$, $\Sigma_a = \set{p \in \map {\operatorname{pt}} L : a \in p}$
Let $\Sigma_L = \set{\Sigma_a : a \in L}$
Let $\map {\operatorname{Sp}'} L = \struct{\map {\operatorname{pt}'} L, \set{\Sigma'_a : a \in L}}$ be the spectrum of $L$ as meet-irreducible elements where:
:*$\quad\map {\operatorname{pt}'} L$ denotes the set of points as meet-irreducible elements of $L$.
:*$\quad$for each $a \in L$, $\Sigma'_a = \set{p \in \map {\operatorname{pt}'} L : a \npreceq p}$
Let $\Sigma'_L = \set{\Sigma'_a : a \in L}$
Let $f : \map {\operatorname{pt}} L \to \map {\operatorname{pt}'} L$ be the mapping defined by:
:$\forall p \in \map {\operatorname{pt}} L : \map f 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}$
Then:
:$f$ is a bijection
:$f^\to \restriction_{\Sigma_L}$ is a surjection from $\Sigma_L$ to $\Sigma'_L$

Proof:
=== $f$ is a Bijection ===
From Meet Irreducible Element Induced by Completely Prime Filter:
:$f$ is a well-defined mapping
Let $g : \map {\operatorname{pt}'} L \to \map {\operatorname{pt}} L$ be the mapping defined by:
:$\forall m \in \map {\operatorname{pt}'} L : \map g m = \set{a \in L : a \npreceq m}$
From Completely Prime Filter Induced by Meet Irreducible Element:
:$g$ is a well-defined mapping
From Completely Prime Filter Induced by Meet Irreducible Induced by Completely Prime Filter:
:$g \circ f = \operatorname {id}_{\map {\operatorname{pt}} L}$
where $\operatorname {id}_{\map {\operatorname{pt}} L}$ is the identity mapping on $\map {\operatorname{pt}} L$
From Meet Irreducible Induced by Completely Prime Filter Induced by Meet Irreducible:
:$f \circ g = \operatorname {id}_{\map {\operatorname{pt}'} L}$
where $\operatorname {id}_{\map {\operatorname{pt}} L}$ is the identity mapping on $\map {\operatorname{pt}'} L$
Hence $f$ is a bijection by definition.
{{qed|lemma}}
Theorem: Canonical Bijection from Frame Homomorphisms to Continuous Maps

Let $\struct {L, \preceq}$ be a locale.
Let $\map {\operatorname{Sp}} L = \struct{\map {\operatorname{pt}} L, \set{\Sigma_a : a \in L}}$ be the spectrum of $L$ as frame homomorphisms where:
{{begin-itemize}}
{{item|*|$\map {\operatorname{pt} } L$ denotes the set of points as frame homomorphisms of $L$.}}
{{item|*|for each $a \in L$, $\Sigma_a {{=}} \set {\phi \in \map {\operatorname{pt} } L : \map \phi a {{=}} \top}$}}
{{end-itemize}}
Let $\Sigma_L = \set{\Sigma_a : a \in L}$
Let $\map {\operatorname{Sp}'} L = \struct{\map {\operatorname{pt}'} L, \set{\Sigma'_a : a \in L}}$ be the spectrum of $L$ as continuous maps where:
{{begin-itemize}}
{{item|*|$\map {\operatorname{pt}'} L$ denotes the set of points as continuous maps of $L$.}}
{{item|*|for each $a \in L$, $\Sigma'_a {{=}} \set {g \in \map {\operatorname{pt} } L : \map {\loweradjoint g} a {{=}} \top}$ where:
:$\loweradjoint g : L \to 2$ is the frame homomorphism such that $\tuple {g,\loweradjoint g}$ is a Galois connection
}}
{{end-itemize}}
Let $\Sigma'_L = \set{\Sigma'_a : a \in L}$
Let $f : \map {\operatorname{pt}} L \to \map {\operatorname{pt}'} L$ be the mapping defined by:
:$\forall \phi \in \map {\operatorname{pt}} L : \map f \phi = \upperadjoint \phi$
where $\tuple{\upperadjoint \phi, \phi}$ is a Galois connection
Then:
:$f$ is a bijection
:$f^\to \restriction_{\Sigma_L}$ is a surjection from $\Sigma_L$ to $\Sigma'_L$

Proof:
=== $f$ is a Bijection ===
From Frame Homomorphism is Lower Adjoint of Galois Connection and Galois Connection is Unique for Given Lower Adjoint:
:$\forall \phi \in \map {\operatorname{pt}} L: \exists !$ Galois connection $\tuple{\upperadjoint \phi, \phi}$
By definition of continuous map:
:$\forall \phi \in \map {\operatorname{pt}} L: \exists !$ continuous map $\upperadjoint \phi : \tuple{\upperadjoint \phi, \phi}$ is a Galois connection
Hence $f$ is a well-defined mapping.
From Galois Connection is Unique for Given Lower Adjoint:
:$f$ is an injection
By definition of continuous map:
:$f$ is a surjection
Hence $f$ is a bijection by definition.
{{qed|lemma}}
Theorem: Everywhere Dense Set determines Adjoint Linear Transformation

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \innerprod \cdot \cdot_X}$ and $\struct {Y, \innerprod \cdot \cdot_Y}$ be Hilbert spaces.
Let $\DD$ be an everywhere dense subset of $Y$. 
Let $T : X \to Y$ and $S : Y \to X$ be bounded linear transformations such that:
:$\innerprod {T x} y_Y = \innerprod x {S y}_X$ for each $x \in X$ and $y \in \DD$. 
Then $S = T^\ast$.

Proof:
By the definition of the adjoint, we have:
:$\innerprod x {S y}_X = \innerprod {T x} y_Y = \innerprod x {T^\ast y}_X$ for each $x \in X$ and $y \in \DD$.
Let $y \in Y$.
Since $\DD$ is everywhere dense in $Y$, there exists a sequence $\sequence {y_n}_{n \mathop \in \N}$ in $\DD$ such that $y_n \to y$.
Then:
:$\innerprod x {S y_n}_X = \innerprod x {T^\ast y_n}$ for each $x \in X$.
Taking $n \to \infty$ and using Inner Product is Continuous, we have:
:$\innerprod x {S y}_X = \innerprod x {T^\ast y}$ for each $x \in X$ and $y \in Y$.
So:
:$\innerprod x {S y - T^\ast y}_X = 0$ for each $x \in X$ and $y \in Y$. 
Hence $S y - T^\ast y \in X^\bot$. 
From Linear Subspace Dense iff Zero Orthocomplement, we have $X^\bot = \set { {\mathbf 0}_Y}$. 
Hence $S y - T^\ast y = {\mathbf 0}_Y$.
So $S y = T^\ast y$ for each $y \in Y$. 
Hence $S = T^\ast$.
{{qed}}
Category:Adjoints
9eo0wvd54d5m78p0sqf0btjvso8i65n
Theorem: Supremum of Continuous Bounded Real-Valued Function on Everywhere Dense Subset

Let $\struct {X, \tau}$ be a topological space.
Let $\DD$ be an everywhere dense subset of $\struct {X, \tau}$. 
Let $f : X \to \R$ be a continuous bounded real-valued function.
Then:
:$\ds \sup_{x \mathop \in \DD} \map f x = \sup_{x \mathop \in X} \map f x$

Proof:
Since $\DD \subseteq X$ we have:
:$\ds \sup_{x \mathop \in \DD} \map f x \le \sup_{x \mathop \in X} \map f x$
Conversely, from the definition of supremum, for each $\epsilon > 0$ there exists $y \in X$ such that:
:$\ds \sup_{x \mathop \in X} \map f x - \frac \epsilon 2 \le \map f y \le \sup_{x \mathop \in X} \map f x$
Since $f$ is continuous, there exists an open set $U$ such that:
:$\ds \size {\map f y - \map f w} < \frac \epsilon 2$
hence:
:$\ds \map f y - \frac \epsilon 2 < \map f w < \map f y + \frac \epsilon 2$ 
for $w \in U$.
Since $\DD$ is everywhere dense, we have $\DD \cap U \ne \O$. 
Picking $w \in \DD \cap U$, we have:
:$\ds \map f w > \map f y - \frac \epsilon 2 \ge \sup_{x \mathop \in X} \map f x - \epsilon$ 
while:
:$\ds \map f w \le \sup_{x \mathop \in \DD} \map f x$
since $w \in \DD$.
Hence for each $\epsilon > 0$ we have:
:$\ds \sup_{x \mathop \in X} \map f x \le \sup_{x \mathop \in \DD} \map f x + \epsilon$
Taking $\epsilon \to 0^+$, we then obtain:
:$\ds \sup_{x \mathop \in X} \map f x \le \sup_{x \mathop \in \DD} \map f x$
Hence we have:
:$\ds \sup_{x \mathop \in \DD} \map f x = \sup_{x \mathop \in X} \map f x$
{{qed}}
Category:Continuous Real-Valued Functions
Category:Everywhere Dense
fwssw5wj2a7f7ep7k612op5m3ckys3i
Theorem: Hilbert Space Direct Sum of Countably Many Separable Hilbert Spaces is Separable

Let $\GF \in \set {\R, \C}$. 
For each $n \in \N$, let $\struct {\HH_n, \innerprod \cdot \cdot_n}$ be a separable Hilbert space over $\GF$. 
Let:
:$\ds \HH = \bigoplus_{n \mathop \in \N} \HH_n$
be the direct sum of $\sequence {\HH_n}_{n \mathop \in \N}$. 
Then $\HH$ is separable.

Proof:
For each $n \in \N$, let $\sequence {e_k^{(n)} }_{k \mathop \in \N}$ be a countable everywhere dense subset of $\HH_n$.
Let $\SS$ be the set of $f \in \HH$ for which there exists $N \in \N$ such that:
:$\map f n = e_{\map k n}^{(n)} \in \HH_n$ for some $\map k n \in \N$ if $n \le N$
:$\map f n = {\mathbf 0}_{\HH_n}$ if $n > N$.
To every $f \in \SS$, we can associate a function $\phi_f : \N \to \Z_{\ge 0}$ defined by:
:$\map {\phi_f} n = \map k n$ for $n \le N$
:$\map {\phi_f} n = 0$ for $n > N$.
From Set of Finitely Supported Functions on Integers is Countable and Subset of Countable Set is Countable, $\set {\phi_f : f \in \SS}$ is countable.
Hence $\SS$ is countable.
From Everywhere Dense Subset of Countable Hilbert Space Direct Sum in terms of Everywhere Dense Subsets of Summands, $\SS$ is everywhere dense in $\HH$.
Hence $\HH$ is separable.
{{qed}}
Category:Hilbert Space Direct Sums
brcq26r3601sxfv7u1wqt6lxgz9e34q
Theorem: Set of Finitely Supported Functions on Integers is Countable

Let $\SS$ be the set of functions $f : \Z \to \Z$ for which there exists $N \in \N$ such that:
:$\map f n = 0$ for all $n \in \Z$ with $\size n > N$.
Then $\SS$ is countable.

Proof:
Let $\sequence {p_n}_{n \mathop \in \N}$ be an enumeration of the prime numbers.
For each $f \in \SS$ let $N_f \in \N$ be least such that:
:$\map f n = 0$ for all $n \in \Z$ with $\size n > N_f$.
Then for each $f \in \SS$, define $\map \phi f$ by:
:$\ds \map \phi f = 2^{\map f 0} \prod_{j \mathop = 1}^{N_f} p_{2 j + 1}^{\map f j} \prod_{j \mathop = 1}^{N_f} p_{2 \paren {j + 1} }^{\map f {-j} }$
We show that $\phi : \SS \to \N$ is an injection.
Suppose that $f, g \in \SS$ and that $\map \phi f = \map \phi g$.
We have:
:$\ds 2^{\map f 0} \prod_{j \mathop = 1}^{N_f} p_{2 j + 1}^{\map f j} \prod_{j \mathop = 1}^{N_f} p_{2 \paren {j + 1} }^{\map f {-j} } = 2^{\map g 0} \prod_{j \mathop = 1}^{N_g} p_{2 j + 1}^{\map g j} \prod_{j \mathop = 1}^{N_g} p_{2 \paren {j + 1} }^{\map g {-j} }$
Since $N_f$ and $N_g$ were picked to be least, we must have $N_f = N_g$.
Further from the Fundamental Theorem of Arithmetic, we must have:
:$\map f j = \map g j$ for all $j \in \Z$.
Hence $f = g$. 
Hence $\phi$ is an injection.
So $\SS$ is countable.
{{qed}}
Category:Countable Sets
19cnytp01w2eq8bv0bu30zqgvykjss3
Theorem: Direct Sum of Representations of C*-Algebra is Representation

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra. 
Let $\family {\tuple {\pi_i, \HH_i} }_{i \mathop \in I}$ be an $I$-index family of representations of $\struct {A, \ast, \norm {\, \cdot \,} }$.
Let:
:$\ds \HH = \bigoplus_{i \mathop \in I} \HH_i$
be the Hilbert space direct sum of $\sequence {\struct {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ with norm $\norm {\, \cdot \,}_\HH$.
Let:
:$\ds \pi = \bigoplus_{i \mathop \in I} \pi_i$
be the direct sum of $\family {\pi_i}_{i \mathop \in I}$. 
Then $\tuple {\pi, \HH}$ be a representation of $A$.

Proof:
Let $a, b \in A$ and $\lambda \in \C$.
{{begin-eqn}}
{{eqn	| l = \map \pi {a + \lambda b}
		| r = \bigoplus_{i \mathop \in I} \map {\pi_i} {a + \lambda b} 
}}
{{eqn	| r = \bigoplus_{i \mathop \in I} \paren {\map {\pi_i} a + \lambda \map {\pi_i} b}
		| c = $\pi_i$ is a linear transformation for each $i \in I$ 
}}
{{eqn	| r = \bigoplus_{i \mathop \in I} \map {\pi_i} a + \lambda \bigoplus_{i \mathop \in I} \map {\pi_i} a
		| c = Linear Combination of Direct Sums of Bounded Linear Operators on Hilbert Space
}}
{{eqn	| r = \map \pi a + \lambda \map \pi b
}}
{{end-eqn}}
so $\pi$ is a linear transformation.
We also have:
{{begin-eqn}}
{{eqn	| l = \map \pi {a b}
		| r = \bigoplus_{i \mathop \in I} \map {\pi_i} {a b}
}}
{{eqn	| r = \bigoplus_{i \mathop \in I} \map {\pi_i} a \map {\pi_i} b
		| c = $\pi_i$ is an algebra homomorphism for each $i \in I$
}}
{{eqn	| r = \paren {\bigoplus_{i \mathop \in I} \map {\pi_i} a} \paren {\bigoplus_{i \mathop \in I} \map {\pi_i} b}
		| c = Composition of Direct Sums of Bounded Linear Operators on Hilbert Space
}}
{{eqn	| r = \map \pi a \map \pi b
}}
{{end-eqn}}
Hence $\pi$ is an algebra homomorphism.
We also have:
{{begin-eqn}}
{{eqn	| l = \paren {\map \pi a}^\ast 
		| r = \paren {\bigoplus_{i \mathop \in I} \map {\pi_i} a}^\ast 
}}
{{eqn	| r = \bigoplus_{i \mathop \in I} \paren {\map {\pi_i} a}^\ast 
		| c = Adjoint of Direct Sum of Bounded Linear Operators on Hilbert Space
}}
{{eqn	| r = \bigoplus_{i \mathop \in I} \map {\pi_i} {a^\ast} 
		| c = $\pi_i$ is an algebra homomorphism for each $i \in I$ 
}}
{{eqn	| r = \map \pi {a^\ast} 
}}
{{end-eqn}}
so $\pi$ is a $\ast$-algebra homomorphism.
Finally, if $A$ is unital, we have:
{{begin-eqn}}
{{eqn	| l = \map \pi { {\mathbf 1}_A}
		| r = \bigoplus_{i \mathop \in I} \map {\pi_i} { {\mathbf 1}_A}
}}
{{eqn	| r = \bigoplus_{i \mathop \in I} I_{\map B {\HH_i} }
		| c = {{Defof|Representation of C*-Algebra}}
}}
{{eqn	| r = I_{\map B \HH}
		| c = Direct Sum of Identity Operators on Hilbert Spaces is Identity Operator
}}
{{end-eqn}}
Hence $\tuple {\pi, \HH}$ is a representation of $A$.
{{qed}}
Theorem: Inverse Image Mapping of Frame Homomorphism Preserves Completely Prime Filter

Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be frames.
Let $\phi : L_1 \to L_2$ be a frame homomorphism.
Let $\phi^\gets$ denote the inverse image mapping of $\phi$.
Let $F$ be a completely prime filter of $L_2$.
Then:
:$\map {\phi^\gets} F$ is a completely prime filter of $L_1$

Proof:
From Characterization of Completely Prime Filter in Complete Lattice it is sufficient to show:
:$(1)\quad\forall A \subseteq L : \bigvee A \in \map {\phi^\gets} F \iff \paren{\exists a \in A : a \in \map {\phi^\gets} F}$
:$(2)\quad\forall $ finite $A \subseteq L : \bigwedge A \in \map {\phi^\gets} F \iff \paren{\forall a \in A : a \in \map {\phi^\gets} F}$
Theorem: Existence of Primitive Element for every Prime

Let $p$ be a prime number.
Then there exists a primitive element of the multiplicative group of reduced residues $\Z'_p$.

Proof:
{{ProofWanted|It needs to be demonstrated that $\Z'_p$ is cyclic, which Nelson assures us is "not elementary, and determining the smallest primitive element can be difficult."}}
Theorem: Standard Topology on Locally Convex Space makes Seminorms Continuous

Let $\struct {X, \PP}$ be a locally convex space.
Let $\tau$ be the standard topology on $\struct {X, \PP}$. 
Let $p \in \PP$.
Then $p$ is continuous as a function $\struct {X, \PP} \to \R$.

Proof:
It is enough to show that for each $x \in X$ and $\epsilon > 0$, there exists $U_x \in \tau$ such that:
:$\size {\map p x - \map p y} < \epsilon$ for each $y \in U_x$. 
From the definition of the standard topology, we have:
:$U_x = \set {y \in X : \map p {y - x} < \epsilon} \in \tau$
Then from Reverse Triangle Inequality: Seminormed Vector Space, we have:
:$\size {\map p y - \map p x} \le \map p {y - x} < \epsilon$ 
Hence $U_x \in \tau$ works.
{{qed}}
Category:Locally Convex Spaces
04oumg7bn1fls8f7ggzbkf5lgn58m01
Theorem: Lateral Face of Prismatoid is Triangle, Trapezium or Parallelogram

Let $\PP$ be a prismatoid.
Let $\FF$ be a lateral face of $\PP$.
Then $\FF$ is one of the following:
:a triangle
:a trapezium
:a parallelogram.

Proof:
We have that an antiprism is {{apriori}} a prismatoid.
The lateral faces of an antiprism are triangles.
We have that an oblique prism is {{apriori}} a prismatoid.
The lateral faces of an oblique prism are parallelograms.
Suppose that $\FF$ were a polygon with more than $4$ sides.
Then at least $2$ of those adjacent sides, $S$ and $T$ say, are also sides of $\FF$.
But as $S$ and $T$ are not in the same plane as the lateral edges that form the other sides of $\FF$, they cannot form a polygon.
So the lateral faces can have no more than $4$ sides.
So, let $A$ and $B$ be the bases of $\PP$.
They are parallel by definition.
Let $L_1$ and $L_2$ be sides of $A$ and $B$ respectively which form the sides of one of the lateral faces $\FF$ of $\PP$.
Let $L_1$ and $L_2$ be such that they are not of the same length.
Then $\FF$ is a quadrilateral which has $2$ unequal sides parallel.
Hence by definition it is a trapezium.
{{qed}}
Theorem: Homeomorphism Preserves System of Open Neighborhoods

Let $T_1 = \struct{S_1, \tau_1}$ and $T_2 = \struct{S_2, \tau_2}$ be topological spaces.
Let $f : T_1 \to T_2$ be a homeomorphism between $T_1$ and $T_2$.
Let $f^\to : \powerset{S_1}\to \powerset{S_2}$ denote the direct image mapping of $f : S_1 \to S_2$.
Then:
:$\forall x \in S_1 : f^\to \sqbrk {\map \UU x} = \map \UU {\map f x}$
where $\map \UU x$ and $\map \UU {\map f x}$ denote the systems of open neighborhoods of $x$ and $\map f x$ respectively.

Proof:
Let $x \in S_1$.
Theorem: Frame Homomorphism Onto Two 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$.
Let $p$ be a completely prime filter of $L$.
Let $\phi_p : L \to \mathbf 2$ be the mapping defined by:
::<nowiki>$\forall a \in L : \map {\phi_p} a = \begin{cases}
\top & : a \in p\\
\bot & : a \notin p 
\end{cases}$</nowiki>
Then:
:$\phi_p$ is a frame homomorphism

Proof:
=== $\phi_p$ is Arbitrary Join Preserving ===
Let $\set{a_i : i \in I}$ be an indexed subset of elements of $L$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\phi_p} {\bigvee_{i \in I} a_i}
      | r = \top
}}
{{eqn | ll = \leadstoandfrom
      | l = \bigvee_{i \in I} a_i
      | o = \in
      | r = p
      | c = Definition of $\phi_p$
}}
{{eqn | ll = \leadstoandfrom
      | l = \exists i \in I : a_i
      | o = \in
      | r = p
      | c = Characterization of Completely Prime Filter in Complete Lattice
}}
{{eqn | ll = \leadstoandfrom
      | l = \exists i \in I : \map {\phi_p} {a_i}
      | r = \top
      | c = Definition of $\phi_p$
}}
{{eqn | ll = \leadstoandfrom
      | l = \bigvee_{i \in I} \map {\phi_p} {a_i}
      | r = \top
      | c = {{Defof|Two (Boolean Lattice)|(Boolean Lattice) 2}}
}}
{{end-eqn}}
It follows that $\phi_p$ is arbitrary join preserving.
{{qed|lemma}}
Theorem: Completely Prime Filter Induced by Frame Homomorphism Onto Two

Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\struct{\mathbf 2, \vee, \wedge, \preceq}$ denote the (Boolean Lattice) $\mathbf 2$.
Let $\phi : L \to \mathbf 2$ be a frame homomorphism.
Then:
:$\map {\phi^{-1}} \top$ is a completely prime filter
where $\map {\phi^{-1}} \top$ denotes the preimage of $\top \in \mathbf 2$ under the mapping $\phi$

Proof:
From Singleton of Greatest Element in Two is Completely Prime Filter:
:$\set \top$ is a completely prime filter
From Inverse Image Mapping of Frame Homomorphism Preserves Completely Prime Filter:
:$\map {\phi^\gets}{\set \top}$ is a completely prime filter
We have:
{{begin-eqn}}
{{eqn | l = \map {\phi^\gets}{\set \top}
      | r = \phi^{-1} \sqbrk {\set \top}
      | c = {{Defof|Inverse Image Mapping of Mapping}}
}}
{{eqn | r = \map {\phi^{-1} } \top
      | c = {{Defof|Inverse Image of Element under Mapping}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Completely Prime Filters
Category:Two (Boolean Lattice)
Category:Frame Homomorphisms
3wiljdv304bq4ppbtjeakfbpcxdckpe
Theorem: Total Variation is Smallest Measure exceeding Modulus of Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be either a signed measure or complex measure on $\struct {X, \Sigma}$.
Let $\nu$ be a measure such that:
:$\cmod {\map \mu A} \le \map \nu A$ for each $A \in \Sigma$. 
Let $\cmod \mu$ be the variation of $\mu$.
Then:
:$\map {\cmod \mu} A \le \map \nu A$ for each $A \in \Sigma$.

Proof:
Let $\map P A$ be the set of finite partitions of $A$ into $\Sigma$-measurable sets.
Let $\set {A_1, A_2, \ldots, A_n} \in \map P A$.
Then we have:
{{begin-eqn}}
{{eqn	| l = \sum_{j \mathop = 1}^n \cmod {\map \mu {A_j} }
		| o = \le
		| r = \sum_{j \mathop = 1}^n \map \nu {A_j}
}}
{{eqn	| r = \map \nu {\sum_{j \mathop = 1}^n A_j} 
		| c = {{Defof|Signed Measure}} or {{Defof|Complex Measure}}
}}
{{eqn	| r = \map \nu A 
		| c = $\set {A_1, A_2, \ldots, A_n} \in \map P A$ 
}}
{{end-eqn}}
Taking the supremum over $\set {A_1, A_2, \ldots, A_n}$ we obtain:
:$\map {\cmod \mu} A \le \map \nu A$ 
{{qed}}
Category:Variation of Complex Measure
Category:Variation of Signed Measure
74zf1pcpdpagnmn7n2nfpof9evy1tdz
Theorem: Positive and Negative Parts of Signed Measure are Mutually Singular

Let $\struct {X, \Sigma}$ be a measurable space. 
Let $\mu$ be a signed measure on $\struct {X, \Sigma}$.
Let $\tuple {\mu^+, \mu^-}$ be the Jordan decomposition of $\mu$.
Then $\mu^+$ and $\mu^-$ are mutually singular.

Proof:
From the Hahn Decomposition Theorem, there exists $\mu$-positive set and a $\mu$-negative set such that:
:$X = P \cup N$
and:
:$P \cap N = \O$ 
From the Jordan Decomposition Theorem, we have:
:$\map {\mu^+} A = \map \mu {A \cap P}$
and:
:$\map {\mu^-} A = -\map \mu {A \cap N}$
for each $A \in \Sigma$.
From the definition of a signed measure we have $\map \mu \O = 0$. 
Hence $\map {\mu^+} N = 0$ and $\map {\mu^-} {X \setminus N} = 0$.
So $\mu^+$ is concentrated on $N^c$ and $\mu%-$ is concentrated on $N$. 
So $\mu^+$ and $\mu^-$ are mutually singular.
{{qed}}
Category:Mutually Singular Measures
Category:Signed Measures
tpb2o2xppprvpgf11qx49mir6emlqz8
Theorem: Lebesgue Decomposition Theorem/Uniqueness

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a measure on $\struct {X, \Sigma}$.
Let $\nu$ be either: 
:a $\sigma$-finite measure
:a complex measure.
Then the Lebesgue decomposition of $\nu$ with respect to $\mu$ is unique.

Proof:
Suppose that:
:$\nu = \nu_a + \nu_s = \nu_a' + \nu_s'$
where:
:$\nu_a$ and $\nu_a'$ are absolutely continuous with respect to $\mu$
:$\nu_s$ and $\nu_s'$ are mutually singular with respect to $\mu$.
Theorem: Triangle Inequality for Variation of Complex Measure

Let $\struct {X, \Sigma}$ be measurable space.
Let $\mu$ and $\nu$ be two complex measures.
Let $\cmod {\mu + \nu}$, $\cmod \mu$ and $\cmod \nu$ be the variation of $\mu + \nu$, $\mu$ and $\nu$ respectively.
Then:
:$\cmod {\mu + \nu} \le \cmod \mu + \cmod \nu$

Proof:
Let $\map P A$ be the set of finite partitions of $A$ into $\Sigma$-measurable sets.
Let $\set {A_1, A_2, \ldots, A_n} \in \map P A$. 
Then from Triangle Inequality for Complex Numbers we have:
:$\ds \sum_{j \mathop = 1}^n \cmod {\map \mu {A_j} + \map \nu {A_j} } \le \sum_{j \mathop = 1}^n \cmod {\map \mu {A_j} } + \sum_{j \mathop = 1}^n \cmod {\map \nu {A_j} } \le \map {\cmod \mu} A + \map {\cmod \nu} A$
by the definition of variation.
Taking the supremum over $\set {A_1, A_2, \ldots, A_n} \in \map P A$ we have:
:$\map {\cmod {\mu + \nu} } A \le \map {\cmod \mu} A + \map {\cmod \nu} A$ 
{{qed}}
Category:Variation of Complex Measure
Category:Triangle Inequality
iu2n98m84f1vq1lx1h35syllqq9pngw
Theorem: Measure is Discrete iff Concentrated on Countable Set

Let $\struct {X, \Sigma}$ be a measurable space such that:
:$\set x \in \Sigma$ for all $x \in X$.
Let $\mu$ be a measure. 
Then $\mu$ is discrete {{iff}}:
:there exists a countable set $C \subseteq X$ such that $\map \mu {X \setminus C} = 0$.

Proof:
=== Necessary Condition ===
Suppose that $\mu$ is discrete.
Then there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $X$ and a sequence of non-negative real numbers $\sequence {\lambda_n}_{n \mathop \in \N}$ such that:
:$\ds \mu = \sum_{n \mathop = 1}^\infty \lambda_n \delta_{x_n}$
where $\delta_{x_n}$ is the dirac measure at $x_n$.
Let:
:$C = \set {x_n : n \in \N}$
Then $C$ is countable.
Since $x_n \not \in X \setminus C$ for each $n \in \N$, we have $\map {\delta_{x_n} } {X \setminus C} = 0$.
Hence we have $\map \mu {X \setminus C} = 0$. 
{{qed|lemma}}
Theorem: Intersection Measures preserve Absolute Continuity

Let $\struct {X, \Sigma}$ be a measurable space.
Let $A \in \Sigma$.
Let $\mu$ and $\nu$ be measures such that:
:$\mu$ is absolutely continuous {{WRT}} $\nu$.
Let $\mu_A$ be the intersection measure of $\mu$ {{WRT}} $A$.
Then $\mu_A$ is absolutely continuous {{WRT}} $\nu$.

Proof:
Let $B \in \Sigma$ be such that:
:$\map \nu B = 0$
From Null Sets Closed under Subset, we have that $\map \nu {A \cap B} = 0$.
Hence since $\mu$ is absolutely continuous {{WRT}} $\nu$, we have $\map \mu {A \cap B} = 0$.
That is, $\map {\mu_A} B = 0$. 
Hence whenever $B \in \Sigma$ is a $\nu$-null set, it is a $\mu_A$-null set.
Hence $\mu_A$ is absolutely continuous {{WRT}} $\nu$.
{{qed}}
Category:Absolutely Continuous Measures
rkmv9bz17uudbmuk32duv8sqaulozou