Mathlib.Analysis.Special­Functions

SpecialFunctions — Mathlib-shaped helpers for real-power convergence, power integrals, and Jacobi polynomials.

Jacobi 15 core · 23 supporting · 9 submodules This module collects reusable real-analysis infrastructure for normalized shifted Jacobi polynomials: endpoint control, Rodrigues identities, repeated integration by parts, singular-endpoint limits, exact weighted moment Pow 1 core · 0 supporting · 1 submodule For a nonnegative real-valued function f and an exponent s > 0, min(1, f^s) tends to zero along a filter if and only if f tends to zero (tendsto_min_one_rpow_zero_iff).
Power­Integral 1 core · 2 supporting This module evaluates the deterministic interval integrals that appear after the polynomial-tail layer-cake reduction. ★ integral_rpow_neg_Ioc

Power-law interval integrals

This module evaluates the deterministic interval integrals that appear after the polynomial-tail layer-cake reduction. The helper zero_notMem_uIcc supplies the positivity side condition needed by intervalIntegral on a window 0 < a <= b.

The two public evaluations are integral_rpow_neg_Ioc, for the non-logarithmic case kappa != 1, and integral_inv_neg_Ioc, for the boundary case kappa = 1. Together they convert the threshold integral over (t0^(-1), lam^(-1)] into the lam^(kappa - 1) / log (1 / lam) alternatives used by the J and I moment bounds.

theorem integral_rpow_neg_Ioc reviewed
Causalean.Mathlib.Analysis.PowerIntegral

Power integral, κ ≠ 1. If the exponent κ is not equal to 1, a is positive, and a is at most b, then the interval integral of t ↦ t^{-κ} over (a, b] equals (b^{1-κ} − a^{1-κ})/(1−κ).

Formal statement
hypotheses
κ :
ℝ
shared
hκ :
κ ≠ 1
a b :
ℝ
ha :
0 < a
hab :
a ≤ b
conclusion
∫ t in Ioc a b, t ^ (-κ) = (b ^ (1 - κ) - a ^ (1 - κ)) / (1 - κ)
Proof (Lean source)
theorem integral_rpow_neg_Ioc (hκ : κ ≠ 1) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ t in Ioc a b, t ^ (-κ) = (b ^ (1 - κ) - a ^ (1 - κ)) / (1 - κ) := by rw [← intervalIntegral.integral_of_le hab, integral_rpow (inr ⟨fun h => hκ (neg_inj.mp h), zero_notMem_uIcc ha hab⟩), show (-κ + 1 : ℝ) = 1 - κ from by ring]
Causalean.Mathlib.Analysis.PowerIntegral.integral_rpow_neg_Ioc · Causalean/Mathlib/Analysis/SpecialFunctions/PowerIntegral.lean:48
2 supporting declarations (lemmas, instances)
  • zero_notMem_uIcc theorem — 0 ∉ [[a,b]] when 0 < a ≤ b.
    hypotheses
    a b :
    ℝ
    ha :
    0 < a
    hab :
    a ≤ b
    conclusion
    (0 : ℝ) ∉ uIcc a b
    Proof (Lean source)
    theorem zero_notMem_uIcc {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : (0 : ℝ) ∉ uIcc a b := by rw [Set.uIcc_of_le hab, Set.mem_Icc] exact fun h => absurd h.1 (not_le.mpr ha)
    Causalean.Mathlib.Analysis.PowerIntegral.zero_notMem_uIcc · Causalean/Mathlib/Analysis/SpecialFunctions/PowerIntegral.lean:42
  • integral_inv_neg_Ioc theorem — Power integral, κ = 1. ∫ t in (a,b], t^{-1} = log b − log a.
    hypotheses
    a b :
    ℝ
    ha :
    0 < a
    hab :
    a ≤ b
    conclusion
    ∫ t in Ioc a b, t ^ (-(1 : ℝ)) = log b - log a
    Proof (Lean source)
    theorem integral_inv_neg_Ioc {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ t in Ioc a b, t ^ (-(1 : ℝ)) = log b - log a := by have hcongr : EqOn (fun t : ℝ => t ^ (-(1 : ℝ))) (fun t => t⁻¹) (Ioc a b) := fun t _ => by simp [Real.rpow_neg_one] rw [setIntegral_congr_fun measurableSet_Ioc hcongr, ← intervalIntegral.integral_of_le hab, integral_inv (zero_notMem_uIcc ha hab), Real.log_div (ne_of_gt (lt_of_lt_of_le ha hab)) (ne_of_gt ha)]
    Causalean.Mathlib.Analysis.PowerIntegral.integral_inv_neg_Ioc · Causalean/Mathlib/Analysis/SpecialFunctions/PowerIntegral.lean:57