Normed dual of Schwarz space

Stream: PhysLean

[Kenny Lau]

@Joseph Tooby-Smith I thought it might be a good idea to make this a separate thread. What are the things I should keep in mind?

[Kenny Lau]

For example, the question I would have is, how much stuff do we currently have? and which folder should I put it in?

[Kenny Lau]

maybe I should make a separate folder for it, PhysLean/Mathematics/Schwarz/Basic.lean

[Kenny Lau]

to document more of my thoughts, I had an idea to enlarge the test functions to continuous piecewise differentiable but ultimately thought it's a bad idea.

[Kenny Lau]

I think I'll keep the test function to the Schwarz space, and then I'll make some API to account for the piecewise functions

[Joseph Tooby-Smith]

The only thing currently in PhysLean regarding Schwarz maps is the stuff I was doing last week regarding Quantum mechanics which can be found in the Operators and HilbertSpace folders of this directory.

I would even be tempted to put this in the SpaceAndTime directory in a folder like e.g. SpaceAndTime.Distributions., but I think the mathematics folder is also good.

Here are somethings I would like to see:

• Notation that makes the type of distributions look like a function type e.g. ℝ →d ℂ
• API and notation around derivatives so we can use them like we use derivatives of functions.
• API that makes it as easy as possible to treat functions as distributions. This means: Defining distributions from functions, take the derivative of distributions which are actually functions, proving equality of two distributions which are actually functions, etc.
• Important distributions pre-defined as such, e.g. dirac delta, the Heaviside step functions, the inverse potential $1/r^2$. These should have good API, for example their derivatives etc.

[Kenny Lau]

also another question is, do we want R -> C or R -> R? or R -> R^k?

[Kenny Lau]

it seems like in quantum you would want (R -> C) -> C but in variational calculus you would want (R -> R^2) -> R?

[Kenny Lau]

or i can allow both

[Kenny Lau]

I want to make the decision to only use Type 0 lol

[Kenny Lau]

@Joseph Tooby-Smith do you actually use universes? I see that you type universe v u in the beginning of your files but I don't know if you really use them

[Joseph Tooby-Smith]

So as physicists we are mainly interested in functions from space (or spacetime) to Euclidean space or the product of R’s etc. So if it can be done to cover all these cases I think this would be good - if indeed possible.

[Kenny Lau]

yes but i'm saying in quantum you want C

[Joseph Tooby-Smith]

Regarding universes, nope! I’m not sure of anywhere in physlean where universes come in. If they can be avoided here the better I think

[Joseph Tooby-Smith]

Yeah sorry, Euclidean spaces over the reals or complex numbers and also factors of C and C^2 etc. (Sorry for the bad formatting - on my phone)

[Kenny Lau]

Joseph Tooby-Smith said:

Regarding universes, nope! I’m not sure of anywhere in physlean where universes come in. If they can be avoided here the better I think

https://github.com/search?q=repo%3AHEPLean%2FPhysLean%20universe&type=code

[Kenny Lau]

now i'm thinking you might actually want (R -> R/C^k) -> R/C^k!

[Kenny Lau]

@Joseph Tooby-Smith what should the output be?

[Kenny Lau]

for example, where does dirac delta make sense?

[Kenny Lau]

if i start with a function f:R->R^3 defined by f(t) = (sin(t), cos(t), t), and ask you what is (δ*f)(0)?

[Kenny Lau]

then you would say (0, 1, 0) right

[Joseph Tooby-Smith]

I think the output should be R or C still. In particular a function R->R^k defines a distribution (R->R^k)->R through integration over the inner product

[Kenny Lau]

ok but what about my example?

[Kenny Lau]

oh you take the inner product first

[Joseph Tooby-Smith]

I think (though could be wrong) that you have a direction associated with the delta function

[Kenny Lau]

wiki seems to think that it outputs R^n

[Joseph Tooby-Smith]

Kenny Lau said:

Joseph Tooby-Smith said:

Regarding universes, nope! I’m not sure of anywhere in physlean where universes come in. If they can be avoided here the better I think

https://github.com/search?q=repo%3AHEPLean%2FPhysLean%20universe&type=code

I can’t open this right now (as I’m not signed into GitHub on my phone) but I’m going to guess that those universes can be trivially removed

[Kenny Lau]

but this could just be a different convention

[Joseph Tooby-Smith]

could you share the wiki page?

[Kenny Lau]

