avewright/proofwiki-math huggingface dataset:
Theorem: Evaluation Linear Transformation on Normed Vector Space is Weak to Weak-* Homeomorphism onto Image

Let $\Bbb F \in \set {\R, \C}$.
Let $X$ be a normed vector space over $\Bbb F$. 
Let $X^\ast$ be the normed dual of $X$. 
Let $X^{\ast \ast}$ be the second normed dual of $X$. 
Let $w$ be the weak topology on $X$.
Let $w^\ast$ be the weak-$\ast$ topology on $X^{\ast \ast}$.
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
Then $\iota : \struct {X, w} \to \struct {\iota X, w^\ast}$ is a homeomorphism.

Proof:
From Evaluation Linear Transformation on Normed Vector Space is Weak to Weak-* Continuous Embedding into Second Normed Dual, $\iota$ is continuous.
From Evaluation Linear Transformation on Normed Vector Space is Linear Isometry, $\iota$ is bijective.
It remains to show that $\iota^{-1} : \struct {\iota X, w^\ast} \to \struct {X, w}$ is continuous.
From Continuity in Initial Topology, it is enough to show that: 
:$f \circ \iota^{-1} : \struct {\iota X, w^\ast} \to \Bbb F$ is continuous.
From Characterization of Continuity of Linear Functional in Weak-* Topology and Subspace Topology on Initial Topology is Initial Topology on Restrictions, there exists $g \in X^\ast$ such that: 
:$f \circ \iota^{-1} = g^\wedge \restriction_{\iota X}$
We have, for $x^\wedge \in \iota X$:
:$\map {\paren {f \circ \iota^{-1} } } {x^\wedge} = \map f x$
Now note that: 
:$\map f x = \map {x^\wedge} f = \map {f^\wedge} {x^\wedge}$ 
from the definition of the evaluation linear transformation.
So we have: 
:$f^\wedge \restriction_{\iota X} = f \circ \iota^{-1}$ 
So $f \circ \iota^{-1} : \struct {\iota X, w^\ast} \to \Bbb F$ is continuous.
So by Continuity in Initial Topology $\iota^{-1} : \struct {\iota X, w^\ast} \to \struct {X, w}$ is continuous.
So $\iota : \struct {X, w} \to \struct {\iota X, w^\ast}$ is a homeomorphism.
{{qed}}
Category:Evaluation Linear Transformations
Category:Weak Topologies on Topological Vector Spaces
Category:Weak-* Topologies
o6t0noo9d8v7ef3o0est7b66y2lv93u
Theorem: Characterization of Continuity of Linear Functional in Weak-* Topology

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$. 
Let $X^\ast$ be the normed dual space of $X$.
Let $w^\ast$ be the weak-$\ast$ topology on $X^\ast$. 
Let $X^{\ast \ast}$ be the second normed dual of $X$.
Then a linear functional $\phi : \struct {X^\ast, w^\ast} \to \GF$ is continuous {{iff}} there exists $x \in X$ such that: 
:$\phi = x^\wedge$ 
where $x^\wedge$ is the evaluation linear transformation evaluated at $x$.
That is: 
:$\struct {X^\ast, w^\ast}^\ast = \iota X$

Proof:
Note that the weak-$\ast$ topology $w^\ast$ is generated as an initial topology by $\set {x^\wedge : x \in X}$. 
This result is then given by Continuity of Linear Functionals in Initial Topology on Vector Space Generated by Linear Functionals, taking $F = \set {x^\wedge : x \in X}$. 
{{qed}}
Theorem: Normed Dual of Normed Vector Space is Separable iff Closed Unit Ball is Metrizable

Let $\GF \in \set {\R, \C}$.
Let $X$ be a normed vector space over $\GF$.
Let $w$ be the weak topology on $X$. 
Let $X^\ast$ be the normed dual space of $X$.
Let $B_X^-$ be the closed unit ball of $X$. 
Then $X^\ast$ is separable {{iff}} $\struct {B_X^-, w}$ is metrizable.

