OAI/Analysis/LiebThirring/MatrixOrder.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

The matrix field and action

  1. def OAI.SharpLiebThirring.regularizedPrimitive line 17

    Source documentation

    The regularized primitive, including beta = 0 without a special convention.

    def regularizedPrimitive (σ δ y : ℝ) : ℝ :=
…
  2. def OAI.SharpLiebThirring.fieldNormalization line 20
  3. def OAI.SharpLiebThirring.scalarMu line 23
  4. def OAI.SharpLiebThirring.matrixX line 30
  5. def OAI.SharpLiebThirring.truncatedField line 36

    Source documentation

    The symmetric cutoff is part of the definition, not replaced by a potentially non-absolutely-convergent whole-line Bochner integral.

    def truncatedField (σ δ : ℝ) (k : Fin N → ℝ) (B : Matrix (Fin N) (Fin N) ℝ)
    (R : ℝ) : Matrix (Fin N) (Fin N) ℝ :=
…
  6. def OAI.SharpLiebThirring.matrixField line 43

    Source documentation

    The symmetric-cutoff limit, whose convergence and local regularity are proved below.

    def matrixField (σ δ : ℝ) (k : Fin N → ℝ) (B : Matrix (Fin N) (Fin N) ℝ) :
    Matrix (Fin N) (Fin N) ℝ :=
…
  7. def OAI.SharpLiebThirring.fieldPrimitive line 47
  8. def OAI.SharpLiebThirring.RankOneClaim line 51

    Source documentation

    The rank-one comparison for the symmetric-cutoff matrix field.

    def RankOneClaim : Prop :=
…
  9. structure OAI.SharpLiebThirring.H10 line 60

    Source documentation

    The real continuous representative of H¹₀ on a bounded interval.

    structure H10 (l r : ℝ) where
…
  10. def OAI.SharpLiebThirring.LowerTriangular line 72
  11. def OAI.SharpLiebThirring.finiteIntervalAction line 75
  12. def OAI.SharpLiebThirring.ActionClaim line 84

    Source documentation

    The action inequality, with an extended-real supremum so boundedness is not implicit.

    def ActionClaim : Prop :=
…
  13. lemma OAI.SharpLiebThirring.MatrixProof.monotone_sub_mul_nonneg line 98
  14. lemma OAI.SharpLiebThirring.MatrixProof.trace_star_mul_sum line 105
  15. lemma OAI.SharpLiebThirring.MatrixProof.trace_star_mul_change line 111
  16. lemma OAI.SharpLiebThirring.MatrixProof.mixed_diagonal_sub line 129
  17. lemma OAI.SharpLiebThirring.MatrixProof.mixed_diagonal_sub_apply line 143
  18. lemma OAI.SharpLiebThirring.MatrixProof.trace_functional_monotonicity line 153
  19. lemma OAI.SharpLiebThirring.MatrixProof.trace_unitary_conjugate line 194
  20. lemma OAI.SharpLiebThirring.MatrixProof.trace_conjugate_pair line 199
  21. lemma OAI.SharpLiebThirring.MatrixProof.trace_conjugate_difference line 211
  22. lemma OAI.SharpLiebThirring.MatrixProof.hermitian_unitary_conjugate line 222
  23. lemma OAI.SharpLiebThirring.MatrixProof.functional_unitary_conjugate line 227
  24. lemma OAI.SharpLiebThirring.MatrixProof.trace_unitary_comparison line 240

    Source documentation

    The fixed-unitary trace comparison used before averaging.

    lemma trace_unitary_comparison {A : Matrix n n ℂ} (hA : A.IsHermitian)
    {f : ℝ → ℝ} (hf : Monotone f) (U : unitary (Matrix n n ℂ)) :
    0 ≤ (trace (hA.cfc f * (2 • A - conjStarAlgAut ℂ (Matrix n n ℂ) U A -
      conjStarAlgAut ℂ (Matrix n n ℂ) (star U) A))).re := by
…
  25. lemma OAI.SharpLiebThirring.MatrixProof.conjugate_difference_sub_invariant line 249

    Source documentation

    Removing any invariant part, such as (s I - B)^2, is an exact identity.

    lemma conjugate_difference_sub_invariant (U : unitary (Matrix n n ℂ))
    (D Y : Matrix n n ℂ) (hY : conjStarAlgAut ℂ (Matrix n n ℂ) U Y = Y) :
    2 • (D + Y) - conjStarAlgAut ℂ (Matrix n n ℂ) U (D + Y) -
        conjStarAlgAut ℂ (Matrix n n ℂ) (star U) (D + Y) =
      2 • D - conjStarAlgAut ℂ (Matrix n n ℂ) U D - conjStarAlgAut ℂ (Matrix n n ℂ) (star U) D := by
