OAI/Analysis/LiebThirring/MatrixTangent.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.MatrixProof.gaussianSchur line 24

   Source documentation

   The Schur action obtained by one Gaussian average.

   def gaussianSchur (z : n → ℝ) (v h : ℝ) (D : Matrix n n ℂ) : Matrix n n ℂ :=
   …

2. lemma OAI.SharpLiebThirring.MatrixProof.gaussianSchur_eq_average line 27
3. lemma OAI.SharpLiebThirring.MatrixProof.gaussianSchur_norm_le line 42
4. lemma OAI.SharpLiebThirring.MatrixProof.continuous_gaussianSchur line 59
5. lemma OAI.SharpLiebThirring.MatrixProof.gamma_integrable_gaussianSchur line 68
6. def OAI.SharpLiebThirring.MatrixProof.powerSchur line 78
7. lemma OAI.SharpLiebThirring.MatrixProof.gamma_gaussianSchur_integral line 81
8. lemma OAI.SharpLiebThirring.MatrixProof.powerSchur_trace_comparison line 94
9. def OAI.SharpLiebThirring.MatrixProof.tangentSchur line 123
10. lemma OAI.SharpLiebThirring.MatrixProof.continuousOn_powerSchur_tau line 127
11. lemma OAI.SharpLiebThirring.MatrixProof.integrable_powerSchur_tau line 143
12. lemma OAI.SharpLiebThirring.MatrixProof.tangentSchur_trace_comparison line 148
13. lemma OAI.SharpLiebThirring.MatrixProof.tangentSchur_one line 163
14. lemma OAI.SharpLiebThirring.MatrixProof.tangentSchur_selfAdjoint line 174
15. def OAI.SharpLiebThirring.MatrixProof.quadraticTangent line 203
16. lemma OAI.SharpLiebThirring.MatrixProof.integrable_quadraticTangent line 206
17. lemma OAI.SharpLiebThirring.MatrixProof.tangentSchur_apply line 220
18. lemma OAI.SharpLiebThirring.MatrixProof.integral_quadraticTangent line 233

    Source documentation

    Exact integrated tangent map in any diagonalizing basis, not only simple spectrum.

    lemma integral_quadraticTangent {σ δ d : ℝ} (hσ : σ < 1) (hδ : 0 < δ)
        (hd : 0 ≤ d) (z : n → ℝ) (Z : Matrix n n ℂ) :
        fieldNormalization σ • ∫ s : ℝ, quadraticTangent σ δ d z Z s =
          (σ * (d + δ) ^ (σ - 1)) • tangentSchur σ (d + δ) z Z := by
    …

    Mentions: OAI.SharpLiebThirring.fieldNormalization, OAI.SharpLiebThirring.MatrixProof.quadraticTangent, OAI.SharpLiebThirring.MatrixProof.tangentSchur

19. lemma OAI.SharpLiebThirring.MatrixProof.primitive_diagonal_tangent line 254
20. lemma OAI.SharpLiebThirring.ScalarProof.primitive_le_tangent line 271
21. lemma OAI.SharpLiebThirring.MatrixProof.primitive_state_jensen line 298

    Source documentation

    Scalar Jensen inequality for every positive unital real-linear matrix state. No assertion of operator concavity on the whole line is used.

    lemma primitive_state_jensen {σ δ : ℝ} (hσ : σ < 1) (hδ : 0 < δ)
        (φ : Matrix n n ℂ →ₗ[ℝ] ℝ) (hφ : ∀ A, A.PosSemidef → 0 ≤ φ A)
        (hφ₁ : φ 1 = 1) {A : Matrix n n ℂ} (hA : A.IsHermitian) :
        φ (cfc (regularizedPrimitive σ δ) A) ≤ regularizedPrimitive σ δ (φ A) := by
    …

    Mentions: OAI.SharpLiebThirring.regularizedPrimitive