RankOne.lean`

57 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_state_jensen line 26
def OAI.SharpLiebThirring.MatrixProof.unitaryState line 55
Source documentation
A diagonal entry after unitary conjugation is a positive unital state.
```
def unitaryState (U : unitary (Matrix n n ℂ)) (i : n) : Matrix n n ℂ →L[ℝ] ℝ :=
…
```
lemma OAI.SharpLiebThirring.MatrixProof.unitaryState_apply line 61
lemma OAI.SharpLiebThirring.MatrixProof.unitaryState_positive line 64
lemma OAI.SharpLiebThirring.MatrixProof.unitaryState_one line 70
lemma OAI.SharpLiebThirring.MatrixProof.state_quadratic_nonneg line 73
lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_nonneg_implies_quadratic line 86
def OAI.SharpLiebThirring.MatrixProof.diagonalFieldIntegrand line 108
lemma OAI.SharpLiebThirring.MatrixProof.continuous_diagonalFieldIntegrand line 113
lemma OAI.SharpLiebThirring.MatrixProof.diagonalField_cutoff_limit line 119
lemma OAI.SharpLiebThirring.MatrixProof.quadraticMatrix_sub_diagonal line 149
lemma OAI.SharpLiebThirring.MatrixProof.fieldIntegrand_tangent line 162
lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_diagonal_tangent line 183
lemma OAI.SharpLiebThirring.MatrixProof.phaseUnitary_conj_diagonal line 217
lemma OAI.SharpLiebThirring.MatrixProof.trace_conjugate_difference_zero line 226
lemma OAI.SharpLiebThirring.MatrixProof.fieldIntegrand_trace_phase_nonneg line 233
lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_trace_phase_nonneg line 260
lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_tangentSchur_contraction line 288
lemma OAI.SharpLiebThirring.MatrixProof.tangentSchur_sub_smul_one line 302
def OAI.SharpLiebThirring.MatrixProof.vectorMass line 312
lemma OAI.SharpLiebThirring.MatrixProof.vectorMass_nonneg line 315
lemma OAI.SharpLiebThirring.MatrixProof.vectorMass_eq_zero line 319
lemma OAI.SharpLiebThirring.MatrixProof.dot_star_self_vectorMass line 324
lemma OAI.SharpLiebThirring.MatrixProof.rankone_trace line 329
lemma OAI.SharpLiebThirring.MatrixProof.rankone_square line 333
lemma OAI.SharpLiebThirring.MatrixProof.rankone_tracePair_positive line 339
lemma OAI.SharpLiebThirring.MatrixProof.rankone_tracePair_monotone line 344
lemma OAI.SharpLiebThirring.MatrixProof.rankone_tracePair_one line 350
lemma OAI.SharpLiebThirring.MatrixProof.rankone_tracePair_self line 353

lemma OAI.SharpLiebThirring.MatrixProof.rankone_diagonal_comparison line 360

Source documentation

The rank-one comparison in an arbitrary eigenbasis of B. No positivity of C - B² is assumed; its needed trace bound is obtained by contraction.

lemma rankone_diagonal_comparison {σ δ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hδ : 0 < δ)
    {C : Matrix n n ℂ} (hC : C.IsHermitian) (z : n → ℝ) (a : n → ℂ)
    (hM : hermitianField σ δ C (diagonal (fun i ↦ (z i : ℂ))) = vecMulVec a (star a)) :
    (vectorMass a) ^ (1 + 1 / σ) ≤
      (trace (vecMulVec a (star a) * (C - diagonal (fun i ↦ ((z i ^ 2 : ℝ) : ℂ))))).re := by
…

Mentions: OAI.SharpLiebThirring.MatrixProof.hermitianField, OAI.SharpLiebThirring.MatrixProof.vectorMass

def OAI.SharpLiebThirring.MatrixProof.unitaryConjCLM line 405
lemma OAI.SharpLiebThirring.MatrixProof.unitaryConjCLM_apply line 411
lemma OAI.SharpLiebThirring.MatrixProof.quadraticMatrix_conj line 414
lemma OAI.SharpLiebThirring.MatrixProof.cfc_unitary_conj line 423
lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_conj line 429
lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_conj line 437
lemma OAI.SharpLiebThirring.MatrixProof.unitary_conj_rankone line 447
lemma OAI.SharpLiebThirring.MatrixProof.vectorMass_unitary line 453

lemma OAI.SharpLiebThirring.MatrixProof.rankone_hermitian_comparison line 460

Source documentation

The complete complex Hermitian rank-one comparison, before identifying the real symmetric field with its complexification.

lemma rankone_hermitian_comparison {σ δ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hδ : 0 < δ)
    {C B : Matrix n n ℂ} (hC : C.IsHermitian) (hB : B.IsHermitian) (a : n → ℂ)
    (hM : hermitianField σ δ C B = vecMulVec a (star a)) :
    (vectorMass a) ^ (1 + 1 / σ) ≤ (trace (vecMulVec a (star a) * (C - B ^ 2))).re := by
…

Mentions: OAI.SharpLiebThirring.MatrixProof.hermitianField, OAI.SharpLiebThirring.MatrixProof.vectorMass

def OAI.SharpLiebThirring.MatrixProof.complexify line 496
lemma OAI.SharpLiebThirring.MatrixProof.complexify_apply line 503
def OAI.SharpLiebThirring.MatrixProof.complexifyCLM line 505
lemma OAI.SharpLiebThirring.MatrixProof.complexifyCLM_apply line 508
def OAI.SharpLiebThirring.MatrixProof.realPartCLM line 510
lemma OAI.SharpLiebThirring.MatrixProof.realPartCLM_complexify line 516
lemma OAI.SharpLiebThirring.MatrixProof.complexify_hermitian line 520
lemma OAI.SharpLiebThirring.MatrixProof.complexify_cfc line 524
lemma OAI.SharpLiebThirring.MatrixProof.complexify_diagonal line 529
lemma OAI.SharpLiebThirring.MatrixProof.complexify_vecMulVec line 534
lemma OAI.SharpLiebThirring.MatrixProof.vectorMass_ofReal line 540
lemma OAI.SharpLiebThirring.MatrixProof.complexify_trace_real line 543
lemma OAI.SharpLiebThirring.MatrixProof.matrixX_hermitian line 546
lemma OAI.SharpLiebThirring.MatrixProof.complexify_matrixX line 551
lemma OAI.SharpLiebThirring.MatrixProof.complexify_truncatedField line 557
lemma OAI.SharpLiebThirring.MatrixProof.complexify_matrixField line 576

theorem OAI.SharpLiebThirring.MatrixProof.source_rankone_comparison line 601

Source documentation

The rank-one comparison for the real field with its symmetric-cutoff definition.

theorem source_rankone_comparison {N : ℕ} {σ δ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1)
    (hδ : 0 < δ) (k : Fin N → ℝ) {B : Matrix (Fin N) (Fin N) ℝ} (hB : B.IsHermitian)
    (a : Fin N → ℝ) (hM : matrixField σ δ k B = vecMulVec a a) :
    (∑ i, a i ^ 2) ^ (1 + 1 / σ) ≤
      ∑ i, a i * ((diagonal (fun i ↦ k i ^ 2) - B ^ 2) *ᵥ a) i := by
…

Mentions: OAI.SharpLiebThirring.matrixField

theorem OAI.SharpLiebThirring.MatrixProof.rankOneClaim line 616