Kabelo Moiloa – Mathemafrica

A Linear algebra problem

I have this linear algebra problem in the context of quantum mechanics. Let $\mathbf{f}_\lambda$ be a family of linear operators so to each $\lambda \in \mathbf{R}$ we have a linear operator $\mathbf{f}_\lambda : \mathcal{H} \to \mathcal{H}$ where $\mathcal{H}$ is a complex vector space if one is unfamiliar with functional analysis (like I am) or is a Hilbert space if one is. Let’s suppose that this family is differentiable.

Suppose further that $\mathbf{f}_\lambda$ is always a Hermitian operator. Suppose that $\mathbf{f}_\lambda$ has a discrete spectrum of eigenvalues $f_1(\lambda), f_2(\lambda), \cdots$ . I need to show the following:

Theorem

$D_\lambda f_n(\lambda) = \left\langle f_n(\lambda)\right|D_\lambda \mathbf{f}_\lambda \left|f_n(\lambda) \right\rangle$

Now here is a “proof,” it is not quite rigorous since there are probably a lot of technical details regarding functional analysis that I’m missing out on but:

Proof We begin by differentiating the eigenvalue equation $\mathbf{f}_\lambda \left| f_n(\lambda) \right\rangle = f_n(\lambda) \left| f_n(\lambda) \right\rangle$ with respect to $\lambda$ using the product rule:

$(D_\lambda \mathbf{f}_\lambda) \left|f_n(\lambda)\right\rangle + \mathbf{f}_\lambda (D_\lambda \left| f_n(\lambda) \right \rangle) = (D_\lambda f_n(\lambda)) \left| f_n(\lambda) \right \rangle + f_n(\lambda) (D_\lambda \left| f_n(\lambda) \right\rangle)$

After multiplying by $\left\langle f_n(\lambda) \right|$ and rearranging terms we have the following:

$\left\langle f_n(\lambda)\right| D_\lambda f_n(\lambda) \left|f_n(\lambda)\right\rangle = \left\langle f_n(\lambda)\right| D_\lambda \mathbf{f}_\lambda \left| f_n(\lambda) \right\rangle + \left\langle f_n(\lambda)\right| \mathbf{f}_\lambda (D_\lambda \left|f_n(\lambda)\right\rangle) - \left\langle f_n(\lambda)\right| f_n(\lambda) (D_\lambda \left|f_n(\lambda)\right\rangle)$

Now we can take the adjoint of both sides of the eigenvalue equation to get that $\langle f_n(\lambda)| \mathbf{f}_\lambda = \langle f_n(\lambda)| f_n(\lambda)$ since $f_n(\lambda)^* = f_n(\lambda)$ because the eigenvalues of a normal operator are real.…

By Kabelo Moiloa| October 12th, 2016|Uncategorized|0 Comments

Dependent Types

This blog post will carry on from the previous one, and introduce dependent types. So what is a dependent type? To motivate the idea let’s talk about equality. Remember that we interpret propositions as types, so if we have $x, y : A$ then the statement “ $x$ is equal to $y$ ” corresponds to some type, let’s call it $x =_A y$ . This type depends on its values, for example we expect to be able to prove (i.e. construct) $3 =_{\mathbb{N}} 3$ , but not to be able to prove $2 =_{\mathbb{N}} 3$ and so we will have an equality type that depends on its values. This idea is also being explored in various programming languages. These languages have a type like $\mathrm{Vec}(x, A)$ , where $l : \mathrm{Vec}(x, A)$ means that $l$ is a list of $x$ elements from the type $A$ . Since the length of the list is part of its type which is known ahead of time, it is impossible to ask questions like, “What is the first element of this empty list?” Indeed dependent types are so powerful that one can write a compiler and be sure that the compiler preserves the meaning of a program.…

By Kabelo Moiloa| October 11th, 2016|Uncategorized|0 Comments

Type Theory, Logic, and Programming

Hello Internet. In this blog post we are going to learn some type theory, which is a field that lies in the intersection of mathematics and computer science. We are eventually going to learn the variant called Martin-Loef Type Theory, or MLTT for short. To motivate it, we are going to try answering the question, “What is a valid program?”

Not every program makes sense, for example what would a program consisting of the single expression x + 2 mean? If we don’t know what x is, then we don’t know what the meaning of that expression is. More importantly, a program can combine expressions that are incompatible with each other. For example, if + is the usual operation that adds two numbers then an expression like "abc" + 5 can’t be given a meaning. To avoid such meaningless programs, we should talk about the different kinds of data and the valid operations on these pieces of data.…

By Kabelo Moiloa| June 19th, 2016|Uncategorized|2 Comments

About Kabelo Moiloa

A Linear algebra problem

Dependent Types

Type Theory, Logic, and Programming