Proof:
Let $X^{\ast \ast}$ be the second normed dual.
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
Theorem: Image of Subset under Composite Relation

Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be relations.
Let $\RR_2 \circ \RR_1 \subseteq S_1 \times T_2$ be the composition of $\RR_1$ and $\RR_2$.
Let $A \subseteq S_1$.
Then:
:$\RR_2 \sqbrk {\RR_1 \sqbrk A \cap S_2} = \paren{\RR_2 \circ \RR_1} \sqbrk A$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall z \in T_2
      | l = z \in \RR_2 \sqbrk {\RR_1 \sqbrk A \cap S_2}
      | o = \leadstoandfrom
      | r = \exists y \in \RR_1 \sqbrk A \cap S_2 : \tuple{y, z} \in R_2
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | o = \leadstoandfrom
      | r = \exists y \in T_1 \cap S_2 : \exists x \in A : \tuple{x,y} \in R_1 : \tuple{y, z} \in R_2
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | o = \leadstoandfrom
      | r = \exists x \in A : \exists y \in T_1 \cap S_2 : \tuple{x,y} \in R_1 : \tuple{y, z} \in R_2
}}
{{eqn | o = \leadstoandfrom
      | r = \exists x \in A : \tuple{x,z} \in R_2 \circ R_1
      | c = {{Defof|Composite Relation}}
}}
{{eqn | o = \leadstoandfrom
      | r = z \in \paren{R_2 \circ R_1} \sqbrk A
      | c = {{Defof|Image of Subset under Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Element under Composite Relation

Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be relations.
Let $\RR_2 \circ \RR_1 \subseteq S_1 \times T_2$ be the composition of $\RR_1$ and $\RR_2$.
Let $x \in S_1$.
Then:
:$\RR_2 \sqbrk {\map {\RR_1} x \cap S_2} = \map {\paren{\RR_2 \circ \RR_1}} x$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \RR_2 \sqbrk {\map {\RR_1} x \cap S_2}
      | r = \RR_2 \sqbrk {\RR_1 \sqbrk {\set x} \cap S_2}
      | c = Image of Singleton under Relation
}}
{{eqn | r = \paren{\RR_2 \circ \RR_1} \sqbrk {\set x}
      | c = Image of Subset under Composite Relation
}}
{{eqn | r = \map {\paren{\RR_2 \circ \RR_1} } x
      | c = Image of Singleton under Relation
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Subset under Composite Relation with Common Codomain and Domain

Let $\RR_1 \subseteq S \times T$ and $\RR_2 \subseteq T \times U$ be relations.
Let $\RR_2 \circ \RR_1 \subseteq S \times U$ be the composition of $\RR_1$ and $\RR_2$.
Let $A \subseteq S$.
Then:
:$\RR_2 \sqbrk {\RR_1 \sqbrk A} = \paren{\RR_2 \circ \RR_1} \sqbrk A$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \RR_1 \sqbrk A
      | o = \subseteq
      | r = T
      | c = Image is Subset of Codomain
}}
{{eqn | ll = \leadsto
      | l = \RR_1 \sqbrk A
      | r = \RR_1 \sqbrk A \cap T
      | c = Intersection with Subset is Subset
}}
{{eqn | ll = \leadsto
      | l = \RR_2 \sqbrk {\RR_1 \sqbrk A}
      | r = \RR_2 \sqbrk {\RR_1 \sqbrk A \cap T} 
}}
{{eqn | r = \paren{\RR_2 \circ \RR_1} \sqbrk A
      | c = Image of Subset under Composite Relation
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Element under Composite Relation with Common Codomain and Domain

Let $\RR_1 \subseteq S \times T$ and $\RR_2 \subseteq T \times U$ be relations.
Let $\RR_2 \circ \RR_1 \subseteq S \times U$ be the composition of $\RR_1$ and $\RR_2$.
Let $x \in S$.
Then:
:$\RR_2 \sqbrk {\map {\RR_1} x} = \map {\paren{\RR_2 \circ \RR_1}} x$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \RR_2 \sqbrk {\map {\RR_1} x}
      | r = \RR_2 \sqbrk {\RR_1 \sqbrk {\set x} }
      | c = Image of Singleton under Relation
}}
{{eqn | r = \paren{\RR_2 \circ \RR_1} \sqbrk {\set x}
      | c = Image of Subset under Composite Relation with Common Codomain and Domain
}}
{{eqn | r = \map {\paren{\RR_2 \circ \RR_1} } x
      | c = Image of Singleton under Relation
}}
{{end-eqn}}
{{qed}}
Theorem: Normed Vector Space is Reflexive iff Weak and Weak-* Topologies on Normed Dual coincide

Let $X$ be a normed vector space. 
Let $X^\ast$ be the normed dual of $X$.
Let $w$ be the weak topology on $X^\ast$. 
Let $w^\ast$ be the weak-$\ast$ topology on $X^\ast$. 
Then $X$ is reflexive {{iff}} $\struct {X^\ast, w} = \struct {X^\ast, w^\ast}$.

Proof:
=== Necessary Condition ===
Suppose that $X$ is reflexive.
Then for each $\Phi \in X^{\ast \ast}$ there exists $x \in X$ such that $\Phi = x^\wedge$.
Conversely, by Evaluation Linear Transformation on Normed Vector Space is Linear Transformation from Space to Second Normed Dual, we have $x^\wedge \in X^{\ast \ast}$ for each $x \in X$. 
Hence, we have: 
:$\set {x^\wedge : x \in X} = X^{\ast \ast}$ 
By definition, $w$ is the initial topology on $X^\ast$ generated by $X^{\ast \ast}$, and $w^\ast$ is the initial topology on $X^\ast$ generated by the family $\set {x^\wedge : x \in X}$.
It follows that $w = w^\ast$. 
{{qed|lemma}}
Theorem: Normed Vector Space is Reflexive iff Closed Unit Ball in Original Space is Mapped to Closed Unit Ball in Second Dual

Let $X$ be a normed vector space. 
Let $X^\ast$ be the normed dual of $X$.
Let $X^{\ast \ast}$ be the second norm dual.
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
Let $B_X^-$ be the closed unit ball of $X$.
Let $B_{X^{\ast \ast} }^-$ be the closed unit ball of $X^{\ast \ast}$. 
Then $X$ is reflexive {{iff}} $\iota B_X^- = B_{X^{\ast \ast} }^-$.

Proof:
=== Necessary Condition ===
Suppose that $X$ is reflexive.
Then $\iota : X \to X^{\ast \ast}$ is an isometric isomorphism.
So from Injective Linear Transformation between Normed Vector Spaces sends Closed Unit Ball to Closed Unit Ball iff Isometric Isomorphism, we have that $\iota B_X^- = B_{X^{\ast \ast} }^-$. 
{{qed|lemma}}
Theorem: Kakutani's Theorem

Let $X$ be a normed vector space.
Let $w$ be the weak topology on $X$. 
Let $B_X^-$ be the closed unit ball in $X$. 
Let $X^{\ast \ast}$ be the second normed dual of $X$.
Then $X$ is reflexive {{iff}} $\struct {B_X^-, w}$ is compact.

Proof:
Let $B_{X^{\ast \ast} }^-$ be the closed unit ball in $X^{\ast \ast}$. 
Let $w^\ast$ be the weak-* topology on $X^{\ast \ast}$.
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
Theorem: Closed Set in Coarser Topology is Closed in Finer Topology

Let $X$ be a set. 
Let $\tau_1$ and $\tau_2$ be topologies on $X$ such that $\tau_1 \subseteq \tau_2$.
That is, $\tau_1$ is coarser than $\tau_2$. 
Let $C$ be a closed set in $\struct {X, \tau_1}$. 
Then $C$ is closed in $\struct {X, \tau_2}$.

Proof:
Let $C$ be a closed set in $\struct {X, \tau_1}$.
Then by definition of closed set:
:$X \setminus C$ is open in $\struct {X, \tau_1}$.
Hence by definition of open set:
:$X \setminus C \in \tau_1$
By definition of subset:
:$X \setminus C \in \tau_2$
So by definition of open set:
:$X \setminus C$ is open in $\struct {X, \tau_2}$.
So $C$ is closed in $\struct {X, \tau_2}$ by definition.
{{qed}}
Category:Closed Sets
prmsmgnz1nol5j4dp44z612736xf6pm
Theorem: Multiple of Vector in Topological Vector Space Converges

Let $K$ be a topological field. 
Let $\struct {X, \tau}$ be a topological vector space. 
Let $x \in X$.
Let $\lambda \in K$. 
Let $\sequence {\lambda_n}_{n \mathop \in \N}$ be a sequence in $K$ such that $\lambda_n \to \lambda$. 
Then: 
:$\lambda_n x \to \lambda x$

Proof:
From the definition of a topological vector space, the map $f : K \times \struct {X, \tau} \to X$ defined by:
:$\map f {\lambda, y} = \lambda y$ 
is continuous. 
From Horizontal Section of Continuous Function is Continuous, we therefore have the map $c_x : X \to X$ defined by: 
:$\map {c_x} \lambda = \lambda x$ 
is continuous.
From Continuous Mapping is Sequentially Continuous, $c_x$ is sequentially continuous.
So we have: 
:$\lambda_n x \to \lambda x$
{{qed}}
Category:Topological Vector Spaces
sp67xfl6regn6tuppj3dstj6efjpcbc
Theorem: Absorbing Set in Vector Space contains Zero Vector

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$. 
Let $A \subseteq X$ be an absorbing subset of $X$. 
Then:
:$\mathbf 0_X \in A$
where $\mathbf 0_X$ denotes the zero vector in $X$.

Proof:
From the definition of an absorbing subset, there exists $t \in \R_{>0}$ such that ${\mathbf 0}_X \in t A$.
So $\mathbf 0_X \in A$.
{{qed}}
Category:Absorbing Sets
t6y5k1oruhc7kxw5uz1l15faj95w7qp
Theorem: Image under Left-Total Relation is Empty iff Subset is Empty

Let $\RR \subseteq S \times T$ be a left-total relation.
Let $A \subseteq S$.
Then:
:$\RR \sqbrk A = \O$ {{iff}} $A = \O$

Proof:
=== Necessary Condition ===
We prove the contrapositive statement:
:$A \ne \O \implies \RR \sqbrk A \ne \O$
Let $s \in A$.
By definition of left-total relation:
:$\exists t \in T : \tuple{s, t} \in \RR$
By definition of image:
:$\exists t \in T : t \in \RR \sqbrk A$
Hence:
:$\RR \sqbrk A \ne \O$
The result follows from Rule of Transposition.
{{qed|lemma}}
Theorem: Minkowski Functional of Convex Absorbing Set is Positive Homogeneous

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $A$ be a convex absorbing set. 
Let $\mu_A$ be the Minkowski functional of $A$. 
Then $\mu_A$ is positive homogeneous. 
That is, for each $t \ge 0$ we have:
:$\map {\mu_A} {t x} = t \map {\mu_A} x$

Proof:
From Absorbing Set in Vector Space contains Zero Vector, we have ${\mathbf 0}_X \in A$. 
So $\map {\mu_A} {\mathbf 0_X} = 0$.
So the claim clearly holds for $t = 0$.
Now take $t > 0$. 
We argue that: 
:$\set {s > 0 : t x \in s C} = t \set {s > 0 : x \in s C}$
We have: 
:$s \in \set {s > 0 : t x \in s C}$
{{iff}} $s > 0$ and:
:$t x \in s C$
This is equivalent to: 
:$x \in \paren {\dfrac s t} C$
which is equivalent to: 
:$\dfrac s t \in \set {s > 0 : x \in s C}$
Hence we deduce: 
:$\set {s > 0 : t x \in s C} = t \set {s > 0 : x \in s C}$
From Multiple of Infimum, we obtain: 
:$\map {\mu_C} {t x} = t \map {\mu_C} x$ 
{{qed}}
Category:Minkowski Functionals
hcvqe1ihr9o32xpj5fi0nu3tl60vxjs
Theorem: Convex Subset of Topological Vector Space containing Zero Vector in Interior is Absorbing Set

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \tau}$ be a topological vector space over $\GF$. 
Let $C \subseteq X$ be a convex set such that ${\mathbf 0}_X \in C^\circ$, where $C^\circ$ denotes the interior of $C$. 
Then $C$ is an absorbing set.

Proof:
Let $x \in X$. 
Let $V$ be an open neighborhood of ${\mathbf 0}_X$ contained in $C$. 
Then from Multiple of Vector in Topological Vector Space Converges, we have: 
:$\ds \frac x n \to {\mathbf 0}_X$
So by the definition of a convergent sequence, for some $N \in \N$ we have: 
:$\ds \frac x N \in V$
Then: 
:$\ds x \in N V \subseteq N C$
Since $x \in X$ was arbitrary, we can apply Characterization of Convex Absorbing Set in Vector Space and obtain that: 
:$C$ is absorbing set.
{{qed}}
Category:Absorbing Sets
Category:Topological Vector Spaces
Category:Convex Sets (Vector Spaces)
cfh7ci07jga3yg7fix9jl5oumkpqi6n
Theorem: Minkowski Functional of Open Convex Set containing Zero Vector in Topological Vector Space recovers Set

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C \subseteq X$ be an open convex set with ${\mathbf 0}_X \in C$. 
From Convex Subset of Topological Vector Space containing Zero Vector in Interior is Absorbing Set, $C$ is absorbing.
Let $\mu_C$ be the Minkowski functional of $C$. 
Then we have: 
:$C = \set {x \in X : \map {\mu_C} x < 1}$

Proof:
From Convex Absorbing Set contained between Sets in terms of Minkowski Functional, we have: 
:$\set {x \in X : \map {\mu_C} x < 1} \subseteq C$
Conversely, suppose that $x \in C$. 
From Multiple of Vector in Topological Vector Space Converges, we have: 
:$\paren {1 + \dfrac 1 n} x \to x$
From the definition of a convergent sequence, we have: 
:$\paren {1 + \dfrac 1 N} x \in C$
for some $N \in \N$. 
Then: 
:$x \in \dfrac 1 {1 + \dfrac 1 N} C$
So, by the definition of the Minkowski functional, we have: 
:$\map {\mu_A} x \le \dfrac 1 {1 + \dfrac 1 N} < 1$
{{qed}}
Category:Minkowski Functionals
0yh9xlvgsprwb15wqj0flpye96yqlh0
Theorem: Convex Absorbing Set contained between Sets in terms of Minkowski Functional

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C$ be a convex absorbing set.
Let $\mu_C$ be the Minkowski functional of $C$. 
Then we have: 
:$\set {x \in X : \map {\mu_C} x < 1} \subseteq C \subseteq \set {x \in X : \map {\mu_C} x \le 1}$

Proof:
Let $x \in X$ be such that $\map {\mu_C} x < 1$.
Then: 
:$\inf \set {t > 0 : \dfrac x t \in C} < 1$
So there exists $t < 1$ such that $x \in t C$.
From Absorbing Set in Vector Space contains Zero Vector, we have that ${\mathbf 0}_X \in C$. 
So, we have, since $C$ is convex: 
:$x = x + \paren {1 - t} {\mathbf 0}_X \in t C + \paren {1 - t} C \subseteq C$
So $x \in C$.
So we have: 
:$\set {x \in X : \map {\mu_C} x < 1} \subseteq C$
Now let $x \in C$.
We clearly have: 
:$1 \in \set {t > 0 : \dfrac x t \in C}$
So:
:$\map {\mu_C} x = \inf \set {t > 0 : \dfrac x t \in C} \le 1$
Hence we obtain the inclusion: 
:$C \subseteq \set {x \in X : \map {\mu_C} x \le 1}$
{{qed}}
Category:Minkowski Functionals
duo96da0tp0h25ofg71qeifg3rx24oh
Theorem: Real Linear Functional is Real Part of Unique Linear Functional

Let $X$ be a vector space over $\C$. 
Let $g : X \to \R$ be a $\R$-linear functional.
Then there exists a unique $\C$-linear functional $f : X \to \C$ such that: 
:$\map g x = \map \Re {\map f x}$ 
for each $x \in X$. 
Further: 
:$\map f x = \map g x - i \map g {i x}$

Proof:
Define $f : X \to \C$ by: 
:$\map f x = \map g x - i \map g {i x}$
for each $x \in X$. 
Then for $\lambda, \mu \in \R$ and $x, y \in X$ we have: 
{{begin-eqn}}
{{eqn	| l = \map f {\lambda x + \mu y}
		| r = \map g {\lambda x + \mu y} - i \map g {i \paren {\lambda x + \mu y} } 
}}
{{eqn	| r = \lambda \map g x + \mu \map g x - i \lambda \map g {i x} - i \mu \map g {i x}
		| c = since $g$ is $\R$-linear
}}
{{eqn	| r = \lambda \map f x + \mu \map f y
}}
{{end-eqn}}
So $f$ is $\R$-linear. 
To show that $f$ is $\C$-linear, we need to show that:
:$\map f {i x} = i \map f x$ 
for each $x \in X$. 
We have: 
{{begin-eqn}}
{{eqn	| l = \map f {i x}
		| r = \map g {i x} - i \map g {-x}
}}
{{eqn	| r = \map g {i x} + i \map g x
}}
{{eqn	| r = i \paren {\map g x - i \map g {i x} }
}}
{{eqn	| r = i \map f x
}}
{{end-eqn}}
Then for $\alpha + i\beta, \gamma + i\delta \in \C$ and $x, y \in X$ we have: 
{{begin-eqn}}
{{eqn	| l = \map f {\paren {\alpha + i \beta} x + \paren {\gamma + i \delta} y}
		| r = \map f {\alpha x} + \map f {i \beta x} + \map f {\gamma y} + \map f {i \delta y}
}}
{{eqn	| r = \alpha \map f x + \beta \map f {i x} + \gamma \map f y + \delta \map f {i y}
}}
{{eqn	| r = \alpha \map f x + i\beta \map f x + \gamma \map f y + i \delta \map f y
}}
{{eqn	| r = \paren {\alpha + i \beta} \map f x + \paren {\gamma + i \delta} \map f y
}}
{{end-eqn}}
So $f : X \to \C$ is a linear functional with:
:$\map g x = \map \Re {\map f x}$
Further, from Linear Functional on Complex Vector Space is Uniquely Determined by Real Part, we have that $f : X \to \C$ is unique.
{{qed}}
Category:Linear Functionals
gdq6lolzo8djq5wl2p4etaccr469ovh
Theorem: Realification of Normed Dual is Isometrically Isomorphic to the Normed Dual of Realification

Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\C$. 
Let $\struct {X_\R, \norm {\, \cdot \,} }$ be the realification of $\struct {X, \norm {\, \cdot \,} }$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual of $\struct {X, \norm {\, \cdot \,} }$.
Let $\struct {X^\ast_\R, \norm {\, \cdot \,}_{X^\ast_\R} }$ be the normed dual of $\struct {X_\R, \norm {\, \cdot \,} }$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }_\R$ be the realification of $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$.
Then $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }_\R$ and $\struct {X^\ast_\R, \norm {\, \cdot \,}_{X^\ast} }$ are isometrically isomorphic.
Further $T : \struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }_\R \to \struct {X^\ast_\R, \norm {\, \cdot \,}_{X^\ast} }$ defined by: 
:$T f = \map \Re f$
is an isometric isomorphism.

Proof:
We first need to show that if $f \in X^\ast$, then $T f = \map \Re f \in X^\ast_\R$.
From Real Part of Linear Functional is Linear Functional, we have that $\map \Re f : X \to \R$ is $\R$-linear.
We just need to show that $\map \Re f$ is bounded. 
We have for each $x \in X$:
{{begin-eqn}}
{{eqn	| l = \cmod {\map \Re {\map f x} }
		| r = \sqrt {\paren {\map \Re {\map f x} }^2}
}}
{{eqn	| o = \le
		| r = \sqrt {\paren {\map \Re {\map f x} }^2 + \paren {\map \Im {\map f x} }^2}
}}
{{eqn	| r = \cmod {\map f x}
}}
{{eqn	| o = \le
		| r = \norm f_{X^\ast} \norm x
		| c = Fundamental Property of Norm on Bounded Linear Functional
}}
{{end-eqn}}
So we have that: 
:$\map \Re f$ is bounded
with: 
:$\norm {\map \Re f}_{X^\ast_\R} \le \norm f_{X^\ast}$
We want to show that: 
:$\norm {\map \Re f}_{X^\ast_\R} = \norm f_{X^\ast}$
for each $f \in X^\ast$. 
Let $f \in X^\ast$.
Let $\sequence {u_n}_{n \in \N}$ be a sequence with $\norm {u_n} = 1$ and:
:$\ds \norm f_{X^\ast} - \frac 1 n \le \cmod {\map f {u_n} } \le \norm f_{X^\ast}$ 
so that $\cmod {\map f {u_n} } \to \norm f_{X^\ast}$.
Pick $\alpha_n \in \C$ with $\cmod {\alpha_n} = 1$ such that $\cmod {\map f {u_n} } = \alpha_n \map f {u_n}$.
Since $f : X \to \C$ is $\C$-linear, we have $\alpha_n \map f {u_n} = \map f {\alpha_n u_n}$. 
So we have $\map \Re {\map f {\alpha_n u_n} } = \cmod {\map f {u_n} }$.
Then: 
:$\map \Re {\map f {\alpha_n u_n} } \to \norm f_{X^\ast}$
while: 
:$\norm {\alpha_n u_n} = 1$ for each $n \in \N$.
This gives: 
:$\norm f_{X^\ast} \le \norm {\map \Re f}_{X^\ast_\R}$
so that: 
:$\norm {\map \Re f}_{X^\ast_\R} = \norm f_{X^\ast}$
Finally, we show that $T$ is surjective.
This is given by Bounded Real-Valued Linear Functional is Real Part of Unique Bounded Complex-Valued Linear Functional. 
{{qed}}
Category:Realifications of Complex Vector Spaces
Category:Normed Dual Spaces
Category:Isometric Isomorphisms (Normed Vector Spaces)
n18n80zzf7n6tsnvnnlp2n2ztvu6u7f
Theorem: Primitive of Reciprocal of a x squared + b by Root of c x squared + d

