avewright/proofwiki-math huggingface dataset:
Theorem: Length of Legendre Polynomial

Let $\map {P_n} x$ denote the '''Legendre polynomial of order $n$'''.
Let $\norm {\map {P_n} x}$ denote the '''length''' of $\map {P_n} x$.
Then:
:$\norm {\map {P_n} x} := \sqrt {\dfrac 2 {2 n + 1} }$

Proof:
Applying Bonnet's Recursion Formula for $n - 1$:
:$n \map {P_n} x = \paren {2 n - 1} x \map {P_{n - 1} } x - \paren {n - 1} \map {P_{n - 2} } x$
so:
:$\map {P_n} x = \dfrac {2 n - 1} n x \map {P_{n - 1} } x - \dfrac {n - 1} n \map {P_{n - 2} } x$
Substituting for $\map {P_n} x$:
{{begin-eqn}}
{{eqn | l = \norm {\map {P_n} x}^2
      | r = \int_{-1}^1 \map {P_n} x \map {P_n} x \rd x
      | c = 
}}
{{eqn | r = \int_{-1}^1 \map {P_n} x \paren {\frac {2 n - 1} n x \map {P_{n - 1} } x - \frac {n - 1} n \map {P_{n - 2} } x} \rd x
      | c = 
}}
{{eqn | r = \frac {2 n - 1} n \int_{-1}^1 x \map {P_n} x \map {P_{n - 1} } x \rd x - \frac {n - 1} n \int_{-1}^1 \map {P_n} x \map {P_{n - 2} } x \rd x
      | c = Linear Combination of Definite Integrals
}}
{{end-eqn}}
From Orthogonality of Legendre Polynomials:
:$\ds \int_{-1}^1 \map {P_n} x \map {P_m} x \rd x = 0 \iff n \ne m$
so:
:$\ds (1): \quad \norm {\map {P_n} x}^2 = \frac {2 n - 1} n \int_{-1}^1 x \map {P_n} x \map {P_{n - 1} } x \rd x$
From Bonnet's Recursion Formula:
:$x \map {P_n} x = \dfrac {n + 1} {2 n + 1} \map {P_{n + 1} } x + \dfrac n {2 n + 1} \map {P_{n - 1} } x$
Substituting for $x \map {P_n} x$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \norm {\map {P_n} x}^2
      | r = \frac {2 n - 1} n \frac {n + 1} {2 n + 1} \int_{-1}^1 \map {P_{n + 1} } x \map {P_{n - 1} } x \rd x + \frac {2 n - 1} {2 n + 1} \int_{-1}^1 \map {P_{n - 1} } x \map {P_{n - 1} } x \rd x
      | c = 
}}
{{eqn | r = \frac{2 n - 1} {2 n + 1} \int_{-1}^1 \map {P_{n - 1} } x \map {P_{n - 1} } x \rd x
      | c = 
}}
{{eqn | r = \frac {2 n - 1} {2 n + 1} \norm {\map {P_{n - 1} } x}^2
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \norm {\map {P_n} x}^2
      | r = \frac {2 n - 1} {2 n + 1} \norm {\map {P_{n - 1} } x}^2
      | c = 
}}
{{eqn | r = \frac {2 n - 1} {2 n + 1} \frac {2 n - 3} {2 n - 1} \norm {\map {P_{n - 2} } x}^2
      | c = 
}}
{{eqn | r = \cdots
      | c = 
}}
{{eqn | r = \frac {2 n - 1} {2 n + 1} \frac {2 n - 3} {2 n - 1} \frac {2 n - 5} {2 n - 3} \dotsm \frac 3 5 \frac 1 3 \norm {\map {P_0} x}^2
      | c = 
}}
{{end-eqn}}
Most of this cancels out, leaving:
:$\norm {\map {P_n} x}^2 = \dfrac {\norm {\map {P_0} x}^2} {2 n + 1}$
It remains to compute the length of the first Legendre polynomial:
{{begin-eqn}}
{{eqn | l = \norm {\map {P_0} x}^2
      | r = \int_{-1}^1 1 \rd x
      | c = 
}}
{{eqn | r = \bigintlimits x {-1} 1
      | c = Primitive of Constant
}}
{{eqn | r = 2
      | c = 
}}
{{end-eqn}}
Thus:
:$\norm {\map {P_n} x}^2 = \dfrac 2 {2 n + 1}$
and so taking the square root:
:$\norm {\map {P_n} x} = \sqrt {\dfrac 2 {2 n + 1} }$
{{qed}}
Category:Legendre Polynomials
a54c6tuf49gxy6r1tpyh4bymi474p8z
Theorem: Lemniscate of Bernoulli from Tangents to Rectangular Hyperbola

