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
Project-declaredLean 4.32.0

Third tree pointwise

TileStructure.Forest.third_tree_pointwise

Plain-language statement

For a tree in the forest, a point xx in a boundary cube LL, and a bounded compactly supported function ff, the oscillatory sum of the error fapproxOnCube(f)f-\operatorname{approxOnCube}(f) over the relevant scales is bounded pointwise by a constant times the tree’s boundary operator applied to the cube-wise approximation of f|f|, evaluated at any other point xLx'\in L.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record