Monotone convergence

theorem CommutingRepetition.BorelCalc.Bdd.of_unit {g : ℝ → ℝ} (hg : Measurable g) (h0 : ∀ (t : ℝ), 0 ≤ g t) (h1 : ∀ (t : ℝ), g t ≤ 1) : Bdd g

theorem CommutingRepetition.BorelCalc.bfc_tendsto_of_monotone {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℕ → ℝ → ℝ} {G : ℝ → ℝ} (hg : ∀ (n : ℕ), Measurable (g n)) (hG : Measurable G) (h0 : ∀ (n : ℕ) (t : ℝ), 0 ≤ g n t) (h1 : ∀ (n : ℕ) (t : ℝ), g n t ≤ 1) (hmono : ∀ (t : ℝ), Monotone fun (n : ℕ) => g n t) (hlim : ∀ (t : ℝ), Filter.Tendsto (fun (n : ℕ) => g n t) Filter.atTop (nhds (G t))) (ξ : 𝓗) : Filter.Tendsto (fun (n : ℕ) => (bfc E hE (g n)) ξ) Filter.atTop (nhds ((bfc E hE G) ξ))

Monotone convergence for the Borel calculus: 0 ≤ gₙ ↑ G ≤ 1 pointwise gives bfc gₙ → bfc G strongly.

theorem CommutingRepetition.BorelCalc.bfc_tendsto_of_antitone {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℕ → ℝ → ℝ} {G : ℝ → ℝ} (hg : ∀ (n : ℕ), Measurable (g n)) (hG : Measurable G) (h0 : ∀ (n : ℕ) (t : ℝ), 0 ≤ g n t) (h1 : ∀ (n : ℕ) (t : ℝ), g n t ≤ 1) (hanti : ∀ (t : ℝ), Antitone fun (n : ℕ) => g n t) (hlim : ∀ (t : ℝ), Filter.Tendsto (fun (n : ℕ) => g n t) Filter.atTop (nhds (G t))) (ξ : 𝓗) : Filter.Tendsto (fun (n : ℕ) => (bfc E hE (g n)) ξ) Filter.atTop (nhds ((bfc E hE G) ξ))

Antitone convergence: 1 ≥ gₙ ↓ G ≥ 0 pointwise gives bfc gₙ → bfc G strongly.

Continuous approximants of half-line indicators

noncomputable def CommutingRepetition.BorelCalc.stepApprox (a : ℝ) (n : ℕ) (t : ℝ) : ℝ

The continuous approximants of 1_{Iic a}: t ↦ max 0 (min 1 (1 − n (t − a))).

Equations

• CommutingRepetition.BorelCalc.stepApprox a n t = max 0 (min 1 (1 - ↑n * (t - a)))

theorem CommutingRepetition.BorelCalc.stepApprox_continuous (a : ℝ) (n : ℕ) : Continuous (stepApprox a n)

theorem CommutingRepetition.BorelCalc.stepApprox_nonneg (a : ℝ) (n : ℕ) (t : ℝ) : 0 ≤ stepApprox a n t

theorem CommutingRepetition.BorelCalc.stepApprox_le_one (a : ℝ) (n : ℕ) (t : ℝ) : stepApprox a n t ≤ 1

theorem CommutingRepetition.BorelCalc.stepApprox_of_le (a : ℝ) (n : ℕ) {t : ℝ} (ht : t ≤ a) : stepApprox a n t = 1

theorem CommutingRepetition.BorelCalc.stepApprox_antitone (a t : ℝ) : Antitone fun (n : ℕ) => stepApprox a n t

theorem CommutingRepetition.BorelCalc.stepApprox_tendsto (a t : ℝ) : Filter.Tendsto (fun (n : ℕ) => stepApprox a n t) Filter.atTop (nhds ((Set.Iic a).indicator 1 t))

theorem CommutingRepetition.BorelCalc.indicator_one_nonneg (I : Set ℝ) (t : ℝ) : 0 ≤ I.indicator 1 t

theorem CommutingRepetition.BorelCalc.indicator_one_le_one (I : Set ℝ) (t : ℝ) : I.indicator 1 t ≤ 1

Membership in a strongly sequentially closed star subalgebra

theorem CommutingRepetition.BorelCalc.isClosed_of_strong {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) : IsClosed ↑S

theorem CommutingRepetition.BorelCalc.cfc_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) (hES : E ∈ S) (g : ℝ → ℝ) : cfc g E ∈ S

theorem CommutingRepetition.BorelCalc.bfc_mem_of_continuous {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) (hES : E ∈ S) {g : ℝ → ℝ} (hg : Bdd g) (hc : Continuous g) : bfc E hE g ∈ S

