Differentiate the defining psi integral

Proved

RybinAI2026.P01.psi_hasDerivAt

by WillR · Sep 29, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysisreal-analysis

For every positive t, the scalar integral psi(t)=integral from 0 to 1 of (1+(t-1)s^2)^(-1) is differentiable, with derivative equal to the integral of the pointwise derivative -s^2(1+(t-1)s^2)^(-2). This is the calculus bridge needed for the diagonal pair-contraction slope argument.

Preamble

import Mathlib

Formal statement

theorem RybinAI2026.P01.psi_hasDerivAt (t : ℝ) (ht : 0 < t) :
    HasDerivAt (fun x : ℝ => ∫ s in (0 : ℝ)..1, (1 + (x - 1) * s ^ 2)⁻¹)
      (∫ s in (0 : ℝ)..1, -(s ^ 2 * (1 + (t - 1) * s ^ 2)⁻¹ ^ 2)) t := by
  sorry

Source

Differentiation under the integral sign for psi in the aligned diagonal proof in artifacts/p01_slack/2026-09-29-no-w-pair.md.

View graph