Research proof index

If $d[X_1;X_2] > 0$ then there are $G$-valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$. Phrased in the contrapositive form for convenience of proof.

Chain rule for β(T) : d/dT F(β(T)) = F'(β(T)) * (-1 / (kB * T^2)), within Ioi 0.

We combine limsup_le_of_eventually_monotone_of_tendsto_on_dense and le_liminf_of_eventually_monotone_of_tendsto_on_dense to prove that F · a converges to f a if f is continuous at a.

Tendsto conversion: if F tends to c at atImInfty, then F.resToImagAxis tends to c at atTop.

The analytic kernel: if g : ℝ → ℂ is eventually bounded by C * exp(-b * t) for some b > 0, then t^s * g(t) → 0 as t → ∞ for any real power s. This follows from the fact that t^s * exp(-b * t) → 0 (mathlib's tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero) combined with the big-O transfer lemma.

Truncated contour shift through a simple pole. The left vertical side stays as the symmetric truncation; only the right vertical side is required to be Bochner integrable.