…
  26. lemma OAI.SharpLiebThirring.MatrixProof.trace_unitary_comparison_sub_invariant line 262
  27. def OAI.SharpLiebThirring.MatrixProof.hsSquared line 272

    Source documentation

    The squared Hilbert--Schmidt norm, without changing the ambient matrix norm.

    def hsSquared (A : Matrix n n ℂ) : ℝ := ∑ i, ∑ j, Complex.normSq (A i j)
…
  28. lemma OAI.SharpLiebThirring.MatrixProof.hsSquared_eq_trace line 275
  29. lemma OAI.SharpLiebThirring.MatrixProof.hsSquared_change line 284
  30. lemma OAI.SharpLiebThirring.MatrixProof.hsSquared_cfc_sub line 290

    Source documentation

    The finite-dimensional Hilbert--Schmidt calculus estimate, proved in mixed eigenbases.

    lemma hsSquared_cfc_sub {A B : Matrix n n ℂ}
    (hA : A.IsHermitian) (hB : B.IsHermitian) (f : ℝ → ℝ) (L : ℝ) (hL : 0 ≤ L)
    (hf : ∀ i j, |f (hA.eigenvalues i) - f (hB.eigenvalues j)| ≤
      L * |hA.eigenvalues i - hB.eigenvalues j|) :
    hsSquared (hA.cfc f - hB.cfc f) ≤ L ^ 2 * hsSquared (A - B) := by
…

    Mentions: OAI.SharpLiebThirring.MatrixProof.hsSquared

  31. def OAI.SharpLiebThirring.MatrixProof.tracePairCLM line 332

    Source documentation

    Real trace pairing as a continuous linear functional.

    def tracePairCLM (M : Matrix n n ℂ) : Matrix n n ℂ →L[ℝ] ℝ :=
…
  32. lemma OAI.SharpLiebThirring.MatrixProof.tracePairCLM_apply line 337
  33. lemma OAI.SharpLiebThirring.MatrixProof.trace_unitary_comparison_limit line 341

    Source documentation

    Trace comparison commutes with limits in matrix norm.

    lemma trace_unitary_comparison_limit {ι : Type u2} {l : Filter ι} [l.NeBot]
    {F : ι → Matrix n n ℂ} {M D : Matrix n n ℂ}
    (hlim : Filter.Tendsto F l (nhds M)) (U : unitary (Matrix n n ℂ))
    (hF : ∀ᶠ i in l, 0 ≤ (trace (F i * (2 • D - conjStarAlgAut ℂ (Matrix n n ℂ) U D -
      conjStarAlgAut ℂ (Matrix n n ℂ) (star U) D))).re) :
    0 ≤ (trace (M * (2 • D - conjStarAlgAut ℂ (Matrix n n ℂ) U D -
      conjStarAlgAut ℂ (Matrix n n ℂ) (star U) D))).re := by
…
  34. lemma OAI.SharpLiebThirring.MatrixProof.trace_comparison_average line 358

    Source documentation

    The integration step in trace-average, for any symmetric probability average. The symmetry needed is expressed by equality of the two integrals.

    lemma trace_comparison_average {α : Type u3} [MeasurableSpace α] (ν : Measure α)
    [IsProbabilityMeasure ν] (U : α → unitary (Matrix n n ℂ))
    (M D : Matrix n n ℂ)
    (hU : Integrable (fun t ↦ conjStarAlgAut ℂ (Matrix n n ℂ) (U t) D) ν)
    (hUs : Integrable (fun t ↦ conjStarAlgAut ℂ (Matrix n n ℂ) (star (U t)) D) ν)
    (hsym : (∫ t, conjStarAlgAut ℂ (Matrix n n ℂ) (star (U t)) D ∂ν) =
      ∫ t, conjStarAlgAut ℂ (Matrix n n ℂ) (U t) D ∂ν)
    (hpoint : ∀ᵐ t ∂ν, 0 ≤ (trace (M * (2 • D - conjStarAlgAut ℂ (Matrix n n ℂ) (U t) D -
      conjStarAlgAut ℂ (Matrix n n ℂ) (star (U t)) D))).re) :
    (trace (M * (∫ t, conjStarAlgAut ℂ (Matrix n n ℂ) (U t) D ∂ν))).re ≤
      (trace (M * D)).re := by
…
  35. def OAI.SharpLiebThirring.MatrixProof.phaseUnitary line 385

    Source documentation

    In a fixed eigenbasis of B, the unitary exp(itB).

    def phaseUnitary (z : n → ℝ) (t : ℝ) : unitary (Matrix n n ℂ) :=
