Finite sums in the complex Borel calculus

theorem CommutingRepetition.VN.Modular.cbdd_finset_sum {ι : Type u_2} (s : Finset ι) {G : ι → ℝ → ℂ} (hG : ∀ (i : ι), BorelCalc.CBdd (G i)) : BorelCalc.CBdd fun (t : ℝ) => ∑ i ∈ s, G i t

theorem CommutingRepetition.VN.Modular.cbfc_finset_sum {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {ι : Type u_2} (s : Finset ι) {G : ι → ℝ → ℂ} (hG : ∀ (i : ι), BorelCalc.CBdd (G i)) : (BorelCalc.cbfc E hE fun (t : ℝ) => ∑ i ∈ s, G i t) = ∑ i ∈ s, BorelCalc.cbfc E hE (G i)

The Dirichlet kernel and the Fejér majorant

noncomputable def CommutingRepetition.VN.Modular.dirK (N : ℕ) (t : ℝ) : ℂ

D_N(θ) = ∑_{k ≤ N} e^{ikθ}.

Equations

• CommutingRepetition.VN.Modular.dirK N t = ∑ k ∈ Finset.range (N + 1), CommutingRepetition.VN.Modular.eitf (↑k) t

theorem CommutingRepetition.VN.Modular.cbdd_dirK (N : ℕ) : BorelCalc.CBdd (dirK N)

theorem CommutingRepetition.VN.Modular.cbfc_dirK {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (N : ℕ) : BorelCalc.cbfc E hE (dirK N) = ∑ k ∈ Finset.range (N + 1), eit E hE ↑k

theorem CommutingRepetition.VN.Modular.re_eitf (t l : ℝ) : (eitf t l).re = Real.cos (t * l)

theorem CommutingRepetition.VN.Modular.norm_dirK_ge {N : ℕ} (hN : 1 ≤ N) {t : ℝ} (ht : |t| ≤ 1 / ↑N) : (↑N + 1) / 2 ≤ ‖dirK N t‖

On |t| ≤ 1/N the Dirichlet kernel is at least (N+1)/2.

noncomputable def CommutingRepetition.VN.Modular.fejerMaj (N : ℕ) (t : ℝ) : ℝ

The Fejér majorant Q_N = 4(N+1)^{-2}|D_N|².

Equations

• CommutingRepetition.VN.Modular.fejerMaj N t = 4 / (↑N + 1) ^ 2 * ‖CommutingRepetition.VN.Modular.dirK N t‖ ^ 2

theorem CommutingRepetition.VN.Modular.bdd_fejerMaj (N : ℕ) : BorelCalc.Bdd (fejerMaj N)

theorem CommutingRepetition.VN.Modular.fejerMaj_nonneg (N : ℕ) (t : ℝ) : 0 ≤ fejerMaj N t

theorem CommutingRepetition.VN.Modular.one_le_fejerMaj {N : ℕ} (hN : 1 ≤ N) {t : ℝ} (ht : |t| ≤ 1 / ↑N) : 1 ≤ fejerMaj N t

theorem CommutingRepetition.VN.Modular.eitf_add_two_pi (k : ℕ) (t : ℝ) : eitf (↑k) (t + 2 * Real.pi) = eitf (↑k) t

theorem CommutingRepetition.VN.Modular.dirK_add_two_pi (N : ℕ) (t : ℝ) : dirK N (t + 2 * Real.pi) = dirK N t

theorem CommutingRepetition.VN.Modular.fejerMaj_add_two_pi (N : ℕ) (t : ℝ) : fejerMaj N (t + 2 * Real.pi) = fejerMaj N t

Haar-distributed vectors

def CommutingRepetition.VN.Modular.IsHaarVec {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) : Prop

ζ is Haar distributed for E: the Fourier moments ⟪ζ, e^{ikE}ζ⟫ vanish for every nonzero integer k (HJX Lemma 2.2).

Equations

• CommutingRepetition.VN.Modular.IsHaarVec hE ζ = ∀ (k : ℤ), k ≠ 0 → inner ℂ ζ ((CommutingRepetition.VN.Modular.eit E hE ↑k) ζ) = 0

theorem CommutingRepetition.VN.Modular.inner_eit_eit {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) (h : IsHaarVec hE ζ) (j k : ℤ) : inner ℂ ((eit E hE ↑j) ζ) ((eit E hE ↑k) ζ) = if j = k then inner ℂ ζ ζ else 0

theorem CommutingRepetition.VN.Modular.inner_eit_eit_nat {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) (h : IsHaarVec hE ζ) (j k : ℕ) : inner ℂ ((eit E hE ↑j) ζ) ((eit E hE ↑k) ζ) = if j = k then inner ℂ ζ ζ else 0

theorem CommutingRepetition.VN.Modular.norm_sum_eit_sq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) (h : IsHaarVec hE ζ) (N : ℕ) : ‖(∑ k ∈ Finset.range (N + 1), eit E hE ↑k) ζ‖ ^ 2 = (↑N + 1) * ‖ζ‖ ^ 2

theorem CommutingRepetition.VN.Modular.integral_fejerMaj {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) (h : IsHaarVec hE ζ) (N : ℕ) : ∫ (t : ℝ), fejerMaj N t ∂BorelCalc.ν E hE ζ = 4 * ‖ζ‖ ^ 2 / (↑N + 1)

theorem CommutingRepetition.VN.Modular.ν_compl_Icc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) (hspec : spectrum ℝ E ⊆ Set.Icc 0 (2 * Real.pi)) : (BorelCalc.ν E hE ζ) (Set.Icc 0 (2 * Real.pi))ᶜ = 0

