mathlib3 documentation

measure_theory.measure.haar.normed_space

Basic properties of Haar measures on real vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The integral of f (R • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

The integral of f (R • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

The integral of f (R⁻¹ • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

The integral of f (R⁻¹ • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

theorem measure_theory.measure.integral_comp_div {F : Type u_2} [normed_add_comm_group F] [normed_space F] [complete_space F] (g : F) (a : ) :
(x : ), g (x / a) = |a| (y : ), g y