TraceRank.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.sq_sum_le_support_card_mul_sum_sq line 11

Source documentation

Cauchy--Schwarz with only the nonzero summands counted.

theorem sq_sum_le_support_card_mul_sum_sq {ι : Type*} [Fintype ι]
    (f : ι → ℝ) :
    (∑ i, f i) ^ 2 ≤ (Fintype.card {i // f i ≠ 0} : ℝ) * ∑ i, f i ^ 2 := by
…

theorem OAI.Problem335.hermitian_trace_sq_eq_sum_eigenvalues_sq line 27

Source documentation

The second spectral moment of a Hermitian matrix.

theorem hermitian_trace_sq_eq_sum_eigenvalues_sq {ι : Type*} [Fintype ι]
    [DecidableEq ι] {A : Matrix ι ι ℂ} (hA : A.IsHermitian) :
    (A ^ 2).trace = ∑ i, ((hA.eigenvalues i : ℂ) ^ 2) := by
…

theorem OAI.Problem335.hermitian_trace_sq_le_rank_mul_trace_sq line 37
Source documentation
The trace-rank bound used in the moment method. Positivity is not needed for this squared formulation: Hermitian symmetry suffices.
```
theorem hermitian_trace_sq_le_rank_mul_trace_sq {ι : Type*} [Fintype ι]
    [DecidableEq ι] {A : Matrix ι ι ℂ} (hA : A.IsHermitian) :
    A.trace.re ^ 2 ≤ (A.rank : ℝ) * (A ^ 2).trace.re := by
…
```

theorem OAI.Problem335.hermitian_trace_sq_pos line 46

Source documentation

A nonzero Hermitian matrix has strictly positive second moment.

theorem hermitian_trace_sq_pos {ι : Type*} [Fintype ι]
    [DecidableEq ι] {A : Matrix ι ι ℂ} (hA : A.IsHermitian) (hne : A ≠ 0) :
    0 < (A ^ 2).trace.re := by
…

theorem OAI.Problem335.hermitian_rank_ge_trace_ratio line 58

Source documentation

The ratio form of the trace-rank bound.

theorem hermitian_rank_ge_trace_ratio {ι : Type*} [Fintype ι]
    [DecidableEq ι] {A : Matrix ι ι ℂ} (hA : A.IsHermitian)
    (hsecond : 0 < (A ^ 2).trace.re) :
    A.trace.re ^ 2 / (A ^ 2).trace.re ≤ (A.rank : ℝ) := by
…

theorem OAI.Problem335.gram_rank_ge_trace_ratio line 67

Source documentation

Applied to the Gram matrix, the moment method bounds the rank of the original rectangular matrix.

theorem gram_rank_ge_trace_ratio {ι κ : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq κ] (A : Matrix ι κ ℂ)
    (hsecond : 0 < ((A.conjTranspose * A) ^ 2).trace.re) :
    (A.conjTranspose * A).trace.re ^ 2 / ((A.conjTranspose * A) ^ 2).trace.re ≤ (A.rank : ℝ) := by
…