Adjoint Carleson adjoint
adjointCarleson_adjoint
Plain-language statement
adjointCarleson is the adjoint of carlesonOn.
Source project: Carleson formalization
Person-level attribution pending.
Source-pinned research
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 130 research declarations. Search 10,000 more complete Mathlib declarations.
130 results
Clear filtersadjointCarleson_adjoint
Plain-language statement
adjointCarleson is the adjoint of carlesonOn.
Source project: Carleson formalization
Person-level attribution pending.
ae_tendsto_zero_of_distribution_le
Plain-language statement
Suppose that, for every error threshold and every measure tolerance , one can choose so that the set where exceeds has measure at most . Then converges to for almost every .
Source project: Carleson formalization
Person-level attribution pending.
antichain_operator
Plain-language statement
For an antichain of pairwise incomparable tiles, and measurable functions and bounded by the indicators of and , the pairing of with the Carleson sum over is controlled by the norms of and and by positive powers of the two tile-density parameters. Concretely, the bound is
Source project: Carleson formalization
Person-level attribution pending.
antichain_operator'
Plain-language statement
For an antichain , a measurable set , and measurable bounded by , the norm of the Carleson sum has the integral estimate
Source project: Carleson formalization
Person-level attribution pending.
Antichain.stack_density
Plain-language statement
Fix a frequency parameter , a level , and a spatial grid cube . Among the auxiliary tiles attached to an antichain whose spatial cube is exactly , the total measure of their active sets inside is at most
Source project: Carleson formalization
Person-level attribution pending.
boundary_exception
Plain-language statement
For a tile , the union of the grid cubes in its level- boundary family has measure at most a constant times the measure of the spatial cube .
Source project: Carleson formalization
Person-level attribution pending.