Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-17 16:08 f087f43d

View on Github →

feat(measure_theory/integral): integral composed with smul (#17455)

Estimated changes

Modified src/analysis/box_integral/integrability.lean

Modified src/measure_theory/function/locally_integrable.lean

added theorem measure_theory.locally_integrable.indicator

added theorem measure_theory.locally_integrable_const

added theorem measure_theory.locally_integrable_map_homeomorph

Modified src/measure_theory/group/measure.lean

added theorem measure_theory.measure_smul

added theorem measure_theory.measure_univ_of_is_mul_left_invariant

Modified src/measure_theory/integral/integrable_on.lean

modified theorem measure_theory.integrable_on.indicator

added theorem measure_theory.integrable_on.integrable_indicator

Modified src/measure_theory/integral/set_integral.lean

added theorem continuous_linear_equiv.integral_comp_comm

Modified src/measure_theory/measure/haar_lebesgue.lean

added theorem measure_theory.measure.integral_comp_inv_smul

added theorem measure_theory.measure.integral_comp_inv_smul_of_nonneg

added theorem measure_theory.measure.integral_comp_smul

added theorem measure_theory.measure.integral_comp_smul_of_nonneg

Modified src/probability/martingale/borel_cantelli.lean

Modified src/topology/algebra/const_mul_action.lean

Modified src/topology/algebra/group.lean

added theorem exists_disjoint_smul_of_is_compact

added theorem local_is_compact_is_closed_nhds_of_group

Modified src/topology/algebra/monoid.lean

Modified src/topology/instances/ennreal.lean

added theorem ennreal.tendsto_of_real_at_top

Modified src/topology/instances/nnreal.lean

deleted theorem nnreal.tendsto_real_to_nnreal

added theorem tendsto_real_to_nnreal

added theorem tendsto_real_to_nnreal_at_top