to_additive and smul of measures

Stream: maths

[Sebastien Gouezel]

I have a problem with to_additive, which is trying to additivize docs#measure_theory.measure.coe_smul (smul on measures), which doesn't make sense. And I don't know how to convince it that it shouldn't try (apart of rewriting my proofs separately in the additive and multiplicative setting. Changing the arguments order of coe_smul does not seem to help. @Floris van Doorn , maybe?

MWE:

import measure_theory.group.basic
open_locale ennreal
namespace measure_theory

class is_haar_measure {G : Type*} [group G] [topological_space G] [measurable_space G]
  (μ : measure G) : Prop :=
(compact_lt_top : ∀ (K : set G), is_compact K → μ K < ∞)

class is_add_haar_measure {G : Type*} [add_group G] [topological_space G] [measurable_space G]
  (μ : measure G) : Prop :=
(compact_lt_top : ∀ (K : set G), is_compact K → μ K < ∞)

attribute [to_additive] is_haar_measure

variables {G : Type*}
[group G] [measurable_space G] [topological_space G] (μ : measure G) [is_haar_measure μ]

@[to_additive is_add_haar_measure.smul] -- fails
lemma is_haar_measure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) :
  is_haar_measure (c • μ) :=
{ compact_lt_top := λ K hK, begin
    have A : μ K < ∞ := is_haar_measure.compact_lt_top K hK,
    simp only [lt_top_iff_ne_top, A.ne, ctop, measure.coe_smul, algebra.id.smul_eq_mul,
      with_top.mul_eq_top_iff, ne.def, not_false_iff, pi.smul_apply, and_false, false_and, or_self],
  end }

end measure_theory

[Eric Wieser]

Am I missing something? Are those typeclasses different? Isn't the group argument unused?

[Yury G. Kudryashov]

@Eric Wieser The actual typeclasses have more axioms.

[Floris van Doorn]

This is the same issue that came up in #9032. I'm afraid to_additive needs to be improved for this to work.
to_additive looks at the first argument of a function to see if it contains a constant type (like ennreal), and will not additivize that function if it does.
Unfortunately, for pi.has_scalar the relevant argument is the second argument (and we cannot reorder the arguments). I will try to generalize to_additive so that it looks at a (user-specified) n-th argument.

From the doc:

* Option 1: It additivized a declaration `d` that should remain multiplicative. Solutions:
  * Make sure the first argument of `d` is a type with a multiplicative structure. If not, can you
    reorder the (implicit) arguments of `d` so that the first argument becomes a type with a
    multiplicative structure (and not some indexing type)?
    The reason is that `@[to_additive]` doesn't additivize declarations if their first argument
    contains fixed types like `ℕ` or `ℝ`. See section Heuristics.
    This is not possible if `d` is something like `pi.has_one` or `prod.group`, where the second
    argument (also) has a multiplicative structure.

[Sebastien Gouezel]

Still there is something I don't get. The lemma that creates a problem is measure_theory.measure.coe_smul (which has just rfl as a proof, and no to_additive argument). I tried to reorder its arguments to put (c : ennreal) as the first argument, to tell to_additive to ignore it. But this doesn't change anything.

[Floris van Doorn]

Are you saying that coe_smul is the problem because if you remove that lemma from the proof, it works?
The problem is with pi.has_scalar. As you can see in the error message pi.has_scalar is incorrectly additivized:

type mismatch at application
  @pi.has_vadd (set G) (λ (ᾰ : set G), ℝ≥0∞) ℝ≥0∞
    (λ (i : set G),
       @has_mul.to_has_scalar ℝ≥0∞
         (@distrib.to_has_mul ℝ≥0∞
            (@non_unital_non_assoc_semiring.to_distrib ℝ≥0∞
               (@non_assoc_semiring.to_non_unital_non_assoc_semiring ℝ≥0∞
                  (@semiring.to_non_assoc_semiring ℝ≥0∞
                     (@comm_semiring.to_semiring ℝ≥0∞
                        (@canonically_ordered_comm_semiring.to_comm_semiring ℝ≥0∞
                           ennreal.canonically_ordered_comm_semiring)))))))
term
  λ (i : set G),
    @has_mul.to_has_scalar ℝ≥0∞
      (@distrib.to_has_mul ℝ≥0∞
         (@non_unital_non_assoc_semiring.to_distrib ℝ≥0∞
            (@non_assoc_semiring.to_non_unital_non_assoc_semiring ℝ≥0∞
               (@semiring.to_non_assoc_semiring ℝ≥0∞
                  (@comm_semiring.to_semiring ℝ≥0∞
                     (@canonically_ordered_comm_semiring.to_comm_semiring ℝ≥0∞
                        ennreal.canonically_ordered_comm_semiring))))))
has type
  set G → has_scalar ℝ≥0∞ ℝ≥0∞
but is expected to have type
  Π (i : set G), has_vadd ℝ≥0∞ ((λ (ᾰ : set G), ℝ≥0∞) i)

The reason that coe_smul causes this error, is that the right-hand-side of this equation contains pi.has_scalar.

[Floris van Doorn]

I think/hope this is fixed by #9138 (cc @Alex J. Best)

[Sebastien Gouezel]

Yes, without coe_smul it works. Just changing the proof, replacing the coe_smul with a change step works fine. For instance, in the current Haar file

@[to_additive]
lemma haar_measure_apply {K₀ : positive_compacts G} {s : set G} (hs : measurable_set s) :
  haar_measure K₀ s = (haar_content K₀).outer_measure s / (haar_content K₀).outer_measure K₀.1 :=
begin
  delta haar_measure,
  change (((haar_content K₀).outer_measure) K₀.val)⁻¹ * (haar_content K₀).measure s = _,
  simp only [hs, div_eq_mul_inv, mul_comm, content.measure_apply],
end

fixes the issue of #9032. But changing it back to

@[to_additive]
lemma haar_measure_apply {K₀ : positive_compacts G} {s : set G} (hs : measurable_set s) :
  haar_measure K₀ s = (haar_content K₀).outer_measure s / (haar_content K₀).outer_measure K₀.1 :=
begin
  delta haar_measure,
  rw coe_smul,
  change (((haar_content K₀).outer_measure) K₀.val)⁻¹ * (haar_content K₀).measure s = _,
  simp only [hs, div_eq_mul_inv, mul_comm, content.measure_apply],
end

makes the problem come back. Even when one changes coe_smul to have as first argument an ennreal.

[Floris van Doorn]

The reason is that in those proofs you avoid pi.has_scalar in the proof.

[Sebastien Gouezel]

ok, thanks for the explanation!