…
  36. lemma OAI.SharpLiebThirring.MatrixProof.phaseUnitary_conj_apply line 403
  37. lemma OAI.SharpLiebThirring.MatrixProof.phaseUnitary_star line 419
  38. lemma OAI.SharpLiebThirring.MatrixProof.continuous_phase_conj line 429
  39. lemma OAI.SharpLiebThirring.MatrixProof.integrable_phase_conj line 438
  40. def OAI.SharpLiebThirring.MatrixProof.entryCLM line 448

    Source documentation

    Entry evaluation is a continuous linear functional even for the operator norm.

    def entryCLM (i j : n) : Matrix n n ℂ →L[ℝ] ℂ :=
…
  41. lemma OAI.SharpLiebThirring.MatrixProof.entryCLM_apply line 454
  42. lemma OAI.SharpLiebThirring.MatrixProof.gaussian_phase_average line 456
  43. lemma OAI.SharpLiebThirring.MatrixProof.gaussian_phase_star_average line 471
  44. lemma OAI.SharpLiebThirring.MatrixProof.integrable_gaussian_phase_star line 487
  45. lemma OAI.SharpLiebThirring.MatrixProof.gaussian_trace_comparison line 499

    Source documentation

    The Gaussian stage of the even-unitary trace contraction.

    lemma gaussian_trace_comparison (z : n → ℝ) (M D : Matrix n n ℂ) (v : ℝ≥0)
    (hpoint : ∀ t : ℝ, 0 ≤ (trace (M * (2 • D -
      conjStarAlgAut ℂ (Matrix n n ℂ) (phaseUnitary z t) D -
      conjStarAlgAut ℂ (Matrix n n ℂ) (star (phaseUnitary z t)) D))).re) :
    (trace (M * (∫ t, conjStarAlgAut ℂ (Matrix n n ℂ) (phaseUnitary z t) D
      ∂ProbabilityTheory.gaussianReal 0 v))).re ≤ (trace (M * D)).re := by
…

    Mentions: OAI.SharpLiebThirring.MatrixProof.phaseUnitary

  46. lemma OAI.SharpLiebThirring.ScalarProof.derivative_continuous line 516
  47. lemma OAI.SharpLiebThirring.ScalarProof.primitive_hasDerivAt line 524
  48. lemma OAI.SharpLiebThirring.ScalarProof.primitive_deriv line 530
  49. lemma OAI.SharpLiebThirring.ScalarProof.primitive_differentiable line 534
  50. lemma OAI.SharpLiebThirring.ScalarProof.primitive_strictMono line 538
  51. lemma OAI.SharpLiebThirring.ScalarProof.primitive_concave line 545
  52. lemma OAI.SharpLiebThirring.ScalarProof.primitive_zero line 553
  53. lemma OAI.SharpLiebThirring.ScalarProof.primitive_nonneg line 556
  54. lemma OAI.SharpLiebThirring.ScalarProof.normalization_integrable line 560
  55. lemma OAI.SharpLiebThirring.ScalarProof.normalization_integral_pos line 572
  56. lemma OAI.SharpLiebThirring.ScalarProof.normalization_pos line 584
  57. lemma OAI.SharpLiebThirring.ScalarProof.mu_zero line 588
  58. lemma OAI.SharpLiebThirring.ScalarProof.shifted_base_lower line 594

    Source documentation

    A global comparison with the Japanese-bracket integrable majorant, including negative shifts. It supplies all scalar dominated-convergence bounds.

    lemma shifted_base_lower {δ : ℝ} (hδ : 0 < δ) (z s : ℝ) :
    (δ / (δ + |z| + 1)) * (1 + s ^ 2) ≤ max (s ^ 2 + z) 0 + δ := by
…
  59. lemma OAI.SharpLiebThirring.ScalarProof.shifted_derivative_integrable line 606
  60. lemma OAI.SharpLiebThirring.ScalarProof.primitive_difference_bound line 618
  61. lemma OAI.SharpLiebThirring.ScalarProof.mu_integrand_integrable line 640
  62. lemma OAI.SharpLiebThirring.ScalarProof.mu_hasDerivAt_integral line 650
  63. lemma OAI.SharpLiebThirring.ScalarProof.mu_strictMono line 674
  64. lemma OAI.SharpLiebThirring.ScalarProof.quadratic_integral_scale line 691

    Source documentation

    The scaling integral used in the evaluation of the scalar field.

    lemma quadratic_integral_scale (t : ℝ) {a : ℝ} (ha : 0 < a) :
    (∫ s : ℝ, (s ^ 2 + a) ^ t) =
      a ^ (t + 1 / 2) * ∫ s : ℝ, (1 + s ^ 2) ^ t := by
