Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-04 09:53 c2d9927e

View on Github →

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.

Estimated changes

Modified src/analysis/normed/group/basic.lean

added theorem zero_lt_one_add_norm_sq'

Modified src/analysis/normed_space/basic.lean

Created src/analysis/special_functions/japanese_bracket.lean

added theorem closed_ball_rpow_sub_one_eq_empty_aux

added theorem finite_integral_one_add_norm

added theorem finite_integral_rpow_sub_one_pow_aux

added theorem integrable_one_add_norm

added theorem integrable_rpow_neg_one_add_norm_sq

added theorem le_rpow_one_add_norm_iff_norm_le

added theorem one_add_norm_le_sqrt_two_mul_sqrt

added theorem rpow_neg_one_add_norm_sq_le

added theorem sqrt_one_add_norm_sq_le

Modified src/measure_theory/measure/haar_lebesgue.lean

added theorem measure_theory.measure.add_haar_closed_ball_eq_add_haar_ball