:$\ds \int \dfrac {\d x} {\paren {a x^2 + b} \sqrt {c x^2 + d} } = \begin {cases}
\dfrac 1 {\sqrt {b \paren {a d - b c} } } \arctan \dfrac {x \sqrt {a d - b c} } {\sqrt {b \paren {c x^2 + d} } } + C & : a d > b c \\
\dfrac 1 {2 \sqrt {b \paren {a d - b c} } } \ln \size {\dfrac {\sqrt {b \paren {c x^2 + d} } + x \sqrt {b c - a d} } {\sqrt {b \paren {c x^2 + d} } - x \sqrt {b c - a d} } } + C & : b c > a d
\end {cases}$

Proof:
=== Case $1$: $a d > b c$ ===
{{:Primitive of Reciprocal of a x squared + b by Root of c x squared + d/a d greater than b c}}{{qed|lemma}}
Theorem: Primitive of Reciprocal of a x squared + b by Root of c x squared + d/a d greater than b c

:$\ds \int \dfrac {\d x} {\paren {a x^2 + b} \sqrt {c x^2 + d} } = \dfrac 1 {\sqrt {b \paren {a d - b c} } } \arctan \dfrac {x \sqrt {a d - b c} } {\sqrt {b \paren {c x^2 + d} } } + C$

