How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The profile moments of are central binomial coefficients
Statement
For the limit profile of The Logan-Shepp-Vershik-Kerov limit profile , and by the declaration of Shifted character observables and profile moments .
Facts & Assumptions
Given: the even profile and its profile moments , (The Logan-Shepp-Vershik-Kerov limit profile , Shifted character observables and profile moments ).
is even, for , and for it is with (The Logan-Shepp-Vershik-Kerov limit profile ). Hence is even, vanishes outside , and is continuous and piecewise on and , with ; integrating by parts on the two pieces gives, for , (all boundary terms vanish: at because vanishes there, at because ), so (Shifted character observables and profile moments ).
Monotone change of variables: if is a monotone differentiable bijection with integrable derivative and is Riemann integrable on , then (Monotone change of variable for Riemann-integrable functions).
Arcsine: for (Principal inverse sine and inverse cosine), and and have the usual derivatives (The derivatives of sine and cosine are cosine and minus sine).
Integration by parts on a closed interval: if are differentiable on with integrable derivatives then (If are differentiable on with integrable, then ).
Proof
Odd moments vanish: is even and supported in by [F1], so for odd the integrand is odd and its integral over the symmetric interval vanishes; hence for odd by the definition, and by the convention.
Reduction for even moments: fix and put . By [F1] and the integration-by-parts form of the profile moment, The integrand is even (odd factor times the odd function ), so the integral equals .
Substitution : by [F2] applied to the increasing bijection from onto (with and by [F4]), the integral of step 1.2 equals
Integration by parts and Wallis: on put and ; both are differentiable with continuous derivatives and , so [F5] gives because and while . Multiplying by and using [F3], , where the last equality is of [F3].
Conclusion: step 1.1 gives the vanishing for odd (including by convention) and steps 1.2, 2.1, 3.1 give for every .
Depends on
- The Logan-Shepp-Vershik-Kerov limit profile $\Omega$
- Shifted character observables $p_\rho^\#$ and profile moments $\tilde p_k$
- Monotone change of variable for Riemann-integrable functions
- If $u,v$ are differentiable on $[a,b]$ with $u',v'$ integrable, then $\int_a^b u v' = u(b)v(b)-u(a)v(a) - \int_a^b u'v$
- Principal inverse sine and inverse cosine
- The derivatives of sine and cosine are cosine and minus sine
- Wallis integrals satisfy the two-step recurrence, closed forms, and the adjacent-integral squeeze
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
Used by
Dependency tree · two levels
64 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.