Let $\KK$ be a rectangular hyperbola.
Let $\LL$ be the locus of the foot of the perpendicular from the origin to the tangents to $\KK$.
Then $\LL$ is the '''lemniscate of Bernoulli'''.

Proof:
:600px
{{ProofWanted}}
Theorem: Matroid Bases Satisfy Formulation 7 of Matroid Base Axiom/Lemma 1

Let $n \in \N_{>0}$.
Let $C_1, C_2, \ldots, C_n \in \mathscr C$ satisfy:
:$\forall 0 \le k \le n : C_k \nsubseteq \ds \bigcup_{i \ne k} C_i$
Let:
:$A \subseteq S : \size A < n$
Let $r = \size A$.
Then:
:$\ds \exists D_1, \ldots, D_{n - r} \in \mathscr C : \bigcup_{i = 1}^{n - r} D_i \subseteq \paren{\bigcup_{i = 1}^{n} C_i} \setminus A$

Proof:
=== Case 1 : $n = 1$ ===
Let $n = 1$.
Hence $\size A = 0$.
From Cardinality of Empty Set:
:$A = \O$
It follows that $C_1$ suffices for $D_1$.
{{qed|lemma}}
Theorem: Mechanical Advantage of Type 3 Lever is Less than 1

Let $M$ be a type $3$ lever.
Then the mechanical advantage of $M$ is less than $1$.
Hence, instead of amplifying the force applied, a type $3$ lever amplifies the velocity ratio.

Proof:
From Principle of Lever:
:$\text {MA} = \dfrac b a$
where:
:$b$ is the distance of the effort from the fulcrum
:$a$ is the distance of the load from the fulcrum.
But in a type $3$ lever, the effort acts between the load and the fulcrum.
That is:
:$a > b$
and hence the result.
{{qed}}
Theorem: Independent Subset Contains No Dependent Subset

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $X \subseteq S$ be any independent subset of $M$.
Then:
:No dependent subset $D$ of $M$ is a subset of $X$.

Proof:
By definition of independent subset:
:$X \in \mathscr I$
By definition of matroid, specifically matroid axiom $( \text I 2)$:
:$\forall Y \subseteq X : Y \in \mathscr I$
By definition of dependent subset:
:$\forall Y \subseteq X : Y$ is not a dependent subset
{{qed}}
Category:Matroid Independent Subsets
Category:Matroid Dependent Subsets
Category:Independent Subset Contains No Dependent Subset
kinwgwcdmwa6qxgedwpie8xf05hc4nx
Theorem: Independent Subset Contains No Dependent Subset/Corollary 1

Let $B \subseteq S$ be any base of $M$.
Then:
:No dependent subset $D$ of $M$ is a subset of $B$.

Proof:
By definition of matroid base:
:$B$ is an independent subset of $M$
From Independent Subset Contains No Dependent Subset:
:No dependent subset $D$ of $M$ is a subset of $B$.
{{qed}}
Category:Independent Subset Contains No Dependent Subset
8f6pz3re1rnjnbt5gg4yznwcxg61tvh
Theorem: Independent Subset Contains No Dependent Subset/Corollary 2

Let $X \subseteq S$ be any independent subset of $M$.
Then:
:No circuit $C$ of $M$ is a subset of $X$.

Proof:
Let $C$ be a circuit of $M$.
By definition of matroid circuit:
:$C$ is a dependent subset of $M$
From Independent Subset Contains No Dependent Subset:
:$C$ is not a subset of $X$.
The result follows.
{{qed}}
Category:Independent Subset Contains No Dependent Subset
blh296a5mwoh80eyt1356eq39y7gy0v
Theorem: Independent Subset Contains No Dependent Subset/Corollary 3

Let $B \subseteq S$ be any base of $M$.
Then:
:No circuit $C$ of $M$ is a subset of $B$.