https://en.wikipedia.org/wiki/Dirac_delta_function#Generalizations

[Kenny Lau]

image.png

[Kenny Lau]

oh wait, this is different

[Kenny Lau]

this is the dirac delta R^n -> R, sorry for the confusion

[Joseph Tooby-Smith]

Yeah! I think f here is a function from R^k->R

[Joseph Tooby-Smith]

Kenny Lau said:

Joseph Tooby-Smith said:

Regarding universes, nope! I’m not sure of anywhere in physlean where universes come in. If they can be avoided here the better I think

https://github.com/search?q=repo%3AHEPLean%2FPhysLean%20universe&type=code

Back at a computer, and made a PR removing all universes in PhysLean - none were doing anything.

[Kenny Lau]

@Joseph Tooby-Smith I've made a PR to define distributions and dirac delta function. I've provided a custom constructor that a physicist should be able to understand (try it yourself!).

[Kenny Lau]

https://github.com/HEPLean/PhysLean/pull/644

[Kenny Lau]

cc @ZhiKai Pong

[Kenny Lau]

@Joseph Tooby-Smith do you know why the CI is building all the files even though I haven't touched anything?

[Joseph Tooby-Smith]

This always happens for PhysLean - I think it is basically down to the fact we don't have a cache like Mathlib does. I would like to set one up at some point, but am not entirely sure how - and think it relies on server space somewhere.

[Joseph Tooby-Smith]

BTW you can run the linters locally using (which is quicker then relying on GitHub):

lake exe lint_all
./scripts/lint-style.sh

[Kenny Lau]

@Joseph Tooby-Smith i've updated the file

[ZhiKai Pong]

what does docs#SchwartzMap.delta do or is it something else entirely?

[Kenny Lau]

aha, lol

[Kenny Lau]

nice find!

[Kenny Lau]

so one difference is that it doesn't output a scalar

[Kenny Lau]

https://en.wikipedia.org/wiki/Distribution_(mathematics)

[Kenny Lau]

here's an interesting thing

[Kenny Lau]

wiki seems to imply that distributions are actually (U -> R) -> R or (U -> C) -> C

[Kenny Lau]

wiki wants to make the domain high dimensional rather than the target

[Kenny Lau]

what if we just allow (R -> E) -> F because we might need them eventually

[Kenny Lau]

on that note why don't we generalise the R too :rofl:

[Joseph Tooby-Smith]

Yeah I think R really should be generalized, since in general this represents space or spacetime, not necessarily in 1-dimension. I'm still confused why you want to generalize F though?

[Joseph Tooby-Smith]

Maybe my real concern is the following: If you generalize F, I worry that defining e.g. the derivative etc. will become difficult. But maybe it can be done.

[Joseph Tooby-Smith]

Let me add to my list above of things I would like to see:

• A constructor of a distribution based on a function ℝ → ℂ satisfying conditions which can be solved with fun_prop.

[Kenny Lau]

Joseph Tooby-Smith said:

Yeah I think R really should be generalized, since in general this represents space or spacetime, not necessarily in 1-dimension. I'm still confused why you want to generalize F though?

i think you're right, we don't need to generalise F; i just thought we might need to because the dirac delta in the library is S(E,F) ->[L] F

[Kenny Lau]

but if we stick to R/C then we can still define our own dirac by composing it with a linear function

[Joseph Tooby-Smith]

Ok, I'm happy either way, so I am happy for you to make a call on this. I think at some point it will become clear which one is needed anyway :).

[Kenny Lau]

@Joseph Tooby-Smith I think a good enough criterion for f to become a distribution is that int_a^b |f(x)| dx should (exist and) be bounded for every a<b? but this would also mean that your 1/r^2 might not work... how do you make sense of 1/r^2?

[Kenny Lau]

every continuous function should be able to be interpreted as a distribution

[Kenny Lau]

i'll do that in the next PR

[Kenny Lau]

actually i hope you don't mind me asking again, i'm not really familiar with these things; do you have an example where we want the test functions (that's the R->E part) to have high dimensional output value?

[Kenny Lau]

i actually don't understand why S(R, R) ->L R and S(R, C) ->L C aren't enough...

[Kenny Lau]

i thought about the var cal case but actually in that case the test functions are still one dimensional

[Joseph Tooby-Smith]

Kenny Lau said:

Joseph Tooby-Smith I think a good enough criterion for f to become a distribution is that int_a^b |f(x)| dx should (exist and) be bounded for every a<b? but this would also mean that your 1/r^2 might not work... how do you make sense of 1/r^2?

Huh - this is worrying. I want to really make sense of the equation given here:

https://math.stackexchange.com/questions/1335591/divergence-of-vecf-frac-hat-mathrmrr2?noredirect=1&lq=1

I thought, and what people say, is that this is in terms of distributions. This equation comes up in Maxwell's equations for a point particle, and actually gives an example of why S(R, R) ->L R and S(R, C) ->L C aren't enough.

[Joseph Tooby-Smith]

Also the 1/r^2 should be thought of as being in 3d, which may salvage things (r) is the distance from the orgin.

[Kenny Lau]

@Joseph Tooby-Smith Thanks for the example.

1. This is an interesting example indeed. From the proof given in the most upvoted answer, I'll take the definition to be "the limit of the distributions defined by 1/(r^2+a^2) as a->0". If you want a more intrinsic definition maybe principal values will be the answer?
2. The test functions (φ) are actually R^3 -> R, so that's actually not an example I'm looking for. I understand that the first R in my (S(R, R/C) -> R/C) should be generalised, but I'm talking about the first "R/C" in my expression.

[Joseph Tooby-Smith]

c.f. 2, yes, sorry you are right. I am interested in the function $f(\vec r) = \hat{r}/r^2$ before taking the divergence, and I want to interpret this as a distribution, which I think would correspond to $S(R^3, R^3)\to R$.

[Joseph Tooby-Smith]

I want to interpret this as a distribution, because I want to make sense of the divergence of it, and ending up with a Dirac delta function.

[Joseph Tooby-Smith]

If you want a more intrinsic definition maybe principal values will be the answer?

I was thinking that, but I don't think it's actually needed, since I think e.g. the norm of $f(\vec r) = \hat r /r^2$ is locally integrable in $R^3$, namely since the volume measure is $= \sin (\theta) r^2 drd\theta d\phi$, the $r^2$'s cancel out.

[Kenny Lau]

I'm wondering if it's possible to make sense of your f : R^3 -> "R^3" without actually modifying the space of test functions S(R^3, R)

[Joseph Tooby-Smith]

(From the

Joseph Tooby-Smith said:

If you want a more intrinsic definition maybe principal values will be the answer?

I was thinking that, but I don't think it's actually needed, since I think e.g. the norm of $f(\vec r) = \hat r /r^2$ is locally integrable in $R^3$, namely since the volume measure is $= \sin (\theta) r^2 drd\theta d\phi$, the $r^2$'s cancel out.

(From the physics point of view this is actually precisely why the $1/r^2$ appears in electromagnetism)

[Joseph Tooby-Smith]

Kenny Lau said:

I'm wondering if it's possible to make sense of your f : R^3 -> "R^3" without actually modifying the space of test functions S(R^3, R)

I guess the question is how would you treat f : R^3 -> R^3 as a distribution in this sense, what would your integral be?

[Kenny Lau]

from a mathematical point of view there's actually nothing "extra" added on by going from a "scalar field" to a "vector field": the behaviour of (f1, f2, f3) is determined by f1, f2, and f3, i think

[Kenny Lau]

generalising the codomain is quite different from generalising the domain

[Kenny Lau]

i'm actually also a bit confused about the statement that it's integrable because the 1D version 1/x^2 seems to not be integrable? am I missing something here?

[Kenny Lau]

oh the 1d version isn't 1/x^2 it's sgn(x)/x^2 right

[Joseph Tooby-Smith]

Kenny Lau said:

oh the 1d version isn't 1/x^2 it's sgn(x)/x^2 right

The 2d version is $1/r$, and the 1d version is $1$. This is explained (for physicists) here:

https://physics.stackexchange.com/questions/629299/does-the-electric-field-in-1d-exist-in-nature

This has a very bizarre physical consequence: A point particle in 1d produces a constant electric field in all of space. (the same way that in 3d an infinite plane of charges produces a constant electric field).

[Kenny Lau]

sorry, by 1d version i just meant the naive way of just looking at the x-axis

[Kenny Lau]

and then for sgn(x)/x^2 you still need to kinda of "take some limit" -- whether you do it explicitly via sgn(x)/(x^2+a^2), or implicitly by considering "principal value" or taking the complement of (-ε, ε) and letting ε -> 0

[Joseph Tooby-Smith]

I agree that the value along the $x$-axis is sgn(x)/x^2, but I don't see why you are trying to integrate along the x-axis, which is of measure zero in 3d.

[Kenny Lau]

ah I just wanted to do an "easier" version but maybe this is not the right thing to do

[Kenny Lau]

maybe 3d domain is really different from 1d domain

[Joseph Tooby-Smith]

Yeah I think it is - I don't think you can just restrict to a 1d line. (which I agree is rather odd intuitively)

[Kenny Lau]

@Joseph Tooby-Smith btw im now leaning towards making a function f: R^n -> R^k into a distribution by taking test function η: R^n -> R (!) and outputting int η x • f x dx (in R^k!); I thought I would ask for your opinion on this.

[Kenny Lau]

I’m 80% convinced that this is the best approach

[Kenny Lau]

update: 90%

[Joseph Tooby-Smith]

Ok this makes sense, I think it will make it easier to eg define the divergence as well

[Tomas Skrivan]

(deleted)

[Tomas Skrivan]

(deleted)

[Joseph Tooby-Smith]

Concerning showing $1/r^2$ is a distribution in 3d, I think what one may need is the generalization of docs#integral_comp_polarCoord_symm to one dimension higher, or something similar. This is related to @ZhiKai Pong 's (as yet unanswered :() post on spherical coordinates: #Is there code for X? > Spherical coordinates . Maybe it is worth developing such an API.

[Kenny Lau]

I recall we have something like a "spherical haar measure"

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Constructions/HaarToSphere.html#MeasureTheory.Measure.toSphere

[Kenny Lau]

this thing

[Joseph Tooby-Smith]

Ah! Nice! Ok, and there is docs#MeasureTheory.integral_fun_norm_addHaar ! Looks very close to what we would want (just over a compact domain not the whole space).

[Kenny Lau]

just set the function to 0 outside the compact domain

[Joseph Tooby-Smith]

Yep!

[Joseph Tooby-Smith]

Honestly I spent a good hour earlier searching loogle for things like

MeasureTheory.integral, "norm"

so don't know how I missed this, maybe I didn't quite use the right words :).

[Joseph Tooby-Smith]

Some other distributions which appear in physics:

• A generalization of a dirac delta function to a line e.g. for the x-axis $\delta_{Lx}$ such that in 3d

$$\langle \delta_{Lx}, \phi(x, y, z) \rangle = \int \phi(x, 0, 0) dx.$$

Physically this appears when studying e.g. lines of charges, or a the magnetic field around a wire.

• A generalization of a dirac delta function to a plane (and in general any co-dimension n surface, e.g. the surface of a ball).
• The function which takes a value 'a' inside a ball of radius 'r' and is zero outside. Used e.g. in gravity.

[Joseph Tooby-Smith]

Here is the definition of the function $1/r^2$ in 3d as a distribution, I'm sure this could very much be neatened up etc.

Code

import Mathlib.Analysis.Distribution.FourierSchwartz
import Mathlib.MeasureTheory.Constructions.HaarToSphere

open MeasureTheory
noncomputable section
open SchwartzMap NNReal

def invSqMeasure : Measure (EuclideanSpace ℝ (Fin 3)) :=
  volume.withDensity (fun x : EuclideanSpace ℝ (Fin 3) => ENNReal.ofReal (1 / ‖x‖ ^ 2))

instance : Measure.HasTemperateGrowth invSqMeasure where
  exists_integrable := by
    use 2
    simp [invSqMeasure]
    rw [MeasureTheory.integrable_withDensity_iff]
    swap
    · fun_prop
    swap
    · rw [@ae_iff]
      simp
    conv =>
      enter [1, i]
      rw [ENNReal.toReal_ofReal (by positivity)]
    have h1 := (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
      (volume (α := EuclideanSpace ℝ (Fin 3))))
    have h2 : IntegrableOn (fun x : EuclideanSpace ℝ (Fin 3) =>  ((1 + ‖x‖) ^ 2)⁻¹ * (‖x‖ ^ 2)⁻¹) {0}ᶜ := by
      rw [MeasureTheory.integrableOn_iff_comap_subtypeVal]
      swap
      · refine MeasurableSet.compl_iff.mpr ?_
        simp
      let f := (fun x : EuclideanSpace ℝ (Fin 3) => ((1 + ‖x‖) ^ 2)⁻¹ * (‖x‖ ^ 2)⁻¹)
        ∘ @Subtype.val (EuclideanSpace ℝ (Fin 3)) fun x => (
          @Membership.mem (EuclideanSpace ℝ (Fin 3)) (Set (EuclideanSpace ℝ (Fin 3))) Set.instMembership {0}ᶜ x)
      have hf : (f ∘ (homeomorphUnitSphereProd (EuclideanSpace ℝ (Fin 3))).symm)∘
        (homeomorphUnitSphereProd (EuclideanSpace ℝ (Fin 3))) = f := by
        funext x
        simp
      change Integrable f _
      rw [← hf]
      refine (h1.integrable_comp_emb ?_).mpr ?_
      · exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (EuclideanSpace ℝ (Fin 3)))
      haveI sfinite : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpace
          Real.measureSpace.toMeasurableSpace Subtype.val volume) := by
        refine { out' := ?_ }
        have h1 := SFinite.out' (μ := volume (α := ℝ))
        obtain ⟨m, h⟩ := h1
        use fun n => Measure.comap Subtype.val (m n)
        apply And.intro
        · intro n
          refine (isFiniteMeasure_iff (Measure.comap Subtype.val (m n))).mpr ?_
          rw [MeasurableEmbedding.comap_apply]
          simp
          have hm := h.1 n
          exact measure_lt_top (m n) {x | 0 < x}
          exact MeasurableEmbedding.subtype_coe measurableSet_Ioi
        · ext s hs
          rw [MeasurableEmbedding.comap_apply, Measure.sum_apply]
          conv_rhs =>
            enter [1, i]
            rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)]
          have h2 := h.2
          rw [Measure.ext_iff'] at h2
          rw [← Measure.sum_apply]
          exact h2 (Subtype.val '' s)
          refine MeasurableSet.subtype_image measurableSet_Ioi hs
          exact hs
          exact MeasurableEmbedding.subtype_coe measurableSet_Ioi
      have hf' :  (f ∘ (homeomorphUnitSphereProd (EuclideanSpace ℝ (Fin 3))).symm) =
        fun x =>((1 + x.2.val) ^ 2)⁻¹ * (x.2.val ^ 2)⁻¹  := by
        funext x
        simp only [Function.comp_apply, homeomorphUnitSphereProd_symm_apply_coe, f]
        rw [norm_smul]
        simp only [Real.norm_eq_abs, norm_eq_of_mem_sphere, mul_one, sq_abs, mul_eq_mul_right_iff,
          inv_inj, inv_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, f]
        rw [abs_of_nonneg (le_of_lt x.2.2)]
        simp only [true_or, f]
      rw [hf']
      simp [Measure.volumeIoiPow]
      rw [MeasureTheory.prod_withDensity_right]
      swap
      · fun_prop
      rw [MeasureTheory.integrable_withDensity_iff ]
      swap
      · refine Measurable.ennreal_ofReal ?_
        refine Measurable.pow_const ?_ 2
        apply Measurable.comp
        · exact measurable_subtype_coe
        · exact measurable_snd
      swap
      · apply Filter.Eventually.of_forall
        intro x
        exact ENNReal.ofReal_lt_top
      have hf'' : (fun (x : ↑(Metric.sphere (α := (EuclideanSpace ℝ (Fin 3))) 0 1) × ↑(Set.Ioi (α := ℝ) 0)) => ( ((1 + x.2.val) ^ 2)⁻¹ * (x.2.val ^ 2)⁻¹ * (ENNReal.ofReal (↑x.2.val ^ 2)).toReal))
          = fun x =>  ((1 + x.2.val) ^ 2)⁻¹:= by
        funext x
        rw [ENNReal.toReal_ofReal]
        generalize (1 + ↑x.2.val) ^ 2 = l
        ring_nf
        have h2 : x.2.val ≠ 0 := by
          have h' := x.2.2
          simp  [- Subtype.coe_prop, f] at h'
          linarith
        field_simp
        ring_nf
        field_simp
        exact sq_nonneg _
      rw [hf'']
      apply (MeasureTheory.integrable_prod_iff' ?_).mpr ?_
      · refine aestronglyMeasurable_iff_aemeasurable.mpr ?_
        fun_prop
      · simp
        apply Integrable.const_mul
        rw [← @Measure.Subtype.volume_def]
        apply MeasureTheory.integrable_of_integral_eq_one
        trans ∫ (x : ℝ ) in Set.Ioi 0, ((1 + x) ^ 2)⁻¹ ∂volume
        · rw [← MeasureTheory.integral_subtype_comap]
          rfl
          exact measurableSet_Ioi
        trans  ∫ (x : ℝ ) in Set.Ioi 1, (x ^ 2)⁻¹ ∂volume
        · let f := fun x : ℝ => (x ^ 2)⁻¹
          change ∫ (x : ℝ ) in Set.Ioi 0, f (1 + x) ∂volume   = ∫ (x : ℝ ) in Set.Ioi 1, f x ∂volume
          let fa := fun x : ℝ => 1 + x
          change  ∫ (x : ℝ ) in Set.Ioi 0, f (fa x) ∂volume  =  _
          rw [← MeasureTheory.MeasurePreserving.setIntegral_image_emb (ν := volume)]
          simp [fa]
          simp [fa]
          exact measurePreserving_add_left volume 1
          simp [fa]
          exact measurableEmbedding_addLeft 1
        · trans ∫ (x : ℝ) in Set.Ioi 1, (x ^ (-2 : ℝ)) ∂volume
          · simp
            rfl
          rw [integral_Ioi_rpow_of_lt ]
          field_simp
          norm_num
          linarith
          linarith
    rw [← MeasureTheory.integrableOn_univ]
    apply MeasureTheory.IntegrableOn.congr_set_ae h2
    rw [← MeasureTheory.ae_eq_set_compl]
    trans (∅  : Set (EuclideanSpace ℝ (Fin 3)))
    · apply Filter.EventuallyEq.of_eq
      rw [← Set.compl_empty]
      exact compl_compl _
    · symm
      simp


def invSq : 𝓢((EuclideanSpace ℝ (Fin 3)), ℝ) →L[ℝ] ℝ := integralCLM ℝ invSqMeasure

[Joseph Tooby-Smith]

I was thinking maybe it would be good to define e.g. the following notation:

scoped notation "¹/r²" => invSq  (EuclideanSpace ℝ (Fin 3))

or similar.

(edit: removed part of message which was incorrect).

[Joseph Tooby-Smith]

I have a construction of a distribution from a function bounded by $c_1 ||r||^{-2} + c_2 ||r||^n$ in this PR. This is only for EuclideanSpace ℝ (Fin 3), but I'm sure everything should generalize nicely.

I'm not sure if this is something you're still aiming for @Kenny Lau , but if so, I suspect anything you produce here will be better then what I have - in which case this PR can be ignored or overwritten at a later date :).

[Kenny Lau]

@Joseph Tooby-Smith there might be a bit of time before my next PR, sorry

[ZhiKai Pong]

#PR reviews > Tempered distributions

@Moritz Doll (sorry for pinging) has a series of PRs on tempered distributions which I believe is closely related to what's been done here (e.g. Distribution) and we may want to update our version to match the mathlib version once it stabilizes. (I'm not so confident with the relevant maths yet)

[ZhiKai Pong]

on a related note there's also #30329 on generalised distributions

[Joseph Tooby-Smith]

Agreed! I wonder if it is possible to set up a Zulip bot that would ping a message when PRs are merged with Mathlib, and/or when a PR becomes a part of a tagged version of Mathlib. I think this would be very helpful in keeping track of these things when they actually get merged, so we can act on them then.

[Daniel Morrison]

I do know there's a Zulip topic #rss > Recent Commits to mathlib4:master which posts new merged PRs and includes a link to the PR so it seems like you could tell a bot to watch that topic and message you when certain PRs are mentioned. On the Github side I believe there's a way to link your PR to other ones and a bot there will comment changes. No idea how either of these work though

[Moritz Doll]

The definition of tempered distributions has now been merged (sorry forgot to mention it here), there is very little of actual useful objects (there are PRs for embeddings, multiplication and derivatives), just the Fourier transform. Fourier multiplier and convolution are work in progress

[Joseph Tooby-Smith]

Great @Moritz Doll - many thanks for postiing here ! We have some stuff specific for PhysLean around distributions in places over PhysLean e.g.

https://github.com/HEPLean/PhysLean/blob/094824dbb0fc6dad6cf46e99369a48b981cb9d88/PhysLean/SpaceAndTime/SpaceTime/Derivatives.lean#L273

So when we next merge with Mathlib we need to remove our definition of a distribution and update all the lemmas around it.

What do you mean by 'multiplication'? Multiplication of a distribution with what?

[Moritz Doll]

Multiplication with a function of temperate growth (i.e., all derivatives are polynomially bounded)