Bounded spectral integration

This file constructs the spectral integral first for complex-valued simple functions and then for bounded measurable functions.

noncomputable def PVM.simpleIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) : E →L[ℂ] E

The spectral sum of a complex-valued simple function against a PVM.

Equations

• E_pvm.simpleIntegral f = ∑ z ∈ f.range, z • E_pvm.proj (⇑f ⁻¹' {z})

theorem PVM.sum_proj_preimage {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) {β : Type u_2} (f : MeasureTheory.SimpleFunc ℝ β) (s : Finset β) : ∑ y ∈ s, E_pvm.proj (⇑f ⁻¹' {y}) = E_pvm.proj (⇑f ⁻¹' ↑s)

The projections of finitely many fibers add to the projection of their union.

theorem PVM.simpleIntegral_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) {β : Type u_2} (f : MeasureTheory.SimpleFunc ℝ β) (g : β → ℂ) : E_pvm.simpleIntegral (MeasureTheory.SimpleFunc.map g f) = ∑ y ∈ f.range, g y • E_pvm.proj (⇑f ⁻¹' {y})

Reindexing a simple function groups the projections of fibers with the same new value.

theorem PVM.simpleIntegral_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f g : MeasureTheory.SimpleFunc ℝ ℂ) : E_pvm.simpleIntegral (f + g) = E_pvm.simpleIntegral f + E_pvm.simpleIntegral g

Simple spectral integration preserves addition.

theorem PVM.simpleIntegral_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) : E_pvm.simpleIntegral (-f) = -E_pvm.simpleIntegral f

Simple spectral integration preserves negation.

theorem PVM.simpleIntegral_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f g : MeasureTheory.SimpleFunc ℝ ℂ) : E_pvm.simpleIntegral (f - g) = E_pvm.simpleIntegral f - E_pvm.simpleIntegral g

Simple spectral integration preserves subtraction.

theorem PVM.sum_proj_fiber_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) : ∑ z ∈ f.range, E_pvm.proj (⇑f ⁻¹' {z}) = 1

The projections of the fibers of a simple function sum to the identity.

theorem PVM.proj_fiber_mul_proj_fiber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) {z w : ℂ} (hzw : z ≠ w) : E_pvm.proj (⇑f ⁻¹' {z}) * E_pvm.proj (⇑f ⁻¹' {w}) = 0

Projections onto two distinct fibers of a simple function multiply to zero.

theorem PVM.simpleIntegral_map_mul_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) {β : Type u_2} (f : MeasureTheory.SimpleFunc ℝ β) (a b : β → ℂ) : E_pvm.simpleIntegral (MeasureTheory.SimpleFunc.map a f) * E_pvm.simpleIntegral (MeasureTheory.SimpleFunc.map b f) = E_pvm.simpleIntegral (MeasureTheory.SimpleFunc.map (fun (z : β) => a z * b z) f)

On a fixed simple partition, pointwise multiplication becomes operator multiplication.

theorem PVM.simpleIntegral_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f g : MeasureTheory.SimpleFunc ℝ ℂ) : E_pvm.simpleIntegral (f * g) = E_pvm.simpleIntegral f * E_pvm.simpleIntegral g

Simple spectral integration preserves pointwise multiplication.