Proof:
By definition of matroid base:
:$B$ is an independent subset of $M$
From Independent Subset Contains No Circuit:
:No circuit $C$ of $M$ is a subset of $B$.
{{qed}}
Category:Independent Subset Contains No Dependent Subset
rcfy54uuv91ecynli40mjz9j12l5m43
Theorem: Subset Intersection Set Difference is Empty Iff Subset of Second Set

Let $S$ and $T$ be sets.
Let $A \subseteq S$.
Then: 
:$A \cap S \setminus T = \O$ {{iff}} $A \subseteq T$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = A \cap \paren {S \setminus T} 
      | r = \paren {A \cap S} \setminus T
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | r = A \setminus T
      | c = Intersection with Subset is Subset
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = A \cap \paren{S \setminus T}
      | r = \O
}}
{{eqn | ll = \leadstoandfrom
      | l = A \setminus T
      | r = \O
      | c = As $A \cap \paren{S \setminus T} = A \setminus T$
}}
{{eqn | ll = \leadstoandfrom
      | l = A
      | o = \subseteq
      | r = T
      | c = Set Difference with Superset is Empty Set
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Intersection
1ap4ilg8aah44ct4nprmh6sqbwed5bo
Theorem: Negative Slope indicates Line slopes Downward from Left to Right

Let $\LL$ be a straight line with a slope which is negative.
Then $\LL$ slopes downward from left to right.

Proof:
Let $\LL$ have a slope which is negative.
Expressed in slope-intercept form, $\LL$ can be written:
:$y = x \tan \psi + c$
where:
:$\psi$ is the angle between $\LL$ and the $x$-axis
:$c$  is the $y$-intercept.
:420px
By construction:
:$90 \degrees < \psi < 180 \degrees$
Hence by Shape of Tangent Function:
:$\tan \psi < 0$
Hence the result.
{{qed}}
Theorem: Graph of Linear Function of One Variable

Let $f: \R \to \R$ be a linear function of one variable expressed by the equation:
:$\map f x = a_0 + a_1 x$
The graph of $f$ in a cartesian plane consists of a straight line:
:whose $y$-intercept is $a_0$
:whose slope is $a_1$.

Proof:
Expressing $f$ in the form $y = \map f x$, we have:
:$y = a_0 + a_1 x$
Thus it is in the same form as the slope-intercept form of an equation of a straight line in the plane.
Hence the result.
{{qed}}
Theorem: Power of Ideal is Subset

Let $\struct {R, +, \cdot}$ be a ring.
Let $I \subseteq R$ be an ideal.
Let $n \in \Z$ be an integer such that $n \ge 1$.
Let $I^n$ denote the $n$th power of $I$.
Then $I^n$ is a subset of $I$:
:$I^n \subseteq I$

Proof:
Let $n = 1$.
Then by definition of Power of Ideal of Ring:
:$I^1 = I$
Hence by Set is Subset of Itself:
:$I^1 \subseteq I$.
{{qed|lemma}}
Let $n > 1$.
By definition of Power of Ideal of Ring, $I^n$ is an ideal generated by elements of $R$ the form:
:$a_1 \cdots a_n$
where each $a_i \in I$.
From Ideal is Subring, $I$ is a subring of $R$.
Hence {{afortiori}} $I$ is closed under addition.
Hence it suffices to show that such generators of $I^n$ are elements of $I$.
Let $a_1 \cdots a_n \in I^n$ such that each $a_i \in I$.
Then:
:$a_1 \in I$
:$a_2 \cdots a_n \in I$
Hence in particular:
:$a_2 \cdots a_n \in R$
Because:
:$a_1 \in I$
:$a_2 \cdots a_n \in R$
it follows that:
:$a_1 \cdot \paren {a_2 \cdots a_n} \in I$
Thus:
:$a_1 \cdots a_n \in I$
and it follows by definition of subset that:
:$I^n \subseteq I$
{{qed}}
Category:Ideal Theory
Category:Subsets
Category:Power Set
9zbg062anguxyhnwkoeg5tqig7tx7kf
Theorem: Element of Spectrum of Densely-Defined Linear Operator not in Residual Spectrum is Approximate Eigenvalue/Corollary

Let $\struct {\map D T, T}$ be a self-adjoint densely-defined linear operator.

Proof:
Let $\map {\sigma_r} T$ be the residual spectrum of $\struct {\map D T, T}$.
From Self-Adjoint Densely-Defined Linear Operator has Empty Residual Spectrum, we have $\map {\sigma_r} T = \O$. 
Hence we have $\lambda \in \map \sigma T \setminus \map {\sigma_r} T$.
From Element of Spectrum of Densely-Defined Linear Operator not in Residual Spectrum is Approximate Eigenvalue, we therefore have that $\lambda$ is an approximate eigenvalue of $\struct {\map D T, T}$.
{{qed}}
Category:Element of Spectrum of Densely-Defined Linear Operator not in Residual Spectrum is Approximate Eigenvalue
mkcrp3a1pj0qpjuy8tcnb1tcsrnj9nn
Theorem: Logarithmic Integral and Eulerian Logarithmic Integral Differ by Constant

Let $x \in \R$ be a real number such that $x > 2$.
Let $\map \li x$ denote the logarithmic integral of $x$.
Let $\map \Li x$ denote the Eulerian logarithmic integral of $x$.
Then $\map \li x - \map \Li x$ is a constant.

Proof:
{{begin-eqn}}
{{eqn | l = \map \li x - \map \Li x
      | r = \PV_0^x \frac {\d t} {\ln t} - \int_2^x \frac {\d t} {\ln t}
      | c = {{Defof|Logarithmic Integral}}, {{Defof|Eulerian Logarithmic Integral}}
}}
{{eqn | r = \lim_{\varepsilon \mathop \to 0^+} \paren {\int_\varepsilon^{1 - \varepsilon} \frac {\rd t} {\ln t} + \int_{1 + \varepsilon}^x \frac {\rd t} {\ln t} } - \int_2^x \frac {\d t} {\ln t}
      | c = {{Defof|Cauchy Principal Value}}
}}
{{eqn | r = \lim_{\varepsilon \mathop \to 0^+} \paren {\int_\varepsilon^{1 - \varepsilon} \frac {\rd t} {\ln t} + \int_{1 + \varepsilon}^x \frac {\rd t} {\ln t} } - \int_2^x \frac {\d t} {\ln t}
      | c = 
}}
{{eqn | r = \lim_{\varepsilon \mathop \to 0^+} \paren {\int_\varepsilon^{1 - \varepsilon} \frac {\rd t} {\ln t} + \int_{1 + \varepsilon}^2 \frac {\rd t} {\ln t} } + \int_2^x \frac {\rd t} {\ln t} - \int_2^x \frac {\d t} {\ln t}
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = \lim_{\varepsilon \mathop \to 0^+} \paren {\int_\varepsilon^{1 - \varepsilon} \frac {\rd t} {\ln t} + \int_{1 + \varepsilon}^2 \frac {\rd t} {\ln t} }
      | c = 
}}
{{end-eqn}}
{{finish|Is it sufficient just to state "which is obviously constant" or would more work be needed to establish what that constant is?}}
Theorem: Matroid Bases Satisfy Formulation 7 of Matroid Base Axiom/Lemma 2

Let $m \in \Z: m \ge 2$.
Let $D_1, D_2, \ldots, D_m \in \mathscr C$ satisfy:
:$\ds \forall 0 \le i \le m : D_i \nsubseteq \bigcup_{j = 1, j \ne i}^m D_j$
Let $X, Y \subseteq S$:
:$\ds \bigcup_{i = 1}^m D_i \subseteq Y \setminus X$
Let $x \in S \setminus X$.
Then:
:$\exists E_1, E_2, \ldots, E_{m - 1} \in \mathscr C$:
::* $\quad \ds \forall 0 \le i \le m - 1 : E_i \nsubseteq \bigcup_{j = 1,j \ne i}^{m - 1} E_j$
::* $\quad \ds \bigcup_{i = 1}^{m-1} E_i \subseteq Y \setminus \paren{X \cup \set x}$

Proof:
=== Case 1: $x$ is not in any $D_i$ ===
Let:
:$\forall 1 \le i \le m : x \notin D_i$
We have:
{{begin-eqn}}
{{eqn | l = \bigcup_{i = 1}^m D_i
      | r = \bigcup_{i = 1}^m \paren{D_i \setminus \set x}
      | c = Set Difference with Disjoint Set
}}
{{eqn | r = \paren{\bigcup_{i = 1}^m D_i} \setminus \set x
      | c = Set Difference is Right Distributive over Union
}}
{{eqn | o = \subseteq
      | r = \paren{Y \setminus X} \setminus \set x
      | c = {{hypothesis}}
}}
{{eqn | r = Y \setminus \paren{X \cup \set x}
      | c = Set Difference with Union
}}
{{end-eqn}}
Furthermore:
:$\ds \forall 0 \le i \le m - 1 : D_i \nsubseteq \ds \bigcup_{i = 1, j \ne i}^{m - 1} D_j$
Hence $D_1, D_2, \ldots, D_{m - 1}$ suffice as the required $E_1, E_2, \ldots, E_{m - 1}$.
{{qed|lemma}}
Theorem: Form of Logit for Logistic Curve

Let $p$ denote the probability of the occurrence of an event.
Let $p$ satisfy a logistic relationship with an explanatory variable $x$ of the form:
:$p = \dfrac 1 {1 + \map \exp {-\paren {\alpha + \beta x} } }$
Let $Y$ be the logit of $p$.
Then:
:$Y = \alpha + \beta x$

Proof:
By definition, the logit of $p$ is given by:
:$Y = \map \ln {\dfrac p {1 - p} }$
In order to simplify the algebra, let $c = -\paren {\alpha + \beta x}$.
Then we have:
{{begin-eqn}}
{{eqn | l = Y
      | r = \map \ln {\dfrac {\frac 1 {1 + \exp c} } {1 - \frac 1 {1 + \exp c} } }
      | c = 
}}
{{eqn | r = \map \ln {\dfrac {\frac 1 {1 + \exp c} } {\frac {1 + \exp c - 1} {1 + \exp c} } }
      | c = putting everything in the lower fraction over a common denominator
}}
{{eqn | r = \map \ln {\dfrac 1 {\exp c} }
      | c = simplification, and multiplying top and bottom by $1 + \exp c$
}}
{{eqn | r = -\map \ln {\exp c}
      | c = Logarithm of Reciprocal
}}
{{eqn | r = -c
      | c = {{Defof|Logarithm}}
}}
{{eqn | r = \alpha + \beta x
      | c = substituting for $c$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 4

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Let $M = \struct{S, \mathscr I}$ where:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
Then $M$ satisfies matroid axiom $(\text I 1)$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map \rho \O
      | r = 0
      | c = Rank axiom $(\text R 1)$
}}
{{eqn | r = \card \O
      | c = Cardinality of Empty Set
}}
{{end-eqn}}
So:
:$\O \in \mathscr I$
Hence:
:$M$ satisfies matroid axiom $(\text I 1)$.
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Let $M = \struct{S, \mathscr I}$ where:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
Then $M$ satisfies matroid axiom $(\text I 2)$.

Proof:
Let
:$X \in \mathscr I$
{{AimForCont}}
:$\exists Y \subseteq X : Y \notin \mathscr I$
Let:
:$Y_0 \subseteq X : \card {Y_0} = \max \set{\card Z : Z \subseteq X \land Z \notin \mathscr I}$
By definition of $\mathscr I$:
:$Y_0 \notin \mathscr I \leadsto \map \rho {Y_0} \ne \card {Y_0}$
From Lemma 2:
:$\map \rho {Y_0} < \card {Y_0}$
As $X \in \mathscr I$ then:
:$Y_0 \ne X$
Hence:
:$Y_0$ is a proper subset of $X$
From Set Difference with Proper Subset:
:$X \setminus Y_0 \ne \O$
Let $y \in X \setminus Y_0$.
We have:
{{begin-eqn}}
{{eqn | l = \card {Y_0} + 1
      | r = \card {Y_0 \cup \set y}
      | c = Corollary of Cardinality of Set Union
}}
{{eqn | r = \map \rho {Y_0 \cup \set y}
      | c = As $\card {Y_0} = \max \set{\card Z : Z \subseteq X \land Z \notin \mathscr I}$
}}
{{eqn | o = \le
      | r = \map \rho {Y_0} + 1
      | c = Rank axiom $(\text R 2)$
}}
{{eqn | o = <
      | r = \card {Y_0} + 1
      | c = As $\map \rho {Y_0} < \card {Y_0}$
}}
{{end-eqn}}
This is a contradiction.
So:
:$\forall Y \subseteq X : Y \in \mathscr I$
Hence:
:$M$ satisfies matroid axiom $(\text I 2)$.
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Let $M = \struct{S, \mathscr I}$ where:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
Then $M$ satisfies matroid axiom $(\text I 2)$.

Proof:
We prove the contrapositive statement:
:$\forall X, Y \subseteq S: Y \notin \mathscr I \land Y \subseteq X \implies X \notin \mathscr I$
Let $X, Y \subseteq S : Y \notin \mathscr I$ and $Y \subseteq X$.
====== Case 1: $Y = X$ ======
Let $Y = X$.
Then $X \notin \mathscr I$.
{{qed|lemma}}
====== Case 2: $Y \subset X$ ======
Let $Y \subset X$.
By definition of $\mathscr I$:
:$\map \rho Y \neq \size Y$
From Lemma 2:
:$\map \rho Y < \size Y$
Let:
:$X \setminus Y = \set{z_1, z_2, \ldots , z_k}$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X
      | r = \map \rho {Y \cup \set{z_1, z_2, \ldots, z_k} }
}}
{{eqn | o = \le
      | r = \map \rho Y + k
      | c = Repeated application of rank axiom $(\text R 2)$
}}
{{eqn | o = <
      | r = \size Y + k
      | c = Lemma 2
}}
{{eqn | r = \size Y + \size {\set {z_1, z_2, \ldots, z_k} }
      | c = {{Defof|Cardinality of Finite Set}}
}}
{{eqn | r = \size {Y \cup \set {z_1, z_2, \ldots, z_k} }
      | c = Corollary of Cardinality of Set Union
}}
{{eqn | r = \size X
}}
{{end-eqn}}
It follows that $X \notin \mathscr I$.
{{qed|lemma}}
In either case we have:
:$X \notin \mathscr I$
This proves the contrapositive statement:
:$\forall X, Y \subseteq S: Y \notin \mathscr I \land Y \subseteq X \implies X \notin \mathscr I$
It follows that $\mathscr I$ satisfies matroid Axiom $(\text I 2)$.
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 6

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Let $M = \struct{S, \mathscr I}$ where:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
Then $M$ satisfies matroid axiom $(\text I 3)$.

