def EigenvalueConcentration.numUpperTriEntries (n : ℕ) : ℕ

Number of entries on or above the diagonal of an $n \times n$ matrix: $n(n+1)/2$.

noncomputable def EigenvalueConcentration.largestEigenvalue {n : ℕ} [NeZero n] (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian) : ℝ

The largest eigenvalue $\lambda_1(A)$ of a Hermitian matrix $A$, defined as the first entry of its eigenvalue list.

theorem EigenvalueConcentration.eigenvalue_has_weighted_certificates {n : ℕ} [NeZero n] (s : ℕ) (hs : s = numUpperTriEntries n) (Ω : Fin s → Type u_1) [(i : Fin s) → DecidableEq (Ω i)] (toMatrix : ((i : Fin s) → Ω i) → Matrix (Fin n) (Fin n) ℝ) (hSymm : ∀ (x : (i : Fin s) → Ω i), (toMatrix x).IsHermitian) (hBdd : ∀ (x : (i : Fin s) → Ω i) (i j : Fin n), |toMatrix x i j| ≤ 1) : TalagrandWeightedCertificates.HasWeightedCertificates (fun (x : (i : Fin s) → Ω i) => largestEigenvalue (toMatrix x) ⋯) (4 * √2)

The largest-eigenvalue functional $\lambda_1$ on the space of Hermitian matrices with entries bounded by $1$ admits weighted Talagrand certificates with constant $4\sqrt{2}$.

theorem EigenvalueConcentration.largest_eigenvalue_concentration {n : ℕ} [NeZero n] (s : ℕ) (hs : s = numUpperTriEntries n) (Ω : Fin s → Type u_1) [(i : Fin s) → DecidableEq (Ω i)] [(i : Fin s) → MeasurableSpace (Ω i)] (μ : (i : Fin s) → MeasureTheory.Measure (Ω i)) [∀ (i : Fin s), MeasureTheory.IsProbabilityMeasure (μ i)] (toMatrix : ((i : Fin s) → Ω i) → Matrix (Fin n) (Fin n) ℝ) (hSymm : ∀ (x : (i : Fin s) → Ω i), (toMatrix x).IsHermitian) (hBdd : ∀ (x : (i : Fin s) → Ω i) (i j : Fin n), |toMatrix x i j| ≤ 1) (M : ℝ) (h_median_upper : ((MeasureTheory.Measure.pi μ) {x : (i : Fin s) → Ω i | (fun (ω : (i : Fin s) → Ω i) => largestEigenvalue (toMatrix ω) ⋯) x ≤ M}).toReal ≥ 1 / 2) (h_median_lower : ((MeasureTheory.Measure.pi μ) {x : (i : Fin s) → Ω i | (fun (ω : (i : Fin s) → Ω i) => largestEigenvalue (toMatrix ω) ⋯) x ≥ M}).toReal ≥ 1 / 2) (t : ℝ) : 0 ≤ t → ((MeasureTheory.Measure.pi μ) {x : (i : Fin s) → Ω i | |(fun (ω : (i : Fin s) → Ω i) => largestEigenvalue (toMatrix ω) ⋯) x - M| ≥ t}).toReal ≤ 4 * Real.exp (-t ^ 2 / 32)

Concentration of the largest eigenvalue around its median (Theorem 9.5.17): for a random Hermitian matrix with independent bounded entries, $\mathbb{P}(|\lambda_1(A) - M\lambda_1(A)| \geq t) \leq 4\exp(-t^2/32)$.