DomMulAct without AddCommGroup?

Stream: mathlib4

[Björn Wehlin]

I'm trying to express a notion of stationarity of (measure-theoretic) kernels under certain group actions. The setup is as follows.

Let Ω E be measurable spaces, and P : Measure Ω. Let G be a group acting on E, and let κ : Kernel Ω E. If r_g is a map taking a measure μ(-) to μ(g • -), stationarity should mean that

$$\kappa_* \mathbb{P} = (\kappa \circ r_g^{-1})_* \mathbb{P}$$

i.e., that the distribution does not change if we perturb E via the action by G.

This is what I have so far:

import Mathlib

noncomputable section

open MeasureTheory
open ProbabilityTheory

variable {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E] [AddCommGroup E]
variable {P : Measure Ω} [IsProbabilityMeasure P]

variable {G : Type*} [Group G] [DistribMulAction G E] [MeasurableConstSMul G E]
variable {κ : Kernel Ω E}

def is_stationary : Prop := ∀ g : G, P.map ((DomMulAct.mk g) • (⇑κ)) = P.map κ

However, I'd like to relax the requirements on E and G slightly, so that E is not an AddCommGroup and that instead of DistribMulAction G E, we have just MulAction G E.

After this change, I get an error failed to synthesize HSMul Gᵈᵐᵃ (Ω → Measure E) ?m.7822. Is there any way around this?

Changed example for reference:

import Mathlib

noncomputable section

open MeasureTheory
open ProbabilityTheory

variable {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
variable {P : Measure Ω} [IsProbabilityMeasure P]

variable {G : Type*} [Group G] [MulAction G E] [MeasurableConstSMul G E]
variable {κ : Kernel Ω E}

def is_stationary : Prop := ∀ g : G, P.map ((DomMulAct.mk g) • (⇑κ)) = P.map κ

Thanks!

[Björn Wehlin]

(The action should be measurable, of course)

[Björn Wehlin]

Also not 100% confident the property is correctly expressed in the code, so any feedback on that is welcome as well!

[Edward van de Meent]

quick investigation shows that the instance used is synthesized via MeasureTheory.Measure.instDistribMulActionDomMulAct, and we indeed seem to lack the more general instance

[Edward van de Meent]

further investigation suggests that you don't get a weaker result by weakening to MulAction instead of DistribMulAction:

import Mathlib

namespace MeasureTheory.Measure
variable {G A : Type*} [Group G] [AddCommGroup A] [MulAction G A] [MeasurableSpace A]
  [MeasurableConstSMul G A]

noncomputable instance foo : DistribMulAction Gᵈᵐᵃ (Measure A) where
  smul g μ := μ.map (DomMulAct.mk.symm g⁻¹ • ·)
  one_smul μ := show μ.map _ = _ by simp
  mul_smul g g' μ := show μ.map _ = ((μ.map _).map _) by
    rw [map_map]
    · simp [Function.comp_def, mul_smul]
    · exact measurable_const_smul ..
    · exact measurable_const_smul ..
  smul_zero g := show (0 : Measure A).map _ = 0 by simp
  smul_add g μ ν := show (μ + ν).map _ = μ.map _ + ν.map _ by
    rw [Measure.map_add]; exact measurable_const_smul ..

end MeasureTheory.Measure
#check MeasureTheory.Measure.foo

[Edward van de Meent]

(literally the same proofs as what's in mathlib right now)

[Etienne Marion]

I am not sure why it is DomMulAct which is used however, shouldn't it rather be MulOpposite?

[Edward van de Meent]

no?

[Edward van de Meent]

or at least i think not?

[Edward van de Meent]

it's acting on the domain of the measure

[Edward van de Meent]

as opposed to on the codomain, which is ENNReal

[Etienne Marion]

Fair enough I was thinking the domain was rather Set A but I guess it doesn't matter.

[Edward van de Meent]

well it is, but it acts on that pointwise

[Edward van de Meent]

meaning that the actions go as follows:
there is a SMul G E, which allows us to find SMul G (Set E), which allows us to find SMul (DomMulAct G) (Set E -> ENNReal) which restricts to SMul (DomMulAct G) (Measure E) because the smul-action acts pointwise on sets (and is continuous for each element of g)

[Edward van de Meent]

the way this goes in the actual instance does some shortcuts, but this is how i conceptualize it

[Björn Wehlin]

Mathlib builds with

variable {G A : Type*} [Group G] [MulAction G A] [MeasurableSpace A]
  [MeasurableConstSMul G A] {μ ν : Measure A} {g : G}

noncomputable instance : DistribMulAction Gᵈᵐᵃ (Measure A) where

I can submit a pull request to generalize this.

[Edward van de Meent]

indeed, that's what i meant by

(literally the same proofs as what's in mathlib right now)

[Yaël Dillies]

Please do!

[Eric Wieser]

Why did the linter not catch this?

[Eric Wieser]

If we don't even mention the AddGroup structure, wouldn't it be flagged as unused?

[Edward van de Meent]

it is used in the DistribMulAction G A part, which is used to define the smul

[Eric Wieser]

Ah, I was comparing to your already-weakened version above

[Edward van de Meent]

ah i see

[Björn Wehlin]

OK, https://github.com/leanprover-community/mathlib4/pull/25317 has been submitted. Just waiting for CI to go through!

[Edward van de Meent]

yea i didn't test this on an actual mathlib, i tend to do these kinds of investigations just in the sandbox

[Etienne Marion]

Björn Wehlin said:

OK, https://github.com/leanprover-community/mathlib4/pull/25317 has been submitted. Just waiting for CI to go through!

Note that you can simply write #25317 and this will automatically create a link towards the PR.

[Björn Wehlin]

I see, good to know!

Either way, all checks are passing so now we just have to make it through the maintainer queue. Thanks everyone!