Pointwise convergence of truncations

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

theorem CommutingRepetition.GraphMod.ψ_eq_indicator : ψ = (Set.Ico 0 1).indicator ψ

theorem CommutingRepetition.GraphMod.ψn_tendsto (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => ψn n t) Filter.atTop (nhds (ψ t))

theorem CommutingRepetition.GraphMod.ψn_mono (t : ℝ) : Monotone fun (n : ℕ) => ψn n t

theorem CommutingRepetition.GraphMod.ψn_le_ψ (n : ℕ) (t : ℝ) : ψn n t ≤ ψ t

theorem CommutingRepetition.GraphMod.ψn_sq_mono (t : ℝ) : Monotone fun (n : ℕ) => ψn n t ^ 2

theorem CommutingRepetition.GraphMod.ψn_sq_tendsto (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => ψn n t ^ 2) Filter.atTop (nhds (ψ t ^ 2))

theorem CommutingRepetition.GraphMod.Bdd.sq {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : BorelCalc.Bdd fun (t : ℝ) => g t ^ 2

The spectral distribution of the modulus

theorem CommutingRepetition.GraphMod.ν₀_univ (M : StdTracialAlgebra) (x : M.H) : (BorelCalc.ν (Eop M x) ⋯ M.traceVector) Set.univ = 1

instance CommutingRepetition.GraphMod.ν₀_isProbabilityMeasure (M : StdTracialAlgebra) (x : M.H) : MeasureTheory.IsProbabilityMeasure (BorelCalc.ν (Eop M x) ⋯ M.traceVector)

noncomputable def CommutingRepetition.GraphMod.μx (M : StdTracialAlgebra) (x : M.H) : MeasureTheory.Measure ℝ

The spectral distribution μ = ψ_* ν_Ω of the left modulus.

Equations

• CommutingRepetition.GraphMod.μx M x = MeasureTheory.Measure.map CommutingRepetition.GraphMod.ψ (CommutingRepetition.BorelCalc.ν (CommutingRepetition.GraphMod.Eop M x) ⋯ M.traceVector)

theorem CommutingRepetition.GraphMod.μx_prob (M : StdTracialAlgebra) (x : M.H) : MeasureTheory.IsProbabilityMeasure (μx M x)

theorem CommutingRepetition.GraphMod.μx_apply (M : StdTracialAlgebra) (x : M.H) {I : Set ℝ} (hI : MeasurableSet I) : (μx M x) I = (BorelCalc.ν (Eop M x) ⋯ M.traceVector) (ψ ⁻¹' I)

theorem CommutingRepetition.GraphMod.μx_Iio (M : StdTracialAlgebra) (x : M.H) : (μx M x) (Set.Iio 0) = 0

Integrability of the modulus

theorem CommutingRepetition.GraphMod.integral_ψn_sq (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : ∫ (t : ℝ), ψn n t ^ 2 ∂BorelCalc.ν (Eop M x) ⋯ M.traceVector = ‖(BorelCalc.P (Eop M x) ⋯ (Set.Icc 0 (aN n))) x‖ ^ 2

theorem CommutingRepetition.GraphMod.lintegral_ψ_sq_le (M : StdTracialAlgebra) (x : M.H) : ∫⁻ (t : ℝ), ENNReal.ofReal (ψ t ^ 2) ∂BorelCalc.ν (Eop M x) ⋯ M.traceVector ≤ ENNReal.ofReal (‖x‖ ^ 2)

theorem CommutingRepetition.GraphMod.integrable_ψ_sq (M : StdTracialAlgebra) (x : M.H) : MeasureTheory.Integrable (fun (t : ℝ) => ψ t ^ 2) (BorelCalc.ν (Eop M x) ⋯ M.traceVector)

theorem CommutingRepetition.GraphMod.integral_ψ_sq (M : StdTracialAlgebra) (x : M.H) : ∫ (t : ℝ), ψ t ^ 2 ∂BorelCalc.ν (Eop M x) ⋯ M.traceVector = ‖x‖ ^ 2

theorem CommutingRepetition.GraphMod.integrable_ψ (M : StdTracialAlgebra) (x : M.H) : MeasureTheory.Integrable ψ (BorelCalc.ν (Eop M x) ⋯ M.traceVector)

theorem CommutingRepetition.GraphMod.moment2 (M : StdTracialAlgebra) (x : M.H) : ∫ (b : ℝ), b ^ 2 ∂μx M x = ‖x‖ ^ 2

The band projections

noncomputable def CommutingRepetition.GraphMod.projx (M : StdTracialAlgebra) (x : M.H) (I : Set ℝ) : ↥M.vnAlg

proj I = 1_I(h_x) = P (ψ⁻¹ I), as an element of the von Neumann algebra.

Equations

• CommutingRepetition.GraphMod.projx M x I = ⟨CommutingRepetition.BorelCalc.P (CommutingRepetition.GraphMod.Eop M x) ⋯ (CommutingRepetition.GraphMod.ψ ⁻¹' I), ⋯⟩

theorem CommutingRepetition.GraphMod.projx_val (M : StdTracialAlgebra) (x : M.H) (I : Set ℝ) : ↑(projx M x I) = BorelCalc.P (Eop M x) ⋯ (ψ ⁻¹' I)

theorem CommutingRepetition.GraphMod.projx_star (M : StdTracialAlgebra) (x : M.H) (I : Set ℝ) : star (projx M x I) = projx M x I

theorem CommutingRepetition.GraphMod.projx_empty (M : StdTracialAlgebra) (x : M.H) : projx M x ∅ = 0

theorem CommutingRepetition.GraphMod.projx_inter (M : StdTracialAlgebra) (x : M.H) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) : projx M x I * projx M x J = projx M x (I ∩ J)

theorem CommutingRepetition.GraphMod.projx_union (M : StdTracialAlgebra) (x : M.H) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) (hd : Disjoint I J) : projx M x (I ∪ J) = projx M x I + projx M x J

theorem CommutingRepetition.GraphMod.projx_trace (M : StdTracialAlgebra) (x : M.H) {I : Set ℝ} (hI : MeasurableSet I) : M.vnModel.τ (projx M x I) = ↑((μx M x) I).toReal

theorem CommutingRepetition.GraphMod.preimage_ψ_subset {I : Set ℝ} (hsub : I ⊆ Set.Ioi 0) : ψ ⁻¹' I ⊆ Set.Ioo 0 1

theorem CommutingRepetition.GraphMod.projx_absorb (M : StdTracialAlgebra) (x : M.H) {I : Set ℝ} (hI : MeasurableSet I) (hsub : I ⊆ Set.Ioi 0) : vEl M x * star (vEl M x) * projx M x I = projx M x I

The two pairings

theorem CommutingRepetition.GraphMod.indicator_one_mul_eq {J : Set ℝ} (f : ℝ → ℝ) (t : ℝ) : J.indicator 1 t * f t = J.indicator f t

theorem CommutingRepetition.GraphMod.inner_PE_ψn (M : StdTracialAlgebra) (x : M.H) {J : Set ℝ} (hJ : MeasurableSet J) (n : ℕ) : inner ℂ ((BorelCalc.P (Eop M x) ⋯ J) M.traceVector) ((BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) = ↑(∫ (t : ℝ), J.indicator 1 t * ψn n t ∂BorelCalc.ν (Eop M x) ⋯ M.traceVector)

⟪P J Ω, ψₙ(E) Ω⟫ = ∫ 1_J ψₙ dν_Ω.

theorem CommutingRepetition.GraphMod.inner_ψn_PE_ψn (M : StdTracialAlgebra) (x : M.H) {J : Set ℝ} (hJ : MeasurableSet J) (n : ℕ) : inner ℂ ((BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) ((BorelCalc.P (Eop M x) ⋯ J) ((BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector)) = ↑(∫ (t : ℝ), ψn n t * (J.indicator 1 t * ψn n t) ∂BorelCalc.ν (Eop M x) ⋯ M.traceVector)

⟪ψₙ(E) Ω, P J ψₙ(E) Ω⟫ = ∫ ψₙ 1_J ψₙ dν_Ω.

theorem CommutingRepetition.GraphMod.indicator_ψn_mono {J : Set ℝ} (t : ℝ) : Monotone fun (n : ℕ) => J.indicator 1 t * ψn n t

theorem CommutingRepetition.GraphMod.indicator_ψn_tendsto {J : Set ℝ} (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => J.indicator 1 t * ψn n t) Filter.atTop (nhds (J.indicator ψ t))

theorem CommutingRepetition.GraphMod.indicator_ψn_ψn_mono {J : Set ℝ} (t : ℝ) : Monotone fun (n : ℕ) => ψn n t * (J.indicator 1 t * ψn n t)

theorem CommutingRepetition.GraphMod.indicator_ψn_ψn_tendsto {J : Set ℝ} (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => ψn n t * (J.indicator 1 t * ψn n t)) Filter.atTop (nhds (J.indicator (fun (t : ℝ) => ψ t ^ 2) t))

theorem CommutingRepetition.GraphMod.pairing1 (M : StdTracialAlgebra) (x : M.H) {I : Set ℝ} (hI : MeasurableSet I) : inner ℂ (M.vnModel.ι (projx M x I)) (hvec M x) = ↑(∫ (b : ℝ) in I, b ∂μx M x)

The first pairing: ⟪P(ψ⁻¹I) Ω, hvec⟫ = ∫_I b dμ.

theorem CommutingRepetition.GraphMod.J_PE_hvec (M : StdTracialAlgebra) (x : M.H) {J : Set ℝ} (hJ : MeasurableSet J) : M.J ((BorelCalc.P (Eop M x) ⋯ J) (hvec M x)) = (BorelCalc.P (Eop M x) ⋯ J) (hvec M x)

theorem CommutingRepetition.GraphMod.pairing2 (M : StdTracialAlgebra) (x : M.H) {I : Set ℝ} (hI : MeasurableSet I) : inner ℂ (hvec M x) ((M.vnModel.Rop (projx M x I)) (hvec M x)) = ↑(∫ (b : ℝ) in I, b ^ 2 ∂μx M x)

The second pairing: ⟪hvec, Rop (P(ψ⁻¹I)) hvec⟫ = ∫_I b² dμ.

Assembly

noncomputable def CommutingRepetition.GraphMod.spectralData (M : StdTracialAlgebra) (x : M.H) : SpectralData M.vnModel x

The left-modulus spectral package of x in the von Neumann model.

Equations

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

theorem CommutingRepetition.GraphMod.spectralData_hvec (M : StdTracialAlgebra) (x : M.H) : (spectralData M x).hvec = hvec M x

theorem CommutingRepetition.GraphMod.spectralData_μ (M : StdTracialAlgebra) (x : M.H) : (spectralData M x).μ = μx M x

theorem CommutingRepetition.GraphMod.spectralData_proj (M : StdTracialAlgebra) (x : M.H) (I : Set ℝ) : ↑((spectralData M x).proj I) = BorelCalc.P (Eop M x) ⋯ (ψ ⁻¹' I)