## Stream: general

### Topic: additive haar measure

#### Floris van Doorn (Jan 07 2021 at 22:42):

The Haar measure is currently only defined for multiplicative groups. I tried using the @[to_additive] attribute to also transfer it to additive groups (which is useful to e.g. define the Lebesgue measure using Haar measure), but I have problems.

• Currently, the naming doesn't have mul or anything in it (and I'd like to keep it that way), so I have to write @[to_additive add_haar_measure] or something. This is a little annoying, but something I can definitely live with.
• More importantly, many of my lemmas use multiplication that I don't want to transfer to addition. Usually this is in the form of multiplication on ennreal, which should still be multiplication in the additive version of the theorem. One way around it is to state the theorem for additive groups, and then add the attribute afterwards:
lemma lintegral_eq_zero_of_is_mul_left_invariant [group G] [topological_group G] (hμ : regular μ)
(h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {f : G → ennreal} (hf : continuous f) :
∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=
begin
[long proof involving multiplication on ennreal]
end

lemma lintegral_eq_zero_of_is_add_left_invariant [add_group G] [topological_add_group G] (hμ : regular μ)
(h2μ : is_add_left_invariant μ) (h3μ : μ ≠ 0) {f : G → ennreal} (hf : continuous f) :
∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=
@lintegral_eq_zero_of_is_mul_left_invariant (multiplicative G) _inst_1 _inst_2 _inst_3
μ _ _ hμ h2μ h3μ f hf

attribute [to_additive] lintegral_eq_zero_of_is_mul_left_invariant


This is fine if it happens once or twice, but in the Haar measure file, I expect this to happen 10-100 times. And note that @[to_additive] is not helping me at all in the above example.

Is there a trick I'm missing?

#### Yury G. Kudryashov (Jan 07 2021 at 23:30):

You can fix #4210 ;)

#### Yury G. Kudryashov (Jan 07 2021 at 23:32):

docs#expr.apply_replacement_fun

#### Yury G. Kudryashov (Jan 07 2021 at 23:32):

A possible heuristic is to skip subexpressions of the form @anyfunction (t : Type*) where t is one of the "bad" types.

#### Yury G. Kudryashov (Jan 07 2021 at 23:33):

I think, all non-variable types should be considered "bad"

#### Floris van Doorn (Jan 07 2021 at 23:44):

Thanks for the link to that issue. Yeah, something like that would be helpful.

#### Floris van Doorn (Jan 07 2021 at 23:45):

Yury G. Kudryashov said:

I think, all non-variable types should be considered "bad"

I just posted a comment that confers something similar: all fixed types (i.e. something that is expr.const) should be "bad". However, something like prod G H is probably not bad.

#### Yury G. Kudryashov (Jan 08 2021 at 00:27):

Note that equiv.perm α is "bad"

#### Yakov Pechersky (Jan 08 2021 at 00:30):

Also matrix has has_zero and has_one iirc.

#### Yury G. Kudryashov (Jan 08 2021 at 00:31):

If you ban constant types, this would be better than the current situation.

Last updated: May 15 2021 at 23:13 UTC