Proof:
=== Lemma ===
{{:Primitive of Reciprocal of a x squared + b by Root of c x squared + d/Lemma}}
{{ProofWanted}}
Theorem: Primitive of Reciprocal of a x squared + b by Root of c x squared + d/b c greater than a d

:$\ds \int \dfrac {\d x} {\paren {a x^2 + b} \sqrt {c x^2 + d} } = \dfrac 1 {2 \sqrt {b \paren {a d - b c} } } \ln \size {\dfrac {\sqrt {b \paren {c x^2 + d} } + x \sqrt {b c - a d} } {\sqrt {b \paren {c x^2 + d} } - x \sqrt {b c - a d} } } + C$

Proof:
=== Lemma ===
{{:Primitive of Reciprocal of a x squared + b by Root of c x squared + d/Lemma}}
{{ProofWanted}}
Theorem: Minkowski Functional of Convex Absorbing Set is Sublinear Functional

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $A$ be a convex absorbing set. 
Let $\mu_A$ be the Minkowski functional of $A$. 
Then $\mu_A$ is a sublinear functional.

Proof:
This follows from Minkowski Functional of Convex Absorbing Set is Positive Homogeneous and Minkowski Functional of Convex Absorbing Set is Sublinear.
{{qed}}
Category:Minkowski Functionals
Category:Sublinear Functionals
7m4ybn4w9pnm8v4lmuvohqpwfjg21y2