additive haar measure

Stream: general

[Floris van Doorn]

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]

You can fix #4210 ;)

[Yury G. Kudryashov]

docs#expr.apply_replacement_fun

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Floris van Doorn]

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

[Floris van Doorn]

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]

Note that equiv.perm α is "bad"

[Yakov Pechersky]

Also matrix has has_zero and has_one iirc.

[Yury G. Kudryashov]

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