mathlib

c2d9927e - feat(analysis/special_functions): the japanese bracket (#16491)

feat(analysis/special_functions): the japanese bracket (#16491) This PR defines and proves basic properties of the japanese bracket, in particular we prove the integrability criterion for negative powers.