OAI/Analysis/LiebThirring/ResolventCalculus.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.MatrixProof.spectralCLM line 19

   Source documentation

   Finite spectral synthesis as a real continuous linear map.

   def spectralCLM {A : Matrix n n ℂ} (hA : A.IsHermitian) :
       (n → ℝ) →L[ℝ] Matrix n n ℂ :=
   …

2. lemma OAI.SharpLiebThirring.MatrixProof.spectralCLM_apply line 37
3. lemma OAI.SharpLiebThirring.MatrixProof.integrable_hermitian_cfc line 41
4. lemma OAI.SharpLiebThirring.MatrixProof.integral_hermitian_cfc line 47
5. lemma OAI.SharpLiebThirring.MatrixProof.cfc_shifted_inverse line 61
6. lemma OAI.SharpLiebThirring.MatrixProof.shifted_inverse_norm_le line 75
7. def OAI.SharpLiebThirring.MatrixProof.resolventMatrix line 84
8. lemma OAI.SharpLiebThirring.MatrixProof.cfc_resolventDifference line 87
9. lemma OAI.SharpLiebThirring.MatrixProof.integrable_resolventMatrix line 109
10. lemma OAI.SharpLiebThirring.MatrixProof.primitive_cfc_resolvent_representation line 122

    Source documentation

    Matrix-valued resolvent representation, not only a scalar or commuting case.

    lemma primitive_cfc_resolvent_representation {A : Matrix n n ℂ} (hA : A.PosSemidef)
        {σ δ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hδ : 0 < δ) :
        hA.isHermitian.cfc (regularizedPrimitive σ δ) =
          resolventNormalization (σ - 1 / 2) •
            ∫ v in Ioi (0 : ℝ), resolventMatrix (σ - 1 / 2) δ A v := by
    …

    Mentions: OAI.SharpLiebThirring.regularizedPrimitive, OAI.SharpLiebThirring.MatrixProof.resolventMatrix

11. def OAI.SharpLiebThirring.MatrixProof.resolventTangentKernel line 157
12. lemma OAI.SharpLiebThirring.MatrixProof.continuousOn_shifted_inverse line 160
13. lemma OAI.SharpLiebThirring.MatrixProof.integrable_resolventTangentKernel line 178
14. lemma OAI.SharpLiebThirring.MatrixProof.shifted_posDef line 201
15. lemma OAI.SharpLiebThirring.MatrixProof.resolventMatrix_le line 205
16. lemma OAI.SharpLiebThirring.MatrixProof.primitive_cfc_tangent line 219

    Source documentation

    Operator tangent inequality for every pair of positive Hermitian matrices, with a fully convergent resolvent integral.

    lemma primitive_cfc_tangent {X Y : Matrix n n ℂ} (hX : X.PosSemidef) (hY : Y.PosSemidef)
        {σ δ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hδ : 0 < δ) :
        hX.isHermitian.cfc (regularizedPrimitive σ δ) ≤
          hY.isHermitian.cfc (regularizedPrimitive σ δ) +
            resolventNormalization (σ - 1 / 2) •
              ∫ v in Ioi (0 : ℝ), resolventTangentKernel (σ - 1 / 2) δ Y (X - Y) v := by
    …

    Mentions: OAI.SharpLiebThirring.regularizedPrimitive, OAI.SharpLiebThirring.MatrixProof.resolventTangentKernel

17. def OAI.SharpLiebThirring.ScalarProof.dividedPrimitive line 245
18. lemma OAI.SharpLiebThirring.ScalarProof.convex_combo_nonneg line 248
19. lemma OAI.SharpLiebThirring.ScalarProof.continuousOn_divided_integrand line 252
20. lemma OAI.SharpLiebThirring.ScalarProof.dividedPrimitive_self line 260
21. lemma OAI.SharpLiebThirring.ScalarProof.dividedPrimitive_mul_sub line 265
22. lemma OAI.SharpLiebThirring.ScalarProof.mixed_resolvent_integrable line 285
23. lemma OAI.SharpLiebThirring.ScalarProof.mixed_resolvent_eq_divided line 307

    Source documentation

    The divided-difference coefficient, including coincident eigenvalues.

    lemma mixed_resolvent_eq_divided {σ δ x y : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1)
        (hδ : 0 < δ) (hx : 0 ≤ x) (hy : 0 ≤ y) :
        resolventNormalization (σ - 1 / 2) *
          (∫ v in Ioi (0 : ℝ), v ^ (σ - 1 / 2) / ((x + δ + v) * (y + δ + v))) =
            dividedPrimitive σ δ x y := by
    …

    Mentions: OAI.SharpLiebThirring.ScalarProof.resolventNormalization, OAI.SharpLiebThirring.ScalarProof.dividedPrimitive

24. def OAI.SharpLiebThirring.MatrixProof.diagonalStarAlgHom line 348
25. lemma OAI.SharpLiebThirring.MatrixProof.cfc_diagonal_real line 357
26. lemma OAI.SharpLiebThirring.MatrixProof.inverse_diagonal_real line 372
27. lemma OAI.SharpLiebThirring.MatrixProof.shifted_diagonal_real line 382
28. lemma OAI.SharpLiebThirring.MatrixProof.diagonal_real_posSemidef line 399
29. lemma OAI.SharpLiebThirring.MatrixProof.resolventTangentKernel_diagonal line 403
30. lemma OAI.SharpLiebThirring.MatrixProof.integral_resolventTangent_diagonal line 414
31. def OAI.SharpLiebThirring.ScalarProof.quadraticDividedIntegrand line 449
32. lemma OAI.SharpLiebThirring.ScalarProof.quadratic_combo line 452
33. lemma OAI.SharpLiebThirring.ScalarProof.quadraticDivided_integrable_left line 456
34. lemma OAI.SharpLiebThirring.ScalarProof.integral_quadraticDivided_left line 463
35. lemma OAI.SharpLiebThirring.ScalarProof.quadraticDivided_integrable_prod line 484
36. lemma OAI.SharpLiebThirring.ScalarProof.integrable_divided_quadratic line 512

    Source documentation

    Absolute convergence of the integrated tangent coefficients.

    lemma integrable_divided_quadratic {σ δ d : ℝ} (hσ : σ < 1) (hδ : 0 < δ)
        (hd : 0 ≤ d) (x y : ℝ) :
        Integrable (fun s ↦ dividedPrimitive σ δ ((s - x) ^ 2 + d) ((s - y) ^ 2 + d)) := by
    …

    Mentions: OAI.SharpLiebThirring.ScalarProof.dividedPrimitive

37. lemma OAI.SharpLiebThirring.ScalarProof.integral_divided_quadratic line 526

    Source documentation

    The integrated tangent kernel.

    lemma integral_divided_quadratic {σ δ d : ℝ} (hσ : σ < 1) (hδ : 0 < δ)
        (hd : 0 ≤ d) (x y : ℝ) :
        fieldNormalization σ *
          (∫ s : ℝ, dividedPrimitive σ δ ((s - x) ^ 2 + d) ((s - y) ^ 2 + d)) =
          σ * (d + δ) ^ (σ - 1) *
            ∫ τ in Icc (0 : ℝ) 1,
              (1 + τ * (1 - τ) / (d + δ) * (x - y) ^ 2) ^ (σ - 1) := by
    …

    Mentions: OAI.SharpLiebThirring.fieldNormalization, OAI.SharpLiebThirring.ScalarProof.dividedPrimitive