Commit 2022-11-10 07:06 262dfc94

View on Github →

feat(analysis/convolution): weaken typeclass assumptions (#17452) Remove some finite-dimensionality or propertness assumptions, by noticing that if a compactly supported function is nonzero then the space has to be finite-dimensional.

Estimated changes

Modified src/analysis/convolution.lean

added theorem convolution_neg_of_neg_eq

modified theorem convolution_zero

modified theorem has_compact_support.cont_diff_convolution_left

modified theorem has_compact_support.cont_diff_convolution_right

modified theorem zero_convolution

Modified src/analysis/normed_space/finite_dimension.lean

added theorem has_compact_mul_support.eq_one_or_finite_dimensional

Modified src/measure_theory/group/measure.lean

added theorem measure_theory.eventually_div_right_iff

added theorem measure_theory.eventually_mul_left_iff

added theorem measure_theory.eventually_mul_right_iff

added theorem measure_theory.is_mul_left_invariant_map

Modified src/topology/separation.lean

added theorem continuous.is_open_mul_support