Proof:
Let
:$U \in \mathscr I$
:$V \subseteq S$
:$\card U < \card V$
We prove the contrapositive statement:
:$\paren{\forall x \in V \setminus U : U \cup \set x \notin \mathscr I} \implies V \notin \mathscr I$
Let:
:$\forall x \in V \setminus U: U \cup \set x \notin \mathscr I$
That is, by definition of $\mathscr I$:
:$\forall x \in V \setminus U : \map \rho {U \cup \set x} \ne \card {U \cup \set x}$
We have:
{{begin-eqn}}
{{eqn | l = \card V
      | o = >
      | r = \card U
      | c = {{hypothesis}}
}}
{{eqn | r = \map \rho U
      | c = As $U \in \mathscr I$
}}
{{eqn | r = \map \rho {U \cup V}
      | c = Lemma 3
}}
{{eqn | o = \ge
      | r = \map \rho V
      | c = Lemma 1
}}
{{end-eqn}}
Hence:
:$V \notin \mathscr I$
It follows:
:$M$ satisfies matroid axiom $(\text I 3)$.
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 7

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Let $M = \struct{S, \mathscr I}$ where:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
Then $M$ satisfies matroid axiom $(\text I 4)$.

Proof:
It is now proved that $\mathscr I$ satisifes the matroid Axiom $(\text I 4)$:
{{begin-axiom}}
{{axiom | n = \text I 4
        | q = \forall U, V \in \mathscr I
        | mr= \size U = \size V + 1 \implies \exists x \in U \setminus V : V \cup \set x \in \mathscr I
}}
{{end-axiom}}
Let $X, Y \in \mathscr I$ such that $\size Y = \size X + 1$.
Let:
:$X = \set {x_1, x_2, \ldots, x_q, z_{q + 1}, \ldots, z_k}$
and
:$Y = \set {x_1, x_2, \ldots, x_q, y_{q + 1}, \ldots, y_k, y_{k + 1}}$
where $\forall i \in \set {q + 1, \ldots, k}$ and $\forall j \in \set {q + 1, \ldots, k + 1}$
:$z_i \neq y_j$
{{AimForCont}}:
:$\forall j \in \set {q + 1, \ldots, k + 1}: X \cup \set{y_j} \notin \mathscr I$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set{y_{q + 1}, \ldots, y_{k + 1} } }
      | r = \map \rho X
      | c = Lemma 3
}}
{{eqn | r = \size X
      | c = as $X \in \mathscr I$
}}
{{eqn | o = <
      | r = \size Y
      | c = {{hypothesis}}
}}
{{end-eqn}}
Now:
:$Y \subseteq X \cup \set{y_{q + 1}, \ldots, y_{k + 1} }$
From Lemma 1:
:$\map \rho Y \le \map \rho {X \cup \set{y_{q + 1}, \ldots, y_{k + 1} } } < \size Y$
This contradicts the assumption that $Y \in \mathscr I$.
Hence:
:$\exists j \in \set {q + 1, \ldots, k + 1}: X \cup \set{y_j} \in \mathscr I$
It follows that $\mathscr I$ satisfies matroid Axiom $(\text I 4)$.
Theorem: Operator with Zero Numerical Range is Zero Operator

Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\C$. 
Let $\norm {\, \cdot \,}$ be the inner product norm on $\struct {\HH, \innerprod \cdot \cdot}$.
Let $\struct {\map D T, T}$ be a densely-defined linear operator on $\HH$ such that:
:$\map W T = \set 0$
where $\map W T$ is the numerical range of $T$. 
Then $T = 0$.

