Zulip Chat Archive

Stream: general

Topic: additive haar measure


view this post on Zulip 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] ( : 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] ( : 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
  μ _ _  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?

view this post on Zulip Yury G. Kudryashov (Jan 07 2021 at 23:30):

You can fix #4210 ;)

view this post on Zulip Yury G. Kudryashov (Jan 07 2021 at 23:32):

docs#expr.apply_replacement_fun

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jan 07 2021 at 23:33):

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

view this post on Zulip Floris van Doorn (Jan 07 2021 at 23:44):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jan 08 2021 at 00:27):

Note that equiv.perm α is "bad"

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 00:30):

Also matrix has has_zero and has_one iirc.

view this post on Zulip 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