# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC