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)

[ZhiKai Pong]

I'm a bit out of the loop on mathlib versions, are we ready to start this refactor or will it be in the next update?

[Joseph Tooby-Smith]

I think we are ready to refactor now with our current update.

[ZhiKai Pong]

I'll give it a go over Christmas (also to give myself a reason to learn the API). I'll probably come up with a lot of questions and will ask here.

[ZhiKai Pong]

so there is

docs#Distribution (defined as abbrev Distribution := 𝓓^{n}(Ω, ℝ) →L_c[ℝ] F)

and

docs#TemperedDistribution (defined as 𝓢(E, ℂ) →Lₚₜ[ℂ] F)

currently in Mathlib.

I don't really understand the difference in terms of topology etc., from what I gathered we should use the second one.

if my understanding is correct, should we just use the mathlib notation (i.e. 𝓢'(E, F) for TemperedDistribution E F) instead of the current E →d[𝕜] F?

[Joseph Tooby-Smith]

Yeah - I think we want the second one. I think the “pt” is related to the topology of the whole space, which I don’t think we use so shouldn’t affect anything.

I personally would be in favour of keeping the ‘E →d[𝕜] F’ notation, since to me it echos that this is like a function, which is how a physicist thinks about them. But happy to hear arguments against

[ZhiKai Pong]

my concern would be that if we are to use the mathlib API the notation mismatch might be confusing

[Alfredo Moreira-Rosa]

Not sure it's the right place to share this video, but here is a nice use of schwartz space functions for non standard Traces detection in particle colliders :
https://www.youtube.com/watch?v=DRS7TbjVTNQ

[ZhiKai Pong]

Also mathlib define this for complex ℂ: abbrev TemperedDistribution := 𝓢(E, ℂ) →Lₚₜ[ℂ] F whereas the PhysLean definition has [RCLike 𝕜]. Just want to check that we do indeed want the ability to write real-valued distributions before pinging Moritz to ask about implementation details

[Joseph Tooby-Smith]

Yeah, we are going to explicitly need it for the reals as well as the complex numbers. In electromagnetism, I think we only use it over the reals. I guess this is one advantage of the current notation - the field is explicit.

[Moritz Doll]

The reason to bake in the complex numbers is that the main motivation for Schwartz functions (and tempered distributions) is the Fourier transform and that is only defined if the codomain is a complex vector space. So even when you solve a PDE that is purely real like the wave equation, you might want to work over the complex numbers.

[ZhiKai Pong]

Thank you Moritz for explaining.

I'm thinking about the following: Maybe we keep the PhysLean version for physical distributions (point charges, current densities etc.), then cast towards the Mathlib version when we need to do Fourier transforms?

[ZhiKai Pong]

The refactor will then be to match analogous API (lemma and proofs where possible) to the Mathlib (complex) version counterpart, but keeping both versions, @Joseph Tooby-Smith do you think this is a good idea

[ZhiKai Pong]

I'm getting myself confused, should physical distributions (charges, currents) be docs#Distribution instead? the tempered part only comes in when we care about Fourier transforms etc.? but I also don't see any connection between docs#Distribution and docs#TemperedDistribution in mathlib, not sure if this is due to both parts being very new or I'm completely misunderstanding things.

[ZhiKai Pong]

if I'm not mistaken docs#TestFunction is ultimately the samething as IsTestFunction used in variational calculus, so it seems to me that we can refactor everything in mathlib API (not sure how challenging this will be)

[ZhiKai Pong]

sorry if this is a bit incoherent, it's late here and I'm quite confused about all of these, just summarizing my thoughts here:

1. For physical distributions, the object we want is 𝓢(E, 𝕜) →L[𝕜] F which is defined over both real and complex whereas the mathlib docs#TemperedDistribution is only defined over the complex.

• 1.1 docs#Distribution requires compact support which is not necessarily the case for physical distributions so it is irrelevant here (is this correct?)

• 1.2 Do we want to duplicate the mathlib API for multiplication and derivatives etc.?

2. @Joseph Tooby-Smith in PhysLean, is distributions and variational calculus currently "orthogonal" in the sense that they can be dealt with separately?

• 2.1 a separate refactor of IsTestFunction should be done?

3. Mathematically, is it correct to say that tempered and has compact support are independent properties, and the mathlib definitions of docs#Distribution and docs#TemeperedDistribution only conincide when the object has both?

is it correct that compactly supported implies temperedness, so docs#TemeperedDistribution is strictly more general than docs#Distribution ?

[Joseph Tooby-Smith]

In response to your points:

1. Yes we want 𝓢(E, 𝕜) →L[𝕜] F.
   1.1 Yes, docs#Distribution is defined on compactly supported functions whilst docs#TemeperedDistribution is defined on all Schwartz maps. Every compactly supported function is a Schwartz map, so every docs#TemeperedDistribution is also defined on all compactly supported functions, and thus is a docs#Distribution. (as your last comment indicates).
   1.2 We currently have derivatives for distributions, but not multiplication. I think it would be worth reproducing this.

2. Yes, distributions and variational calculus are currently orthogonal. In fact, I think they might have to stay this way, since I do not know of anyway to even define a Lagrangian for distributions (instead of functions).
   2.1. I think a refactoring for IsTestFunction should be done.

[ZhiKai Pong]

@Moritz Doll May I ask why does mathlib use docs#LineDeriv for SchwartzMap and TemperedDistribution instead of docs#fderiv ?

I'm trying to understand the difference between the mathlib inplementation and https://physlean.com/docs/PhysLean/Mathematics/Distribution/Basic.html#Distribution.fderivD, especially on the usage of docs#SchwarzMap.fderivCLM

I'm guessing it makes some Fourier stuff easier, but I have never used LineDeriv before so not really sure what's the difference, and if there's a way to convert between the two

[Moritz Doll]

I think it is way more convenient in distribution theory to deal with maps with equal domain and codomain. If you use docs#fderiv directly (and we have docs#SchwartzMap.fderivCLM), then the definition for distributions becomes lengthy because you have to rearrange the evaluation map. This is exactly why the definition of fderivD is so tedious. However the definition for the directional derivative is just one line, docs#TemperedDistribution.instLineDeriv.
Note that lineDerivOp is mainly for the notation (and then there are algebraic type-classes on top), so it all looks very nice (and consistent).
For the Fourier transform on Schwartz functions, we proved docs#SchwartzMap.fderivCLM_fourier_eq first and then deduced the variants for the line derivative, whereas for tempered distributions it follows for the line derivatives directly from duality, so no fderivCLM needed.

[ZhiKai Pong]

Many thanks @Moritz Doll for typing this out. I've tried playing around with it a bit but am still kind of lost (could very well be my knowledge of distributions isn't good enough), I'm wondering would it be possible to demonstrate something like derivative of the heaviside step function (not even sure how to write this as a distribution) equals Dirac delta or is this actually much more completed than I think.

(@Joseph Tooby-Smith I thought you had something along these lines for 1D point charge, is it still somewhere in PhysLean or am I misremembering?)

[Moritz Doll]

There is a bit of stuff missing, but nothing too major:

import Mathlib.Analysis.Distribution.TemperedDistribution

open SchwartzMap MeasureTheory

open scoped LineDeriv

noncomputable section

def heaviside : 𝓢'(ℝ, ℂ) where
  toFun f := ∫ x in Set.Ioi 0, f x
  map_add' := sorry
  map_smul' := sorry
  cont := sorry

@[simp]
theorem heaviside_apply (f : 𝓢(ℝ, ℂ)) : heaviside f = ∫ x in Set.Ioi 0, f x := rfl

@[simp]
theorem lineDerivOp_eq_deriv (f : 𝓢(ℝ, ℂ)) (x : ℝ) : ∂_{(1 : ℝ)} f x = deriv f x := rfl

theorem linederiv_heaviside : ∂_{(1 : ℝ)} heaviside = TemperedDistribution.delta (0 : ℝ) := by
  ext f
  simp only [TemperedDistribution.lineDerivOp_apply_apply, heaviside_apply, SchwartzMap.neg_apply,
    lineDerivOp_eq_deriv, TemperedDistribution.delta_apply]
  rw [MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto (f := -f) (m := 0)]
  · simp
  · fun_prop
  · intro x hx
    exact (f.hasDerivAt x).neg
  · refine Integrable.integrableOn ?_
    apply (-derivCLM ℝ ℂ f).integrable
  · sorry

obviously not mathlib level code. The last sorry is obviously true and follows from the statement about cocompact filters in mathlib.

[ZhiKai Pong]

Thanks! I'll try to work through this later

[Joseph Tooby-Smith]

@ZhiKai Pong This was for the point particle in 1 dimension, but I replaced the heaviside step function with (x-r)/||x-r||, as this was more general, and carried over to higher dimensions.

The corresponding derivatives are calculated in this file:

https://github.com/lean-phys-community/PhysLean/blob/master/PhysLean/SpaceAndTime/Space/Norm.lean

Maybe the thing to do here is relate fderiv of our distributions to linederiv, if possible.

[ZhiKai Pong]

Yea I'm planning to refactor the relevant PhysLean parts to follow Mathlib more closely, I'm still experimenting to see how everything fits together, especially since we want to be able to do stuff with 𝓢(E, 𝕜) →L[𝕜] F, maybe we just duplicate the whole docs#TemperedDistribution API but I'll think about it

[ZhiKai Pong]

I can see this being a source of confusion (it already is quite confusing) I'm thinking maybe some sort of namespace structuring might be helpful but we should probably be more careful about this and think this through

[Joseph Tooby-Smith]

In PhysLean we have the condition IsDistBounded which is different from HasTemperateGrowth (in particular it deals with non-smooth functions such as $x \mapsto 1/\|x\|$, which often appear in physics).

We have things like the following

distOfFunction (fun x : Space d.succ => ‖x‖ ^ (- d.succ : ℤ) • basis.repr x) (by fun_prop)

Here the by fun_prop is a proof of a IsDistBounded lemma. I am wondering if we can define a macro, so we can make this look much more like a function. I'm thinking of something like:

⸨‖x‖ ^ (- d.succ : ℤ) • basis.repr x⸩ᵈ

to represent the above, where the x is automatically inferred and the fun_prop is automatically proved.

[Joseph Tooby-Smith]

In addition to the above, maybe some sort of equality =d which takes a distribution on the left and a function on the right, and is true when the distribution corresponds to the integration of the function.

[Joseph Tooby-Smith]

I have put an implementation of the ⸨‖x‖ ^ (- d.succ : ℤ) • basis.repr x⸩ᵈ style notation in PhysLean#953, along with some other simplifying definitions around distributions.