therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.32.0

Holder van der corput

holder_van_der_corput

Plain-language statement

If φ\varphi is supported in the ball B(z,R)B(z,R), then the oscillatory integral with phase difference f−gf-g satisfies

∥∫ei(f(x)−g(x))φ(x) dx∥≤C(a) μ(B(z,R)) ∥φ∥Hol,τ;B(z,2R) (1+dz,R(f,g))−1/(2a2+a3).\left\lVert\int e^{i(f(x)-g(x))}\varphi(x)\,dx\right\rVert \le C(a)\,\mu(B(z,R))\,\lVert\varphi\rVert_{\mathrm{Hol},\tau;B(z,2R)}\,(1+d_{z,R}(f,g))^{-1/(2a^2+a^3)}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record