Haar measure
“The Haar Measure assigns an “invariant volume” to subsets of Locally compact topological groups. Thus defining an integral for functions on those groups”
def Haar := sorry
lemma unique_measure_on_the_group (G : compact group) :
... := sorry
lemma l_mul_invariant :
Haar g = Haar(U * g) := sorry
lemma r_mul_invariant :
Haar g = Haar(g * U) := sorry
The Haar probability distribution for finite groups happens to be the uniform distribution.
Examples: The circle group. The sphere group.
---
/-
Haar random unitary U. Apply on |0⟩. Get a random pure state. Initial vector does not matter.
-/
/-
p(ψ) ∈ Haar probability distribution over {|ψ⟩}
-/
Let (G,.) be a locally compact Hausdorff topological group.
The σ-algebra generated by all open subsets of G is called the Borel algebra.
And element of the Borel algebra is called a Borel set.
If g is an element of G and S is a subset of G,
then we define the left and right translates of S by g as follows:
def left_translate (g : G) (S : susbet G) :=
{g * s | s ∈ S}
def right_translate (g : G) (S : susbet G) :=
{s * g | s ∈ S}
/--
The measure μ is right-translation-invariant := μ(Sg) = μ(S)
for every g ∈ G and all Borel sets S ⊆ G.
-/
/--
Haar's theorem: ∃ up to a positive multiplicative constant
a uniquely countably additive, nontrivial measure μ
on the Borel sets S ⊆ G satisfying the following properties:
The measure μ is left-translation-invariant μ(gS) = μ(S)
for every g ∈ G and all Borel sets S ⊆ G.
The measure μ is finite on every compact set: μ(K) < ∞
for all compact K ⊆ G.
The measure μ is outer regular on Borel sets S ⊆ G:
μ(S) = inf{μ(U) | open U, S ⊆ U}
The measure μ is inner regular on open sets U ⊆ G:
μ(S) = sup{μ(U) | compact K, K ⊆ U}
-/