Commit 2023-06-13 06:31 9e3895d1

View on Github →

feat: port Analysis.SpecialFunctions.JapaneseBracket (#4924)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

added theorem closedBall_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 Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.lintegral_union_le

added theorem MeasureTheory.set_lintegral_mono'

added theorem MeasureTheory.set_lintegral_mono_ae'