Generalising docs#MeasureTheory.integral_smul

Stream: mathlib4

[Yaël Dillies]

I am trying to refactor the definition of discrete convolution I have in APAP to be an abbrev on top of docs#MeasureTheory.convolution. Every lemma is its own battle.

[Yaël Dillies]

Currently I am trying to generalise LeanAPAP#smul_conv, which states

lemma smul_conv {G H R : Type*} [DecidableEq G] [AddCommGroup G] [Fintype G]
    [CommSemiring R] [DistribSMul H R] [IsScalarTower H R R] (c : H) (f g : G → R) :
    c • f ∗ g = c • (f ∗ g)

where ∗ is the discrete convolution as defined in APAP

[Yaël Dillies]

The corresponding lemma for MeasureTheory.convolution is docs#MeasureTheory.smul_convolution, but it only works for y a scalar from the same scalar field of the linear maps, but really it should work for scalars in any subring of that scalar field

[Yaël Dillies]

Tracing it back, docs#MeasureTheory.integral_smul and its preliminary lemmas already aren't properly generalised. Do people have an idea of how hard it would be to generalise the scalars appearing in all those lemmas?

[Yaël Dillies]

cc @Floris van Doorn since I suspect similar concerns might be coming up in Carleson

[David Loeffler]

I'm confused, what do you think the definition of docs#MeasureTheory.integral_smul should be?

[Eric Wieser]

It would be nice if it supported smultiplication by normed rings instead of only fields

[Yaël Dillies]

... or even semirings, eg for n : ℕ we really do want to know the fact that ∫ x, n • f x ∂μ = n • ∫ x, f x ∂μ

[Eric Wieser]

I think for semirings you might be out of luck because we don't have NormedAddCommMonoid

[Yaël Dillies]

I am still hoping... :smile:

[Eric Wieser]

I would suggest focusing on just the noncommutativity for now, and see what you get for free as a result

[Eric Wieser]

I think I looked at this in the past, when I tried to generalize docs#integral_mul_left to quaternions

[Yaël Dillies]

Oh I wasn't hoping for noncommutativity, but that's an interesting thought. All I want is ℕ and ℤ

[Eric Wieser]

Oh, I'm thinking of docs#integral_mul_const and !3#19073

[Floris van Doorn]

Eric Wieser said:

I think for semirings you might be out of luck because we don't have NormedAddCommMonoid

ENormedAddCommMonoid (which is slightly weaker since it also includes ENNReal) coming in #21422. Maybe that can be used for this.

I don't really use scalar subrings of the reals in Carleson. But these generalizations are useful.

[Eric Wieser]

Yury and I have discussed NormedAddCommMonoid in the past, but I think we decided that generalizing a bunch of results to TVS first makes such a future migration easier

[Eric Wieser]

My memory of the titular generalization is that you run into trouble with junk values

[Eric Wieser]

If your f : ℝ → ℝ × ℝ is integrable in the first component but not the second (and therefore as a whole not integrable), then an action that projects out one component violates the theorem you want

[Eric Wieser]

You can probably make it work by requiring IsUnit c ∨ c = 0 but that's pretty ugly

[Eric Wieser]

Or by requiring integrability, since docs#MeasureTheory.Integrable.smul is already at the right generality