smul invariant measure

Stream: maths

[Yury G. Kudryashov]

I suggest to generalize left/right-invariant measures to

@[to_additive]
def is_smul_invariant (M : Type*) {α : Type*} [has_scalar M α] [measurable_space α] (μ : set α → ℝ≥0∞) : Prop :=
∀ (g : M) {A : set α} (h : measurable_set A), μ ((λ h, g • h) ⁻¹' A) = μ A

Then is_mul_left_invariant (μ : measure G) = is_smul_invariant G μ and is_mul_right_invariant (μ : measure G) = is_smul_invariant Gᵒᵖ μ.

[Yury G. Kudryashov]

@Floris van Doorn @Sebastien Gouezel What do you think?

[Yury G. Kudryashov]

Also, I think about replacing def with a class.

[Alex J. Best]

I do this in https://github.com/leanprover-community/mathlib/pull/2819/files but it should probably be an independent PR first, so +1 from me :smile:

[Floris van Doorn]

Yeah, that is probably a good idea.

[Sebastien Gouezel]

Looks good to me.