Multiplication distributes across integrals

Stream: Is there code for X?

[Eric Wieser]

I was sad to find I can't prove $\int_0^1 a f(t) dt = a \int_0^1 f(t) dt$ for $a : \mathbb{H}$.

import measure_theory.integral.fund_thm_calculus
import analysis.quaternion

open_locale quaternion

example (a : ℍ[ℝ]) (f : ℝ → ℍ[ℝ]) : ∫ t : ℝ in 0..1, a * f t = a * ∫ t : ℝ in 0..1, f t :=
interval_integral.integral_const_mul q f  -- fails, needs is_R_or_C ℍ[ℝ]

Is there some mathematical technicality for why this is the case?

[Kevin Buzzard]

I don't think the problem is a mathematical one.

[Anatole Dedecker]

Yes this should be fine this multiplication by a is \R-linear (and continuous)

[Kevin Buzzard]

Integral basically satisfies the same theorems as finset.sum because it's a limit of such things

[Eric Wieser]

And there's not some stupid reason that it's false if f isn't integrable?

[Kevin Buzzard]

Oh I didn't think about that.

[Anatole Dedecker]

I'm checking that

[Ruben Van de Velde]

Can af be integrable when f isn't?

[Kevin Buzzard]

If a=0 then yes

[Kevin Buzzard]

but multiplication by nonzero a will preserve integrability (or reflect it or whatever is needed -- it will be an iff)

[Eric Wieser]

I suspect a lot of the problem here is that our usual approach of "prove the smul result then derive the mul result" falls apart in normed spaces, because there we're not allowed to smul by anything that isn't a field

[Kevin Buzzard]

oh-oh...

[Anatole Dedecker]

The two lemmas to check are docs#weighted_smul_smul and docs#measure_theory.set_to_fun_smul

[Kevin Buzzard]

Normed spaces for division rings coming up :-/

[Eric Wieser]

That's not enough for me, I need them for rings...

[Eric Wieser]

Or at least, I want the result above for (say) 2x2 matrices too

[Eric Wieser]

Anatole Dedecker said:

Yes this should be fine this multiplication by a is \R-linear (and continuous)

This is docs#continuous_linear_map.interval_integral_comp_comm, right?

[Kevin Buzzard]

So are you telling me we can't do Banach modules (i.e. complete normed modules) over Banach rings (i.e. complete normed rings)? I once wrote a paper about those things (all p-adic of course)

[Anatole Dedecker]

Eric Wieser said:

Anatole Dedecker said:

Yes this should be fine this multiplication by a is \R-linear (and continuous)

This is docs#continuous_linear_map.interval_integral_comp_comm, right?

Yes. Of course this will require integrability

[Anatole Dedecker]

And the map should be docs#continuous_linear_map.mul

[Kevin Buzzard]

Formalising section 2 of that paper of mine is on my todo list. Are there problems with mathlib's set-up?

[Anatole Dedecker]

Yes. I think this has been discussed a few times before. Changing the definition should be straightforward, and then it's the kind of slow transition of everything that we know well, so I wouldn't worry too much about it. But right now you'll definitely have some troubles.

[Anatole Dedecker]

For example the open mapping theorem will probably need to be adapted.

[Kevin Buzzard]

Eric Wieser said:

Or at least, I want the result above for (say) 2x2 matrices too

For 2x2 matrices it's really not true, because they're not a domain, so choose nonzero a,b with a*b=0 (e.g. a=b=[0,0;1,0]) and f0 non-integrable from [0,1] to R, and then define f=b*f0. That was why I suggested division ring. Of course you can just stick to integrable f like we do in actual maths and then you're fine.

[Kevin Buzzard]

Anatole Dedecker said:

For example the open mapping theorem will probably need to be adapted.

See Prop 2.1(a) of my paper :-)

[Anatole Dedecker]

Yes I meant that you won't be able to use docs#continuous_linear_map.is_open directly (I haven't actually checked the proof, it may be completely fine to generalize)

[Anatole Dedecker]

Sorry I read A-modules instead of K-modules, so you won't actually have any problem.

[Anatole Dedecker]

I was surprised by the claim that Bourbaki proves this for normed modules, and for a good reason since they don't and you didn't claim that :sweat_smile:

[Eric Wieser]

#19052 makes some slight progress here and at least lets us claim that $af(x)$ is integrable when $f(x)$ is

