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 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersSpace.integrableOn_norm_rpow_ball_compl_iff
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on {x : Space d | 0 < a ≤ ‖x‖} iff d + p < 0.
Source project: Physlib
Person-level attribution pending.
Space.integrableOn_norm_rpow_ball_iff
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on {x : Space d | 0 ≤ ‖x‖ < b} iff 0 < d + p.
Source project: Physlib
Person-level attribution pending.
Space.integrableOn_norm_rpow_iff_of_isBounded_nhds
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on a bounded neighborhood of the origin iff 0 < d + p.
Source project: Physlib
Person-level attribution pending.
Space.integrableOn_norm_rpow_of_isBounded_compl_nhds
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on a bounded subset with the origin in its exterior.
Source project: Physlib
Person-level attribution pending.
Space.integrableOn_norm_rpow_shell
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on the shell {x : Space d | 0 < a ≤ ‖x‖ ∧ ‖x‖ < b}.
Source project: Physlib
Person-level attribution pending.