Trace/CFC scalar cutoff-resolvent provider layer

This module exposes only the trace/CFC scalar cutoff-resolvent provider layer. It is not a Lieb/Epstein sign theorem, and it does not claim arbitrary-weight cutoff removal or any improper-integral representation.

theorem HighDimProb.trace_cfc_eq_sum_of_isHermitian_RCLike {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (f : ℝ → ℝ) : (cfc f M).trace = ∑ i : n, ↑(f (hM.eigenvalues i))

Finite-dimensional Hermitian CFC trace-sum bridge in the RCLike setting.

theorem HighDimProb.trace_cfc_eq_sum_of_isHermitian {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ} (hM : M.IsHermitian) (f : ℝ → ℝ) : (cfc f M).trace = ∑ i : Fin n, f (hM.eigenvalues i)

Real finite-dimensional specialization of trace_cfc_eq_sum_of_isHermitian_RCLike.

theorem HighDimProb.trace_mul_cfc_eq_sum_conj_diag_of_isHermitian_RCLike {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [RCLike K] {M B : Matrix n n K} (hM : M.IsHermitian) (f : ℝ → ℝ) : (B * cfc f M).trace = ∑ i : n, (star ↑hM.eigenvectorUnitary * B * ↑hM.eigenvectorUnitary) i i * ↑(f (hM.eigenvalues i))

Weighted finite-dimensional Hermitian CFC trace-sum bridge in the RCLike setting. The weights are the diagonal entries of B in the eigenbasis of M.

theorem HighDimProb.trace_mul_cfc_eq_sum_conj_diag_of_isHermitian {n : ℕ} {M B : Matrix (Fin n) (Fin n) ℝ} (hM : M.IsHermitian) (f : ℝ → ℝ) : (B * cfc f M).trace = ∑ i : Fin n, (star ↑hM.eigenvectorUnitary * B * ↑hM.eigenvectorUnitary) i i * f (hM.eigenvalues i)

Real weighted specialization of trace_mul_cfc_eq_sum_conj_diag_of_isHermitian_RCLike.

theorem HighDimProb.trace_inv_add_const_eq_sum_inv_of_isHermitian_of_strictlyPositive {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) (s : ℝ) (hs : 0 ≤ s) : (A + SMul.smul s 1)⁻¹.trace = ∑ i : Fin n, (hA.eigenvalues i + s)⁻¹

Trace of the inverse of a strictly positive Hermitian matrix after an identity shift as a finite sum of shifted scalar inverses.

noncomputable def HighDimProb.traceMulResolventAffineLine {n : ℕ} (A B C : Matrix (Fin n) (Fin n) ℝ) (t : ℝ) : ℝ

Scalar trace-resolvent integrand along an affine matrix line.

noncomputable def HighDimProb.traceMulResolventCutoff {n : ℕ} (A B C : Matrix (Fin n) (Fin n) ℝ) (T t : ℝ) : ℝ

Finite-cutoff trace-resolvent prototype for the log-resolvent route.

noncomputable def HighDimProb.traceMulResolventKernelCutoff {n : ℕ} (A B C : Matrix (Fin n) (Fin n) ℝ) (T : ℝ) : ℝ

Fixed-cutoff trace-resolvent kernel integral over identity shifts.

theorem HighDimProb.integral_inv_add_eq_log_div_of_pos {x T : ℝ} (hx : 0 < x) (hT : 0 ≤ T) : ∫ (s : ℝ) in 0..T, (x + s)⁻¹ = Real.log ((x + T) / x)

Scalar finite-cutoff resolvent integral as a log ratio.

theorem HighDimProb.cfc_log_add_const_eq_of_isHermitian {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (t : ℝ) : cfc (fun (x : ℝ) => Real.log (x + t)) A = cfc Real.log (A + SMul.smul t 1)

Shift the scalar Real.log inside cfc along an affine identity translate.

theorem HighDimProb.trace_cfcLog_add_const_eq_sum_of_isHermitian {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (t : ℝ) : (cfc Real.log (A + SMul.smul t 1)).trace = ∑ i : Fin n, Real.log (hA.eigenvalues i + t)

Trace of the shifted matrix log as the sum of shifted scalar logs.

theorem HighDimProb.trace_cfcLog_add_const_sub_trace_cfcLog_eq_sum_log_sub_of_isHermitian {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (t : ℝ) : (cfc Real.log (A + SMul.smul t 1)).trace - (cfc Real.log A).trace = ∑ i : Fin n, (Real.log (hA.eigenvalues i + t) - Real.log (hA.eigenvalues i))

Trace difference between the shifted matrix log and the base matrix log.

theorem HighDimProb.traceMulResolventCutoff_one_zero_eq_sum_log_sub_of_isHermitian_of_strictlyPositive {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A 1 0 T 0 = ∑ i : Fin n, (Real.log (hA.eigenvalues i + T) - Real.log (hA.eigenvalues i))

Identity-weight finite-cutoff resolvent specialization as a finite sum of scalar log differences.

theorem HighDimProb.traceMulResolventCutoff_one_zero_eq_trace_cfcLog_sub_of_isHermitian_of_strictlyPositive {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A 1 0 T 0 = (cfc Real.log (A + SMul.smul T 1)).trace - (cfc Real.log A).trace

Identity-weight finite-cutoff resolvent specialization as the corresponding trace-CFC.log difference.

theorem HighDimProb.trace_mul_inv_add_const_eq_sum_weighted_inv_of_isHermitian_of_strictlyPositive {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) (s : ℝ) (hs : 0 ≤ s) : (B * (A + SMul.smul s 1)⁻¹).trace = ∑ i : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) i i * (hA.eigenvalues i + s)⁻¹

Weighted trace of the inverse of a strictly positive Hermitian matrix after an identity shift as a finite eigenbasis sum.

theorem HighDimProb.trace_resolvent_kernel_eq_sum_conj_entries_of_isHermitian_of_strictlyPositive {n : ℕ} {A B C : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) (s : ℝ) (hs : 0 ≤ s) : ((A + SMul.smul s 1)⁻¹ * B * (A + SMul.smul s 1)⁻¹ * C).trace = ∑ p : Fin n, ∑ q : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) p q * (star ↑hA.eigenvectorUnitary * C * ↑hA.eigenvectorUnitary) q p * (hA.eigenvalues p + s)⁻¹ * (hA.eigenvalues q + s)⁻¹

Fixed-shift resolvent kernel trace pairing as a conjugated-basis double sum. This is the pointwise kernel formula later integrated by traceMulResolventKernelCutoff_eq_sum_integral_conj_entries_of_isHermitian_of_strictlyPositive.

theorem HighDimProb.traceMulResolventKernelCutoff_eq_sum_integral_conj_entries_of_isHermitian_of_strictlyPositive {n : ℕ} {A B C : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventKernelCutoff A B C T = ∑ p : Fin n, ∑ q : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) p q * (star ↑hA.eigenvectorUnitary * C * ↑hA.eigenvectorUnitary) q p * ∫ (s : ℝ) in 0..T, (hA.eigenvalues p + s)⁻¹ * (hA.eigenvalues q + s)⁻¹

Fixed-cutoff resolvent-kernel integral as a finite double sum in the eigenbasis of the Hermitian base matrix. The coefficient is kept outside the interval integral for downstream resolvent-kernel adapters.

theorem HighDimProb.trace_mul_cfcLog_add_const_sub_trace_mul_cfcLog_eq_sum_weighted_log_sub_of_isHermitian {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (t : ℝ) : (B * cfc Real.log (A + SMul.smul t 1)).trace - (B * cfc Real.log A).trace = ∑ i : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) i i * (Real.log (hA.eigenvalues i + t) - Real.log (hA.eigenvalues i))

Weighted trace difference between the shifted matrix log and the base matrix log, expressed in the eigenbasis of the base Hermitian matrix.

theorem HighDimProb.traceMulResolventCutoff_weight_zero_eq_sum_weighted_log_sub_of_isHermitian_of_strictlyPositive {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A B 0 T 0 = ∑ i : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) i i * (Real.log (hA.eigenvalues i + T) - Real.log (hA.eigenvalues i))

Weighted identity-shift finite-cutoff resolvent specialization as a finite sum of weighted scalar log differences.

theorem HighDimProb.traceMulResolventCutoff_weight_zero_eq_trace_mul_cfcLog_sub_of_isHermitian_of_strictlyPositive {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A B 0 T 0 = (B * cfc Real.log (A + SMul.smul T 1)).trace - (B * cfc Real.log A).trace

Weighted identity-shift finite-cutoff resolvent specialization as the corresponding weighted trace-CFC.log difference.

theorem HighDimProb.LogResolvent.kernelFixedSum {n : ℕ} {A B C : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) (s : ℝ) (hs : 0 ≤ s) : ((A + SMul.smul s 1)⁻¹ * B * (A + SMul.smul s 1)⁻¹ * C).trace = ∑ p : Fin n, ∑ q : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) p q * (star ↑hA.eigenvectorUnitary * C * ↑hA.eigenvectorUnitary) q p * (hA.eigenvalues p + s)⁻¹ * (hA.eigenvalues q + s)⁻¹

Short alias for the fixed-shift resolvent-kernel conjugated-basis double-sum formula.

theorem HighDimProb.LogResolvent.kernelCutoffSum {n : ℕ} {A B C : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventKernelCutoff A B C T = ∑ p : Fin n, ∑ q : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) p q * (star ↑hA.eigenvectorUnitary * C * ↑hA.eigenvectorUnitary) q p * ∫ (s : ℝ) in 0..T, (hA.eigenvalues p + s)⁻¹ * (hA.eigenvalues q + s)⁻¹

Short alias for the fixed-cutoff resolvent-kernel double-sum formula.

theorem HighDimProb.LogResolvent.shiftedInvTraceSum {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) (s : ℝ) (hs : 0 ≤ s) : (A + SMul.smul s 1)⁻¹.trace = ∑ i : Fin n, (hA.eigenvalues i + s)⁻¹

Trace of a shifted inverse as a finite eigenvalue sum.

theorem HighDimProb.LogResolvent.identityCutoffSum {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A 1 0 T 0 = ∑ i : Fin n, (Real.log (hA.eigenvalues i + T) - Real.log (hA.eigenvalues i))

Identity-weight finite cutoff as a finite sum of scalar log differences.

theorem HighDimProb.LogResolvent.weightedCutoffSum {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A B 0 T 0 = ∑ i : Fin n, (star ↑hA.eigenvectorUnitary * B * ↑hA.eigenvectorUnitary) i i * (Real.log (hA.eigenvalues i + T) - Real.log (hA.eigenvalues i))

Weighted finite cutoff as a finite sum of scalar log differences in the base eigenbasis.

theorem HighDimProb.LogResolvent.identityCutoffTraceLogSub {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A 1 0 T 0 = (cfc Real.log (A + SMul.smul T 1)).trace - (cfc Real.log A).trace

Identity-weight finite cutoff as the corresponding trace-CFC.log difference.

theorem HighDimProb.LogResolvent.weightedCutoffTraceLogSub {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : traceMulResolventCutoff A B 0 T 0 = (B * cfc Real.log (A + SMul.smul T 1)).trace - (B * cfc Real.log A).trace

Weighted finite cutoff as the corresponding trace-CFC.log difference.

theorem HighDimProb.LogResolvent.weightedTraceLogEqShiftSubCutoff {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) {T : ℝ} (hT : 0 ≤ T) : (B * cfc Real.log A).trace = (B * cfc Real.log (A + SMul.smul T 1)).trace - traceMulResolventCutoff A B 0 T 0

Weighted fixed-cutoff trace-log representation, solved for the base trace-log term. This keeps the shifted-log cutoff remainder visible; it is not an improper-integral representation or cutoff-removal theorem.

theorem HighDimProb.LogResolvent.weightedShiftTraceLogSubScalarLog_tendsto_zero {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) : Filter.Tendsto (fun (T : ℝ) => (B * cfc Real.log (A + SMul.smul T 1)).trace - B.trace * Real.log T) Filter.atTop (nhds 0)

After subtracting the universal scalar divergence trace B * log T, the shifted weighted trace-log remainder tends to zero. This is a renormalized asymptotic, not a cutoff-removal theorem.

theorem HighDimProb.LogResolvent.weightedCutoffSubScalarLog_tendsto_negTraceLog {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) : Filter.Tendsto (fun (T : ℝ) => traceMulResolventCutoff A B 0 T 0 - B.trace * Real.log T) Filter.atTop (nhds (-(B * cfc Real.log A).trace))

Renormalized cutoff removal for the weighted identity-shift resolvent package. The cutoff integral still needs the scalar counterterm trace B * log T; this is not a plain improper-integral representation.

theorem HighDimProb.LogResolvent.weightedShiftRemainderTendstoZero {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) : Filter.Tendsto (fun (T : ℝ) => (B * cfc Real.log (A + SMul.smul T 1)).trace - B.trace * Real.log T) Filter.atTop (nhds 0)

Short alias for the renormalized shifted-log remainder limit.

theorem HighDimProb.LogResolvent.weightedCutoffRenormTendstoNegTraceLog {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian) (hPos : IsStrictlyPositive A) : Filter.Tendsto (fun (T : ℝ) => traceMulResolventCutoff A B 0 T 0 - B.trace * Real.log T) Filter.atTop (nhds (-(B * cfc Real.log A).trace))

Short alias for renormalized weighted cutoff removal.