The spectral measure is concentrated on [0, 2π].

theorem CommutingRepetition.VN.Modular.measureReal_compl_Icc_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) (h : IsHaarVec hE ζ) (hspec : spectrum ℝ E ⊆ Set.Icc 0 (2 * Real.pi)) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : (BorelCalc.ν E hE ζ).real (Set.Icc δ (2 * Real.pi - δ))ᶜ ≤ 4 * ‖ζ‖ ^ 2 * δ

The uniform tail estimate near the branch cut: ν((δ, 2π−δ)ᶜ) ≤ 4‖ζ‖²δ, with a constant independent of E.

From the tail estimate to an operator estimate

theorem CommutingRepetition.VN.Modular.sub_cbfc_eq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) {G : ℝ → ℂ} (hG : BorelCalc.CBdd G) : E ζ - (BorelCalc.cbfc E hE G) ζ = (BorelCalc.cbfc E hE fun (t : ℝ) => ↑(trunc E t) - G t) ζ

E ζ − G(E) ζ = (id − G)(E) ζ, with id truncated to the spectrum.

theorem CommutingRepetition.VN.Modular.norm_sub_cbfc_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (ζ : 𝓗) {G : ℝ → ℂ} (hG : BorelCalc.CBdd G) (h : IsHaarVec hE ζ) (hspec : spectrum ℝ E ⊆ Set.Icc 0 (2 * Real.pi)) {δ η B : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) (h1 : ∀ t ∈ Set.Icc δ (2 * Real.pi - δ), ‖↑t - G t‖ ≤ η) (h2 : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖↑t - G t‖ ≤ B) : ‖E ζ - (BorelCalc.cbfc E hE G) ζ‖ ^ 2 ≤ η ^ 2 * ‖ζ‖ ^ 2 + B ^ 2 * (4 * ‖ζ‖ ^ 2 * δ)

The key ‖·‖-estimate: if the symbol G approximates the identity to η away from the branch cut and to B everywhere, then ‖Eζ − G(E)ζ‖² ≤ η²‖ζ‖² + 4B²‖ζ‖²δ. Both the constants and G are independent of E.

Trigonometric approximation of the identity away from the branch cut

