Lower bound for psi at small argument

Proved

RybinAI2026.P01.psi_small_lower

by WillR · Oct 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

disproofgeometric-affinityp01

For 0 < t <= 1 the integral of 1/(1+(t-1) s^2) over [0,1] is at least 1, because the integrand is at least 1 there.

Preamble

import Mathlib
import Definitions.Def_rybin2026_p01_matrix_integral
set_option autoImplicit false
open Matrix MeasureTheory Metric RybinAI2026.P01
open scoped BigOperators

Formal statement

namespace RybinAI2026.P01

/-- For `0 < t <= 1` the integrand `1 / (1 - (1-t) s^2)` on `[0,1]` is at least `1`, because
`0 <= s^2 <= 1` forces `1 - (1-t) s^2 <= 1`, and the denominator is positive. -/
theorem psi_small_lower {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) :
    (1 : ℝ) ≤ ∫ s in (0 : ℝ)..1, (1 + (t - 1) * s ^ 2)⁻¹ := by sorry

end RybinAI2026.P01

Source

namespace RybinAI2026.P01 /-- For `0 < t <= 1` the integrand `1 / (1 - (1-t) s^2)` on `[0,1]` is at least `1`, because `0 <= s^2 <= 1` forces `1 - (1-t) s^2 <= 1`, and the denominator is positive. -/ theorem psi_small_lower {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : (1 : ℝ) ≤ ∫ s in (0 : ℝ)..1, (1 + (t - 1) * s ^ 2)⁻¹ := by sorry end RybinAI2026.P01

View graph