Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-20 23:36 5ac4cd35

View on Github →

feat(analysis/special_functions/non_integrable): examples of non-integrable functions (#10788)

Estimated changes

Modified src/analysis/calculus/fderiv_measurable.lean

added theorem ae_measurable_deriv

Created src/analysis/special_functions/non_integrable.lean

added theorem interval_integrable_inv_iff

added theorem interval_integrable_sub_inv_iff

added theorem not_interval_integrable_of_sub_inv_is_O_punctured

added theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter

added theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured

added theorem not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_within_diff_singleton

Modified src/data/set/intervals/unordered_interval.lean

added theorem set.interval_oc_subset_interval_oc_of_interval_subset_interval

added theorem set.interval_oc_swap

Modified src/measure_theory/integral/interval_integral.lean

added theorem interval_integrable.mono_fun'

added theorem interval_integrable.mono_fun

added theorem interval_integral.abs_integral_eq_abs_integral_interval_oc

added theorem interval_integral.abs_integral_mono_interval

modified theorem interval_integral.norm_integral_eq_norm_integral_Ioc

added theorem interval_integral.norm_integral_min_max

Modified src/order/filter/basic.lean

Modified src/order/filter/interval.lean

added theorem filter.tendsto.interval

Modified src/topology/continuous_on.lean

modified theorem diff_mem_nhds_within_compl

added theorem diff_mem_nhds_within_diff