The scalar symbols

noncomputable def CommutingRepetition.VN.Modular.clP (x : ℝ) : ℝ

Clamp to [0, π].

Equations

• CommutingRepetition.VN.Modular.clP x = max 0 (min x Real.pi)

noncomputable def CommutingRepetition.VN.Modular.clU (q : ℝ) : ℝ

Clamp to [0, 1].

Equations

• CommutingRepetition.VN.Modular.clU q = max 0 (min q 1)

theorem CommutingRepetition.VN.Modular.clP_nonneg (x : ℝ) : 0 ≤ clP x

theorem CommutingRepetition.VN.Modular.clP_le_pi (x : ℝ) : clP x ≤ Real.pi

theorem CommutingRepetition.VN.Modular.continuous_clP : Continuous clP

theorem CommutingRepetition.VN.Modular.bdd_clP : BorelCalc.Bdd clP

theorem CommutingRepetition.VN.Modular.clP_eq_self {x : ℝ} (h : x ∈ Set.Icc 0 Real.pi) : clP x = x

theorem CommutingRepetition.VN.Modular.clU_nonneg (q : ℝ) : 0 ≤ clU q

theorem CommutingRepetition.VN.Modular.clU_le_one (q : ℝ) : clU q ≤ 1

theorem CommutingRepetition.VN.Modular.continuous_clU : Continuous clU

theorem CommutingRepetition.VN.Modular.bdd_clU : BorelCalc.Bdd clU

theorem CommutingRepetition.VN.Modular.clU_eq_self {q : ℝ} (h : q ∈ Set.Icc 0 1) : clU q = q

noncomputable def CommutingRepetition.VN.Modular.logSym (p : ℝ × ℝ) : ℝ

The symbol of the logarithm: 2π + x(2q − 1) − 2πq, which is x at q = 1 and 2π − x at q = 0.

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.VN.Modular.continuous_logSym : Continuous logSym

theorem CommutingRepetition.VN.Modular.logSym_nonneg (p : ℝ × ℝ) : 0 ≤ logSym p

theorem CommutingRepetition.VN.Modular.logSym_le (p : ℝ × ℝ) : logSym p ≤ 2 * Real.pi

theorem CommutingRepetition.VN.Modular.bdd2_logSym : BorelCalc.Bdd2 logSym

theorem CommutingRepetition.VN.Modular.exp_I_ofReal (x : ℝ) : Complex.exp (Complex.I * ↑x) = ↑(Real.cos x) + Complex.I * ↑(Real.sin x)

e^{i·arg} = cos + i sin for a real argument.

theorem CommutingRepetition.VN.Modular.exp_I_logSym {p : ℝ × ℝ} (hq : clU p.2 = 0 ∨ clU p.2 = 1) : Complex.exp (Complex.I * ↑(logSym p)) = ↑(Real.cos (clP p.1)) + Complex.I * ↑((2 * clU p.2 - 1) * Real.sin (clP p.1))

The key pointwise identity, valid where the sign variable is 0 or 1.

The real and imaginary parts of a unitary

noncomputable def CommutingRepetition.VN.Modular.reU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : K →L[ℂ] K

Re u = (u + u*)/2.

Equations

• CommutingRepetition.VN.Modular.reU u = (1 / 2) • (u + star u)

noncomputable def CommutingRepetition.VN.Modular.imU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : K →L[ℂ] K

Im u = i(u* − u)/2.

Equations

• CommutingRepetition.VN.Modular.imU u = (-(1 / 2) * Complex.I) • (u - star u)

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_reU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : IsSelfAdjoint (reU u)

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_imU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : IsSelfAdjoint (imU u)

theorem CommutingRepetition.VN.Modular.u_eq_reU_add_imU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : u = reU u + Complex.I • imU u

theorem CommutingRepetition.VN.Modular.norm_apply_eq_of_star_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (x : K) : ‖u x‖ = ‖x‖

theorem CommutingRepetition.VN.Modular.norm_le_one_of_star_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) : ‖u‖ ≤ 1

theorem CommutingRepetition.VN.Modular.norm_star_le_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu2 : u * star u = 1) : ‖star u‖ ≤ 1

theorem CommutingRepetition.VN.Modular.norm_reU_le_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : ‖reU u‖ ≤ 1

theorem CommutingRepetition.VN.Modular.norm_imU_le_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : ‖imU u‖ ≤ 1

theorem CommutingRepetition.VN.Modular.commute_self_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : Commute u (star u)

theorem CommutingRepetition.VN.Modular.commute_reU_imU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : Commute (reU u) (imU u)

theorem CommutingRepetition.VN.Modular.reU_sq_add_imU_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : reU u * reU u + imU u * imU u = 1

The angle and the sign

noncomputable def CommutingRepetition.VN.Modular.angU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : K →L[ℂ] K

|arg u| = arccos (Re u), with spectrum in [0, π].

Equations

• CommutingRepetition.VN.Modular.angU u = cfc Real.arccos (CommutingRepetition.VN.Modular.reU u)

noncomputable def CommutingRepetition.VN.Modular.sgnU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : K →L[ℂ] K

The sign of the imaginary part: the spectral projection 1_{[0,∞)}(Im u).

Equations

• CommutingRepetition.VN.Modular.sgnU u = CommutingRepetition.BorelCalc.P (CommutingRepetition.VN.Modular.imU u) ⋯ (Set.Ici 0)

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_angU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : IsSelfAdjoint (angU u)

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_sgnU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : IsSelfAdjoint (sgnU u)

theorem CommutingRepetition.VN.Modular.bdd_arccos_clamp : BorelCalc.Bdd fun (y : ℝ) => Real.arccos (clamp 1 y)