theorem PVM.star_simpleIntegral_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) : star (E_pvm.simpleIntegral f) * E_pvm.simpleIntegral f = ∑ z ∈ f.range, (star z * z) • E_pvm.proj (⇑f ⁻¹' {z})

Multiplying a simple spectral sum by its adjoint removes all cross-fiber terms.

theorem PVM.norm_sq_simpleIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) (x : E) : ‖(E_pvm.simpleIntegral f) x‖ ^ 2 = ∑ z ∈ f.range, ‖z‖ ^ 2 * (inner ℂ ((E_pvm.proj (⇑f ⁻¹' {z})) x) x).re

The squared norm of a simple spectral sum is the weighted sum over its fibers.

theorem PVM.norm_simpleIntegral_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : MeasureTheory.SimpleFunc ℝ ℂ) {C : ℝ} (hbdd : ∀ (t : ℝ), ‖f t‖ ≤ C) : ‖E_pvm.simpleIntegral f‖ ≤ C

A uniform bound for a simple function bounds the norm of its spectral sum.

theorem PVM.norm_simpleIntegral_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f g : MeasureTheory.SimpleFunc ℝ ℂ) {C : ℝ} (hbdd : ∀ (t : ℝ), ‖f t - g t‖ ≤ C) : ‖E_pvm.simpleIntegral f - E_pvm.simpleIntegral g‖ ≤ C

Uniform distance of simple functions controls the operator norm of their spectral sums.

noncomputable def boundedApprox (f : ℝ → ℂ) (hf : Measurable f) (C : ℝ) (hbdd : ∀ (t : ℝ), ‖f t‖ ≤ C) (n : ℕ) : MeasureTheory.SimpleFunc ℝ ℂ

A uniformly bounded simple-function approximation used to construct the bounded spectral integral.

Equations

• boundedApprox f hf C hbdd n = MeasureTheory.SimpleFunc.approxOn f hf (Metric.closedBall 0 C) 0 ⋯ n

theorem exists_bounded_simpleFunc_tendstoUniformly (f : ℝ → ℂ) (hf : Measurable f) (C : ℝ) (hbdd : ∀ (t : ℝ), ‖f t‖ ≤ C) : ∃ (s : ℕ → MeasureTheory.SimpleFunc ℝ ℂ), TendstoUniformly (fun (n : ℕ) (t : ℝ) => (s n) t) f Filter.atTop ∧ ∀ (n : ℕ) (t : ℝ), ‖(s n) t‖ ≤ C

A bounded measurable complex-valued function admits uniformly convergent simple approximations obeying the same pointwise norm bound.

theorem PVM.simpleIntegral_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (z : ℂ) : E_pvm.simpleIntegral (MeasureTheory.SimpleFunc.const ℝ z) = z • 1

The spectral sum of a constant simple function is the corresponding scalar operator.

@[simp]

theorem PVM.simpleIntegral_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : E_pvm.simpleIntegral 0 = 0

The spectral sum of the zero simple function is zero.

@[simp]

theorem PVM.simpleIntegral_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : E_pvm.simpleIntegral 1 = 1

The spectral sum of the unit simple function is the identity operator.

theorem PVM.simpleIntegral_piecewise_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (S : Set ℝ) (hS : MeasurableSet S) (z : ℂ) : E_pvm.simpleIntegral (MeasureTheory.SimpleFunc.piecewise S hS (MeasureTheory.SimpleFunc.const ℝ z) (MeasureTheory.SimpleFunc.const ℝ 0)) = z • E_pvm.proj S

The spectral sum of z on a measurable set and zero off it is z • E(S).

noncomputable def PVM.integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (t : ℝ), ‖f t‖ ≤ C) : E →L[ℂ] E

The bounded spectral integral of a measurable, uniformly bounded complex function.

Equations

• E_pvm.integral f hf hbdd = Filter.atTop.limUnder fun (n : ℕ) => E_pvm.simpleIntegral (boundedApprox f hf (Classical.choose hbdd) ⋯ n)

theorem PVM.tendsto_simpleIntegral_of_tendstoUniformly {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) (hbdd : ∃ (C : ℝ), ∀ (t : ℝ), ‖f t‖ ≤ C) (s : ℕ → MeasureTheory.SimpleFunc ℝ ℂ) (hs : TendstoUniformly (fun (n : ℕ) (t : ℝ) => (s n) t) f Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => E_pvm.simpleIntegral (s n)) Filter.atTop (nhds (E_pvm.integral f hf hbdd))

Spectral sums of any uniformly convergent simple approximation converge to the bounded spectral integral. In particular, the limit is independent of the chosen bound and approximation sequence.

theorem PVM.norm_integral_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f : ℝ → ℂ) (hf : Measurable f) {C : ℝ} (hbdd : ∀ (t : ℝ), ‖f t‖ ≤ C) : ‖E_pvm.integral f hf ⋯‖ ≤ C

A pointwise bound on an integrand bounds the operator norm of its spectral integral.

theorem PVM.integral_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f g : ℝ → ℂ) (hf : Measurable f) (hg : Measurable g) (hbddf : ∃ (C : ℝ), ∀ (t : ℝ), ‖f t‖ ≤ C) (hbddg : ∃ (C : ℝ), ∀ (t : ℝ), ‖g t‖ ≤ C) (hbddfg : ∃ (C : ℝ), ∀ (t : ℝ), ‖(f * g) t‖ ≤ C) : E_pvm.integral (f * g) ⋯ hbddfg = E_pvm.integral f hf hbddf * E_pvm.integral g hg hbddg

Bounded spectral integration preserves pointwise multiplication.

theorem PVM.integral_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (f g : ℝ → ℂ) (hf : Measurable f) (hg : Measurable g) (hbddf : ∃ (C : ℝ), ∀ (t : ℝ), ‖f t‖ ≤ C) (hbddg : ∃ (C : ℝ), ∀ (t : ℝ), ‖g t‖ ≤ C) (hbddsub : ∃ (C : ℝ), ∀ (t : ℝ), ‖(f - g) t‖ ≤ C) : E_pvm.integral (f - g) ⋯ hbddsub = E_pvm.integral f hf hbddf - E_pvm.integral g hg hbddg

Bounded spectral integration preserves pointwise subtraction, independently of the bound witnesses used in the three integrals.

theorem PVM.integral_congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) {f g : ℝ → ℂ} (hfg : f = g) (hf : Measurable f) (hg : Measurable g) (hbddf : ∃ (C : ℝ), ∀ (r : ℝ), ‖f r‖ ≤ C) (hbddg : ∃ (C : ℝ), ∀ (r : ℝ), ‖g r‖ ≤ C) : E_pvm.integral f hf hbddf = E_pvm.integral g hg hbddg

Bounded spectral integration depends only on the function, independently of witnesses.

theorem PVM.integral_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (z : ℂ) : E_pvm.integral (fun (x : ℝ) => z) ⋯ ⋯ = z • 1

Integrating a constant gives the corresponding scalar multiple of the identity.

theorem PVM.integral_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : E_pvm.integral (fun (x : ℝ) => 1) ⋯ ⋯ = 1

Integrating the constant one gives the identity operator.