theorem CommutingRepetition.VN.Modular.cmap_sum_apply {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [AddCommMonoid Y] [ContinuousAdd Y] {ι : Type u_4} (s : Finset ι) (f : ι → C(X, Y)) (x : X) : (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

noncomputable def CommutingRepetition.VN.Modular.ramp (δ t : ℝ) : ℝ

The piecewise-linear sawtooth on [0, 2π]: it equals t·2π/(2π−δ) on [0, 2π−δ] and drops linearly back to 0 on [2π−δ, 2π], so it vanishes at both endpoints and is within δ of the identity on [0, 2π−δ].

Equations

• CommutingRepetition.VN.Modular.ramp δ t = min (t * (2 * Real.pi / (2 * Real.pi - δ))) ((2 * Real.pi - t) * (2 * Real.pi / δ))

theorem CommutingRepetition.VN.Modular.continuous_ramp (δ : ℝ) : Continuous (ramp δ)

theorem CommutingRepetition.VN.Modular.ramp_zero {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) : ramp δ 0 = 0

theorem CommutingRepetition.VN.Modular.ramp_two_pi {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) : ramp δ (2 * Real.pi) = 0

theorem CommutingRepetition.VN.Modular.ramp_eq_of_le {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) {t : ℝ} (ht : t ≤ 2 * Real.pi - δ) : ramp δ t = t * (2 * Real.pi / (2 * Real.pi - δ))

theorem CommutingRepetition.VN.Modular.abs_ramp_sub_le {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 2 * Real.pi - δ) : |ramp δ t - t| ≤ δ

theorem CommutingRepetition.VN.Modular.ramp_nonneg {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) {t : ℝ} (ht0 : 0 ≤ t) (_ht : t ≤ 2 * Real.pi) : 0 ≤ ramp δ t

theorem CommutingRepetition.VN.Modular.ramp_le {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) {t : ℝ} (_ht : t ≤ 2 * Real.pi) : ramp δ t ≤ 2 * Real.pi

theorem CommutingRepetition.VN.Modular.abs_ramp_le {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ < 2 * Real.pi) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 2 * Real.pi) : |ramp δ t| ≤ 2 * Real.pi

noncomputable def CommutingRepetition.VN.Modular.trigSym (s : Finset ℤ) (c : ℤ → ℂ) (t : ℝ) : ℂ

A trigonometric polynomial as a symbol on ℝ.

Equations

• CommutingRepetition.VN.Modular.trigSym s c t = ∑ k ∈ s, c k * CommutingRepetition.VN.Modular.eitf (↑k) t

theorem CommutingRepetition.VN.Modular.cbdd_trigSym (s : Finset ℤ) (c : ℤ → ℂ) : BorelCalc.CBdd (trigSym s c)

theorem CommutingRepetition.VN.Modular.cbfc_trigSym {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (s : Finset ℤ) (c : ℤ → ℂ) : BorelCalc.cbfc E hE (trigSym s c) = ∑ k ∈ s, c k • eit E hE ↑k

theorem CommutingRepetition.VN.Modular.fourier_eq_eitf (k : ℤ) {t : ℝ} : (fourier k) ↑t = eitf (↑k) t

theorem CommutingRepetition.VN.Modular.exists_trigSym {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : ∃ (s : Finset ℤ) (c : ℤ → ℂ), (∀ t ∈ Set.Icc δ (2 * Real.pi - δ), ‖↑t - trigSym s c t‖ ≤ 2 * δ) ∧ ∀ (t : ℝ), ‖trigSym s c t‖ ≤ 2 * Real.pi + 1

Trigonometric approximation of the identity on [δ, 2π−δ], with a global bound that does not depend on the polynomial.

theorem CommutingRepetition.VN.Modular.exists_trig_uniform {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {r : ℝ} (_hr : 0 ≤ r) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset ℤ) (c : ℤ → ℂ), ∀ (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ζ : 𝓗), IsHaarVec hE ζ → spectrum ℝ E ⊆ Set.Icc 0 (2 * Real.pi) → ‖ζ‖ ≤ r → ‖E ζ - (∑ k ∈ s, c k • eit E hE ↑k) ζ‖ ≤ ε

Uniform trigonometric approximation of a Haar-distributed self-adjoint operator (HJX Lemma 2.6(i)'s analytic input). Given a bound r on ‖ζ‖ and an ε > 0, one fixed trigonometric polynomial ∑_{k∈s} c k z^k satisfies ‖Eζ − ∑_{k∈s} c k e^{ikE} ζ‖ ≤ ε simultaneously for every Haar pair (E, ζ).

The unitary group as a strong limit of its exponential partial sums

theorem CommutingRepetition.VN.Modular.cbdd_trunc_pow {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (k : ℕ) : BorelCalc.CBdd fun (l : ℝ) => ↑(trunc E l) ^ k

theorem CommutingRepetition.VN.Modular.cbfc_trunc_pow {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (k : ℕ) : (BorelCalc.cbfc E hE fun (l : ℝ) => ↑(trunc E l) ^ k) = E ^ k

noncomputable def CommutingRepetition.VN.Modular.expCoef (t : ℝ) (k : ℕ) : ℂ

The coefficients of the exponential series.

Equations

• CommutingRepetition.VN.Modular.expCoef t k = (Complex.I * ↑t) ^ k / ↑k.factorial

theorem CommutingRepetition.VN.Modular.expCoef_zero (t : ℝ) : expCoef t 0 = 1

theorem CommutingRepetition.VN.Modular.norm_expCoef (t : ℝ) (k : ℕ) : ‖expCoef t k‖ = |t| ^ k / ↑k.factorial

noncomputable def CommutingRepetition.VN.Modular.expPoly {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t : ℝ) (N : ℕ) : 𝓗 →L[ℂ] 𝓗

The partial sums of the exponential series ∑_{k<N} (it)^k E^k / k!.

Equations

• CommutingRepetition.VN.Modular.expPoly E t N = ∑ k ∈ Finset.range N, CommutingRepetition.VN.Modular.expCoef t k • E ^ k

theorem CommutingRepetition.VN.Modular.expPoly_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t : ℝ) : expPoly E t 0 = 0

theorem CommutingRepetition.VN.Modular.expPoly_succ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t : ℝ) (N : ℕ) : expPoly E t (N + 1) = ∑ i ∈ Finset.range N, expCoef t (i + 1) • E ^ (i + 1) + 1

noncomputable def CommutingRepetition.VN.Modular.expSym {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t : ℝ) (N : ℕ) (l : ℝ) : ℂ

The N-th partial sum of the symbol e^{itl}, with l truncated to the spectrum.

Equations

• CommutingRepetition.VN.Modular.expSym E t N l = ∑ k ∈ Finset.range N, (Complex.I * ↑t * ↑(CommutingRepetition.VN.Modular.trunc E l)) ^ k / ↑k.factorial

theorem CommutingRepetition.VN.Modular.cbdd_expSym {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t : ℝ) (N : ℕ) : BorelCalc.CBdd (expSym E t N)

theorem CommutingRepetition.VN.Modular.cbfc_expSym {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (t : ℝ) (N : ℕ) : BorelCalc.cbfc E hE (expSym E t N) = expPoly E t N

theorem CommutingRepetition.VN.Modular.norm_expSym_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t : ℝ) (N : ℕ) (l : ℝ) : ‖expSym E t N l‖ ≤ Real.exp (|t| * ‖E‖)

theorem CommutingRepetition.VN.Modular.tendsto_expSym {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (t l : ℝ) : Filter.Tendsto (fun (N : ℕ) => expSym E t N l) Filter.atTop (nhds (eitf t (trunc E l)))

theorem CommutingRepetition.VN.Modular.tendsto_expPoly_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E : 𝓗 →L[ℂ] 𝓗} (hE : IsSelfAdjoint E) (t : ℝ) (ζ : 𝓗) : Filter.Tendsto (fun (N : ℕ) => (expPoly E t N) ζ) Filter.atTop (nhds ((eit E hE t) ζ))

The unitary group is the strong limit of the exponential partial sums: ∑_{k<N} (it)^k E^k / k! ζ → e^{itE} ζ.