theorem CommutingRepetition.BorelCalc.bfc_indicator_Iic_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) (hES : E ∈ S) (a : ℝ) : bfc E hE ((Set.Iic a).indicator 1) ∈ S

theorem CommutingRepetition.BorelCalc.bfc_indicator_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) (hES : E ∈ S) {I : Set ℝ} (hI : MeasurableSet I) : bfc E hE (I.indicator 1) ∈ S

Every spectral projection lies in S.

The projection-valued measure

noncomputable def CommutingRepetition.BorelCalc.P {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (I : Set ℝ) : 𝓗 →L[ℂ] 𝓗

The spectral projection P I = 1_I(E) (junk 0 for non-measurable I).

Equations

• CommutingRepetition.BorelCalc.P E hE I = CommutingRepetition.BorelCalc.bfc E hE (I.indicator 1)

theorem CommutingRepetition.BorelCalc.P_of_not_measurable {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : ¬MeasurableSet I) : P E hE I = 0

theorem CommutingRepetition.BorelCalc.P_isSelfAdjoint {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (I : Set ℝ) : IsSelfAdjoint (P E hE I)

theorem CommutingRepetition.BorelCalc.star_P {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (I : Set ℝ) : star (P E hE I) = P E hE I

theorem CommutingRepetition.BorelCalc.P_empty {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) : P E hE ∅ = 0

theorem CommutingRepetition.BorelCalc.P_univ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) : P E hE Set.univ = 1

theorem CommutingRepetition.BorelCalc.P_inter {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) : P E hE I * P E hE J = P E hE (I ∩ J)

theorem CommutingRepetition.BorelCalc.P_union {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) (hd : Disjoint I J) : P E hE (I ∪ J) = P E hE I + P E hE J

theorem CommutingRepetition.BorelCalc.P_compl {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) : P E hE Iᶜ = 1 - P E hE I

theorem CommutingRepetition.BorelCalc.P_idem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) : P E hE I * P E hE I = P E hE I

theorem CommutingRepetition.BorelCalc.P_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (I : Set ℝ) : 0 ≤ P E hE I

theorem CommutingRepetition.BorelCalc.P_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (I : Set ℝ) : P E hE I ≤ 1

theorem CommutingRepetition.BorelCalc.P_norm_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (I : Set ℝ) : ‖P E hE I‖ ≤ 1

theorem CommutingRepetition.BorelCalc.inner_P {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) (ξ : 𝓗) : inner ℂ ξ ((P E hE I) ξ) = ↑((ν E hE ξ) I).toReal

The quadratic form of P I is the spectral measure: ⟪ξ, P I ξ⟫ = ν_ξ(I).

theorem CommutingRepetition.BorelCalc.re_inner_P {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) (ξ : 𝓗) : (inner ℂ ξ ((P E hE I) ξ)).re = ((ν E hE ξ) I).toReal

theorem CommutingRepetition.BorelCalc.norm_P_apply_sq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) (ξ : 𝓗) : ‖(P E hE I) ξ‖ ^ 2 = ((ν E hE ξ) I).toReal

theorem CommutingRepetition.BorelCalc.P_mono {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) (h : I ⊆ J) : P E hE I ≤ P E hE J

theorem CommutingRepetition.BorelCalc.P_compl_spectrum {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) : P E hE (spectrum ℝ E)ᶜ = 0

theorem CommutingRepetition.BorelCalc.P_spectrum {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) : P E hE (spectrum ℝ E) = 1

theorem CommutingRepetition.BorelCalc.P_eq_zero_of_disjoint_spectrum {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) (h : Disjoint I (spectrum ℝ E)) : P E hE I = 0

theorem CommutingRepetition.BorelCalc.P_comm_bfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : Set ℝ} (hI : MeasurableSet I) {g : ℝ → ℝ} (hg : Bdd g) : P E hE I * bfc E hE g = bfc E hE g * P E hE I

theorem CommutingRepetition.BorelCalc.P_comm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) : P E hE I * P E hE J = P E hE J * P E hE I

theorem CommutingRepetition.BorelCalc.P_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) (hES : E ∈ S) (I : Set ℝ) : P E hE I ∈ S

Membership of every spectral projection in a strongly sequentially closed star subalgebra containing E.

Norm bounds, finite sums, and membership of every bounded Borel function

theorem CommutingRepetition.BorelCalc.norm_bfc_apply_sq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : ‖(bfc E hE g) ξ‖ ^ 2 = ∫ (t : ℝ), (g * g) t ∂ν E hE ξ