theorem CommutingRepetition.VN.Modular.angU_eq_bfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : angU u = BorelCalc.bfc (reU u) ⋯ fun (y : ℝ) => Real.arccos (clamp 1 y)

theorem CommutingRepetition.VN.Modular.angU_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : 0 ≤ angU u

theorem CommutingRepetition.VN.Modular.norm_angU_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : ‖angU u‖ ≤ Real.pi

theorem CommutingRepetition.VN.Modular.spectrum_angU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : spectrum ℝ (angU u) ⊆ Set.Icc 0 Real.pi

theorem CommutingRepetition.VN.Modular.spectrum_sgnU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : spectrum ℝ (sgnU u) ⊆ Set.Icc 0 1

theorem CommutingRepetition.VN.Modular.commute_angU_sgnU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : Commute (angU u) (sgnU u)

A vanishing joint symbol is a.e. zero

theorem CommutingRepetition.VN.Modular.ae_eq_zero_of_jbfc_eq_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E₁ E₂ : K →L[ℂ] K} (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hcm : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : BorelCalc.Bdd2 F) (h : BorelCalc.jbfc E₁ E₂ h₁ h₂ hcm F = 0) (ζ : K) : ∀ᵐ (p : ℝ × ℝ) ∂BorelCalc.νP E₁ E₂ h₁ h₂ hcm ζ, F p = 0

The logarithm

noncomputable def CommutingRepetition.VN.Modular.ulog {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : K →L[ℂ] K

The logarithm of a unitary: -i log u, with 0 ≤ · ≤ 2π and e^{i·} = u.

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_ulog {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : IsSelfAdjoint (ulog u hu1 hu2)

theorem CommutingRepetition.VN.Modular.ulog_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : 0 ≤ ulog u hu1 hu2

theorem CommutingRepetition.VN.Modular.ulog_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : ulog u hu1 hu2 ≤ ↑(2 * Real.pi) • 1

theorem CommutingRepetition.VN.Modular.reU_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) {N : VonNeumannAlgebra K} (hu : u ∈ N) : reU u ∈ N

theorem CommutingRepetition.VN.Modular.imU_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) {N : VonNeumannAlgebra K} (hu : u ∈ N) : imU u ∈ N

theorem CommutingRepetition.VN.Modular.angU_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) {N : VonNeumannAlgebra K} (hu : u ∈ N) : angU u ∈ N

theorem CommutingRepetition.VN.Modular.sgnU_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) {N : VonNeumannAlgebra K} (hu : u ∈ N) : sgnU u ∈ N

theorem CommutingRepetition.VN.Modular.ulog_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) {N : VonNeumannAlgebra K} (hu : u ∈ N) : ulog u hu1 hu2 ∈ N

theorem CommutingRepetition.VN.Modular.commute_ulog {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) {T : K →L[ℂ] K} (h1 : Commute u T) (h2 : Commute (star u) T) : Commute (ulog u hu1 hu2) T

Identifying the symbols

theorem CommutingRepetition.VN.Modular.bdd_cos_clP : BorelCalc.Bdd fun (x : ℝ) => Real.cos (clP x)

theorem CommutingRepetition.VN.Modular.bdd_sin_clP : BorelCalc.Bdd fun (x : ℝ) => Real.sin (clP x)

theorem CommutingRepetition.VN.Modular.bdd_sign_clU : BorelCalc.Bdd fun (q : ℝ) => 2 * clU q - 1

theorem CommutingRepetition.VN.Modular.bfc_clU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) : BorelCalc.bfc (sgnU u) ⋯ clU = sgnU u

theorem CommutingRepetition.VN.Modular.jbfc_cos_clP {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : (BorelCalc.jbfc (angU u) (sgnU u) ⋯ ⋯ ⋯ fun (p : ℝ × ℝ) => Real.cos (clP p.1)) = reU u

theorem CommutingRepetition.VN.Modular.jbfc_sin_clP {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : (BorelCalc.jbfc (angU u) (sgnU u) ⋯ ⋯ ⋯ fun (p : ℝ × ℝ) => Real.sin (clP p.1)) = cfc (fun (s : ℝ) => |s|) (imU u)

theorem CommutingRepetition.VN.Modular.jbfc_sign_clU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : (BorelCalc.jbfc (angU u) (sgnU u) ⋯ ⋯ ⋯ fun (p : ℝ × ℝ) => 2 * clU p.2 - 1) = ↑2 • sgnU u - 1

theorem CommutingRepetition.VN.Modular.sign_mul_abs_imU {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : (↑2 • sgnU u - 1) * cfc (fun (s : ℝ) => |s|) (imU u) = imU u

The polar decomposition of Im u: (2·1_{[0,∞)}(Im u) − 1)|Im u| = Im u.

e^{i log u} = u

theorem CommutingRepetition.VN.Modular.ae_clU_snd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) (ζ : K) : ∀ᵐ (p : ℝ × ℝ) ∂BorelCalc.νP (angU u) (sgnU u) ⋯ ⋯ ⋯ ζ, clU p.2 = 0 ∨ clU p.2 = 1

theorem CommutingRepetition.VN.Modular.eit_ulog {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) : eit (ulog u hu1 hu2) ⋯ 1 = u

e^{i log u} = u.

theorem CommutingRepetition.VN.Modular.eit_ulog_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (u : K →L[ℂ] K) (hu1 : star u * u = 1) (hu2 : u * star u = 1) (c t : ℝ) (hcb : IsSelfAdjoint (↑c • ulog u hu1 hu2)) : eit (↑c • ulog u hu1 hu2) hcb t = eit (ulog u hu1 hu2) ⋯ (t * c)

Scaling: e^{it(c·log u)} = e^{i(tc) log u}.