Proof:
Let $x, y \in \map D T$. 
Since $\map W T = \set 0$, we have:
:$\innerprod {\map T {x + y} } {x + y} = \innerprod {T x} x = \innerprod {T y} y = 0$
From Inner Product is Sesquilinear, we have:
:$\innerprod {T x} x + \innerprod {T x} y + \innerprod {T y} x + \innerprod {T y} y = 0$
That is:
:$\innerprod {T x} y = -\innerprod {T y} x$
Similarly, replacing $y$ with $i y$ and applying Inner Product is Sesquilinear, we have:
:$-i \innerprod {T x} y = -\innerprod {\map T {i y} } x$
Since $T$ is linear, we have:
:$\innerprod {T x} y = \innerprod {T y} x$
Hence:
:$\innerprod {T x} y = -\innerprod {T x} y$
This gives:
:$\innerprod {T x} y = 0$ for all $x, y \in \map D T$.
That is:
:$T x \in \map D T^\bot$ for all $x \in \map D T$
where $\map D T^\bot$ is the orthocomplement of $\map D T$.
From Linear Subspace Dense iff Zero Orthocomplement, we have $\map D T^\bot = \set 0$.
Hence:
:$T x = 0$ for all $x \in \map D T$.
{{qed}}
Theorem: Operator with Zero Numerical Range is Zero Operator/Corollary