[Eric Wieser]

Kevin Buzzard said:

For 2x2 matrices it's really not true, because they're not a domain, so choose nonzero a,b with a*b=0 (e.g. a=b=[0,0;1,0]) and f0 non-integrable from [0,1] to R, and then define f=b*f0. That was why I suggested division ring. Of course you can just stick to integrable f like we do in actual maths and then you're fine.

I'm fine if I have is_unit a, right?

[Kevin Buzzard]

Anatole Dedecker said:

I was surprised by the claim that Bourbaki proves this for normed modules, and for a good reason since they don't and you didn't claim that :sweat_smile:

The result for modules is Theorem 6.16 of https://arxiv.org/abs/1910.05934 (the proof is omitted but Wedhorn got an MSc student to write it up)

[Eric Wieser]

I think the quickest way out of this mess is a has_norm_smul_le typeclass

[Eric Wieser]

Because then we can write [mul_action U A] [has_norm_smul_le U A] for U = units A

[Anatole Dedecker]

Kevin Buzzard said:

Anatole Dedecker said:

I was surprised by the claim that Bourbaki proves this for normed modules, and for a good reason since they don't and you didn't claim that :sweat_smile:

The result for modules is Theorem 6.16 of https://arxiv.org/abs/1910.05934 (the proof is omitted but Wedhorn got an MSc student to write it up)

This version is really close to Bourbaki’s version because the sequence of units tending to zero is really what we need non-discreteness for. So the only missing step is to get it for metrizable topological vector spaces instead of normed spaces. But that should be relatively easy too.

[Kevin Buzzard]

Yes, "exists a topologically nilpotent unit" is an important technical assumption in the nonarchimedean theory -- such rings are called Tate rings.

[Jireh Loreaux]

I will certainly need normed space generalized when I tackle Hilbert modules (here the scalar ring is an arbitrary C*-algebra).

[Eric Wieser]

Are you going to want non-unital algebras too?

[Jireh Loreaux]

Well, yes (I did say "arbitrary" after all ;-)), but I think the solution to that problem is just to consider them as modules over the C*-unitization.

[Jireh Loreaux]

I think there is no loss by doing that. However, I was discussing ideals in non-unital rings with @Oliver Nash privately a while back, and I think we concluded that we need non-unital versions of scalar actions in general.

[Eric Wieser]

Eric Wieser said:

I suspect a lot of the problem here is that our usual approach of "prove the smul result then derive the mul result" falls apart in normed spaces, because there we're not allowed to smul by anything that isn't a field

Because for non-unital rings this strategy also fails, as there without a unit a monoid/ring isn't a mul_action/semiring over itself...

[Eric Wieser]

Eric Wieser said:

I think the quickest way out of this mess is a has_norm_smul_le typeclass

Hey, this already exists, its docs#has_bounded_smul!

[Eric Wieser]

#19053 generalized norm_smul_le and norm_smul to work over rings and division rings respectively

[Eric Wieser]

This now seems to pass CI!

[Eric Wieser]

#19073 is the next step towards proving this

[Eric Wieser]

Unfortunately that PR hit a dead end; I can get the results I want for Lp.simple_func, but the final bochner integral resists the generalization

[Eric Wieser]

I think it still has useful results and at least part of it is worth merging; but I don't think I can prove what I originally wanted before the port catches up

[Anatole Dedecker]

Sorry, could you explain again what you were trying to prove ? This thread is a bit of a mess so I’m not sure I understand the final goal anymore 😅

[Eric Wieser]

Let's say

import measure_theory.integral.fund_thm_calculus
import analysis.quaternion

variables {A : Type} [normed_ring A] [normed_algebra ℝ A]
example (a : A) (h : is_unit A) (f : ℝ → A) : ∫ t : ℝ in 0..1, a * f t = a * ∫ t : ℝ in 0..1, f t :=
interval_integral.integral_const_mul q f  -- fails, needs is_R_or_C A

[Sebastien Gouezel]

Isn't what you want a particular case of docs#continuous_linear_map.integral_comp_comm ? (Or the version for linear equivs)

[Sebastien Gouezel]

(docs#continuous_linear_equiv.integral_comp_comm)

[Eric Wieser]

Aha, you're right! I was looking for a way to not need the integrability hypothesis, and indeed the equiv solves that