…
  65. lemma OAI.SharpLiebThirring.ScalarProof.mu_hasDerivAt_nonneg line 707
  66. lemma OAI.SharpLiebThirring.ScalarProof.mu_eq_nonneg line 723
  67. def OAI.SharpLiebThirring.ScalarProof.gammaWeight line 741

    Source documentation

    Normalized Gamma mixing density, used only on the positive half-line.

    def gammaWeight (σ v : ℝ) : ℝ :=
…
  68. lemma OAI.SharpLiebThirring.ScalarProof.gammaWeight_nonneg line 744
  69. lemma OAI.SharpLiebThirring.ScalarProof.gammaWeight_integrable line 750
  70. lemma OAI.SharpLiebThirring.ScalarProof.gamma_mixture line 757
  71. lemma OAI.SharpLiebThirring.ScalarProof.gammaWeight_integral line 775
  72. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_kernel_integrable line 780

    Source documentation

    Integrability of the scalar kernel used in the matrix resolvent tangent formula.

    lemma resolvent_kernel_integrable {β a : ℝ} (hβ₀ : -1 < β) (hβ₁ : β < 1)
    (ha : 0 < a) : IntegrableOn (fun v : ℝ ↦ v ^ β / (a + v) ^ 2) (Ioi 0) := by
…
  73. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_kernel_integral_scale line 809
  74. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_kernel_integral_pos line 824
  75. def OAI.SharpLiebThirring.ScalarProof.resolventDifference line 839

    Source documentation

    The scalar difference whose positive-matrix functional calculus is integrated.

    def resolventDifference (β δ y v : ℝ) : ℝ :=
…
  76. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_difference_eq line 842
  77. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_difference_integrable line 849
  78. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_integral_hasDerivAt line 878
  79. def OAI.SharpLiebThirring.ScalarProof.resolventNormalization line 915

    Source documentation

    The normalization constant for the resolvent representation.

    def resolventNormalization (β : ℝ) : ℝ :=
…
  80. lemma OAI.SharpLiebThirring.ScalarProof.resolvent_normalization_pos line 918
  81. lemma OAI.SharpLiebThirring.ScalarProof.primitive_resolvent_representation line 924

    Source documentation

    Resolvent representation of f, for every nonnegative scalar argument. The exponent sigma-1/2 may be zero or negative.

    lemma primitive_resolvent_representation {σ δ y : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1)
    (hδ : 0 < δ) (hy : 0 ≤ y) :
    regularizedPrimitive σ δ y = resolventNormalization (σ - 1 / 2) *
      ∫ v in Ioi (0 : ℝ), resolventDifference (σ - 1 / 2) δ y v := by
…

    Mentions: OAI.SharpLiebThirring.regularizedPrimitive, OAI.SharpLiebThirring.ScalarProof.resolventNormalization, OAI.SharpLiebThirring.ScalarProof.resolventDifference

  82. lemma OAI.SharpLiebThirring.ScalarProof.inverse_mu_positive line 952
  83. lemma OAI.SharpLiebThirring.ScalarProof.mu_inverse line 960
  84. lemma OAI.SharpLiebThirring.ScalarProof.mu_le_rpow line 968
  85. lemma OAI.SharpLiebThirring.ScalarProof.rankone_scalar_power line 974
  86. lemma OAI.SharpLiebThirring.MatrixProof.resolvent_remainder line 991

    Source documentation

    Exact resolvent remainder. All inverses are the ordinary finite-matrix inverse; invertibility is provided by the positive-definiteness hypotheses.

    lemma resolvent_remainder (A B : Matrix n n ℂ) (hA : IsUnit A) (hB : IsUnit B) :
    -A⁻¹ + A⁻¹ * (B - A) * A⁻¹ - (-B⁻¹) =
      (A⁻¹ * (B - A)) * B⁻¹ * ((B - A) * A⁻¹) := by
…
  87. lemma OAI.SharpLiebThirring.MatrixProof.resolvent_tangent line 1005

    Source documentation

    The resolvent tangent inequality before integration.

    lemma resolvent_tangent {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) :
    -B⁻¹ ≤ -A⁻¹ + A⁻¹ * (B - A) * A⁻¹ := by
…
  88. lemma OAI.SharpLiebThirring.compact_penalty line 1019

    Source documentation

    The compact penalty lemma. No differentiability or convergence of the selected paths is required.

    lemma compact_penalty {X : Type u5} [TopologicalSpace X] {K : Set X}
    (hK : IsCompact K) {f g : X → ℝ} (hf : Continuous f) (hg : Continuous g)
    (hg₀ : ∀ x ∈ K, 0 ≤ g x) (hzero : ∀ x ∈ K, g x = 0 → f x ≤ 0)
    {η : ℝ} (hη : 0 < η) :
    ∃ t₀ : ℝ, 0 < t₀ ∧ ∀ t : ℝ, 0 < t → t ≤ t₀ →
      ∀ x ∈ K, f x - g x / t ≤ η := by
…