Let $\DD$ be a dense linear subspace of $\HH$. 
Let $\struct {\DD, T}$ and $\struct {\DD, S}$ be densely-defined linear operators on $\HH$ such that:
:$\innerprod {T x} x = \innerprod {S x} x$ for each $x \in \DD$.
Then $T = S$.

Proof:
From Inner Product is Sesquilinear, we have:
:$\innerprod {\paren {T - S} x} x = 0$ for each $x \in \DD$.
Applying Operator with Zero Numerical Range is Zero Operator to the densely-defined linear operator $\struct {\DD, T - S}$, we have:
:$T - S = 0$
That is:
:$T = S$
{{qed}}
Theorem: Square of Inner Product Norm of Sum

Let $\struct {X, \innerprod \cdot \cdot}$ be an inner product space. 
Let $\norm {\, \cdot \,}$ be the inner product norm. 
Let $x, y \in X$.
Then, we have:
:$\norm {x + y}^2 = \norm x^2 + 2 \map \Re {\innerprod x y} + \norm y^2$

Proof:
{{begin-eqn}}
{{eqn	| l = \norm {x + y}^2
		| r = \innerprod {x + y} {x + y}
		| c = {{Defof|Inner Product Norm}}
}}
{{eqn	| r = \innerprod x x + \innerprod y x + \innerprod x y + \innerprod y y
		| c = Inner Product is Sesquilinear
}}
{{eqn	| r = \norm x^2 + \overline {\innerprod x y} + \innerprod x y + \norm y^2
		| c = {{Defof|Inner Product Norm}}, conjugate symmetry of inner product
}}
{{eqn	| r = \norm x^2 + 2 \map \Re {\innerprod x y} + \norm y^2
		| c = Sum of Complex Number with Conjugate
}}
{{end-eqn}}
{{qed}}
Category:Inner Product Spaces
6horvgzkcqkh059jaj1bhamhdoiqexd