Measurability of spectral sublevel projectors

For a measurable family of self-adjoint real matrices, the orthogonal projection onto the eigenspace for eigenvalues ≤ t is measurable in the parameter. Since this projector is the continuous functional calculus of the discontinuous indicator Set.indicator (Set.Iic t) 1, measurability is obtained by approximating the indicator from above by continuous downward ramps gApprox t m, whose CFCs are measurable, and passing to the entrywise pointwise limit. The main results are measurable_spectralProjector and its specialization measurable_slowProjector to the sanitized Oseledets limit lambdaHat.

noncomputable def Oseledets.gApprox (t : ℝ) (m : ℕ) : ℝ → ℝ

A continuous approximation to indicator (Iic t) 1: a downward ramp from 1 (at s = t) to 0 (at s = t + 1/(m+1)), clamped to [0,1].

Equations

• Oseledets.gApprox t m s = max 0 (min 1 ((t + 1 / (↑m + 1) - s) * (↑m + 1)))

theorem Oseledets.continuous_gApprox (t : ℝ) (m : ℕ) : Continuous (gApprox t m)

theorem Oseledets.gApprox_of_le (t : ℝ) (m : ℕ) {s : ℝ} (hs : s ≤ t) : gApprox t m s = 1

For s ≤ t, the ramp is exactly 1, agreeing with the indicator.

theorem Oseledets.gApprox_eventually_zero (t : ℝ) {s : ℝ} (hs : t < s) : ∀ᶠ (m : ℕ) in Filter.atTop, gApprox t m s = 0

For s > t, eventually (once 1/(m+1) < s - t) the ramp is 0, agreeing with the indicator.

theorem Oseledets.gApprox_eventually_eq_indicator (t s : ℝ) : ∀ᶠ (m : ℕ) in Filter.atTop, gApprox t m s = (Set.Iic t).indicator 1 s

At every point, gApprox t m s is eventually equal to indicator (Iic t) 1 s.

theorem Oseledets.tendstoUniformlyOn_gApprox (t : ℝ) {S : Set ℝ} (hS : S.Finite) : TendstoUniformlyOn (gApprox t) ((Set.Iic t).indicator 1) Filter.atTop S

Uniform convergence on the finite spectrum: on a finite set, the eventual pointwise equality of gApprox t m with the indicator upgrades to uniform convergence.

theorem Oseledets.tendsto_cfc_gApprox {d : ℕ} (t : ℝ) (M : Matrix (Fin d) (Fin d) ℝ) : Filter.Tendsto (fun (m : ℕ) => cfc (gApprox t m) M) Filter.atTop (nhds (cfc ((Set.Iic t).indicator 1) M))

Spectral CFC convergence. For a self-adjoint matrix M, the continuous CFCs of the ramp gApprox t m converge (in the matrix topology) to the CFC of the discontinuous indicator.

theorem Oseledets.measurable_spectralProjector {X : Type u_1} [MeasurableSpace X] {d : ℕ} (t : ℝ) (M : X → Matrix (Fin d) (Fin d) ℝ) (hM : Measurable M) (hMsa : ∀ (x : X), IsSelfAdjoint (M x)) : Measurable fun (x : X) => cfc ((Set.Iic t).indicator 1) (M x)

For a measurable family M : X → matrix of self-adjoint real matrices, the spectral sublevel projector x ↦ cfc (Set.indicator (Set.Iic t) 1) (M x) — the orthogonal projection onto the ≤ t eigenspace — is measurable. The indicator is discontinuous, so this is obtained as the entrywise pointwise limit of the measurable continuous-CFC ramps cfc (gApprox t m) (M x).

theorem Oseledets.measurable_slowProjector {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (t : ℝ) (hAmeas : Measurable A) (hTmeas : Measurable T) : Measurable fun (x : X) => slowProjector A T t x

Measurability of the slow (sublevel) spectral projector family x ↦ slowProjector A T t x = cfc (indicator (Iic t) 1) (lambdaHat A T x), obtained by composing the spectral-projector measurability with the measurability and everywhere self-adjointness of the sanitized Oseledets limit lambdaHat.