theorem CommutingRepetition.BorelCalc.norm_bfc_apply_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) (ξ : 𝓗) : ‖(bfc E hE g) ξ‖ ≤ C * ‖ξ‖

theorem CommutingRepetition.BorelCalc.norm_bfc_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) : ‖bfc E hE g‖ ≤ C

theorem CommutingRepetition.BorelCalc.Bdd.finsetSum {ι : Type u_2} (s : Finset ι) {g : ι → ℝ → ℝ} (hg : ∀ i ∈ s, Bdd (g i)) : Bdd (∑ i ∈ s, g i)

theorem CommutingRepetition.BorelCalc.bfc_finsetSum {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {ι : Type u_2} (s : Finset ι) {g : ι → ℝ → ℝ} (hg : ∀ i ∈ s, Bdd (g i)) : bfc E hE (∑ i ∈ s, g i) = ∑ i ∈ s, bfc E hE (g i)

noncomputable def CommutingRepetition.BorelCalc.dyadic (g : ℝ → ℝ) (n : ℕ) (t : ℝ) : ℝ

The dyadic approximant ⌊2ⁿ g⌋ / 2ⁿ of a real function.

Equations

• CommutingRepetition.BorelCalc.dyadic g n t = ↑⌊2 ^ n * g t⌋ / 2 ^ n

theorem CommutingRepetition.BorelCalc.dyadic_measurable {g : ℝ → ℝ} (hg : Measurable g) (n : ℕ) : Measurable (dyadic g n)

theorem CommutingRepetition.BorelCalc.dyadic_le (g : ℝ → ℝ) (n : ℕ) (t : ℝ) : dyadic g n t ≤ g t

theorem CommutingRepetition.BorelCalc.lt_dyadic_add (g : ℝ → ℝ) (n : ℕ) (t : ℝ) : g t < dyadic g n t + (1 / 2) ^ n

theorem CommutingRepetition.BorelCalc.abs_sub_dyadic_le (g : ℝ → ℝ) (n : ℕ) (t : ℝ) : |dyadic g n t - g t| ≤ (1 / 2) ^ n

theorem CommutingRepetition.BorelCalc.dyadic_bdd {g : ℝ → ℝ} (hg : Bdd g) (n : ℕ) : Bdd (dyadic g n)

theorem CommutingRepetition.BorelCalc.dyadic_eq_sum {g : ℝ → ℝ} {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) (n : ℕ) : dyadic g n = ∑ k ∈ Finset.Icc (-(⌈2 ^ n * C⌉ + 1)) (⌈2 ^ n * C⌉ + 1), fun (t : ℝ) => ↑k / 2 ^ n * {t : ℝ | ⌊2 ^ n * g t⌋ = k}.indicator 1 t

The dyadic approximant is a finite combination of indicators of level sets.

theorem CommutingRepetition.BorelCalc.bfc_mem_of_bdd {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (S : StarSubalgebra ℂ (𝓗 →L[ℂ] 𝓗)) (hS : ∀ (T : ℕ → 𝓗 →L[ℂ] 𝓗) (L : 𝓗 →L[ℂ] 𝓗), (∀ (n : ℕ), T n ∈ S) → (∀ (ξ : 𝓗), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ S) (hES : E ∈ S) {g : ℝ → ℝ} (hg : Bdd g) : bfc E hE g ∈ S

Every bounded Borel function of E lies in S: the dyadic approximants are finite combinations of spectral projections, and converge in operator norm.

Spectral projections of increasing unions

theorem CommutingRepetition.BorelCalc.indicator_iUnion_tendsto {I : ℕ → Set ℝ} (hmono : Monotone I) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => (I n).indicator 1 t) Filter.atTop (nhds ((⋃ (n : ℕ), I n).indicator 1 t))

theorem CommutingRepetition.BorelCalc.P_tendsto_iUnion {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {I : ℕ → Set ℝ} (hI : ∀ (n : ℕ), MeasurableSet (I n)) (hmono : Monotone I) (ξ : 𝓗) : Filter.Tendsto (fun (n : ℕ) => (P E hE (I n)) ξ) Filter.atTop (nhds ((P E hE (⋃ (n : ℕ), I n)) ξ))

Strong convergence P (I n) → P (⋃ n, I n) for an increasing sequence of Borel sets.

theorem CommutingRepetition.BorelCalc.P_Icc_zero_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (h : spectrum ℝ E ⊆ Set.Icc 0 1) : P E hE (Set.Icc 0 1) = 1

The spectral projections of an operator with spectrum in [0, 1].