Fourier Transform

Stream: PhysLean

[Kenny Lau]

@ZhiKai Pong What are the main difficult(ies) you have faced with the Fourier Transform?

[ZhiKai Pong]

What I want to do is essentially this:
https://en.wikipedia.org/wiki/Analytic_signal

but part of the difficulty also comes from not knowing exactly what I need, give me some time and let me sketch it out

[Kenny Lau]

yeah I think the first thing I need to know is the exact domain (of functions R -> C) that the Hilbert transform is defined on.

[ZhiKai Pong]

image.png
image.png

so the premise is this, given a "signal" Vʳ(t) I want to construct a signal V(t) = Vʳ(t) + H(Vʳ(t)) where H is the Hilbert transform. From the text I believe the Hilbert transform is just from a real function to another real function, and the "signal" Vʳ(t) should be square integrable, but I don't know enough about functional anlysis to be certain of this or if there's anything else I'm missing.

To complicate things further, under this framework I also want to represent a simple cos(ω*t) with Complex.exp (Complex.I*ω*t) (where ω = 2πν). Just from the formula this seems to work if a(ν) is just the Dirac delta, and this makes me think a(ν) should be SchwartzMap. However I think cos isn't square integrable and I'm reading on how people work around this.

[ZhiKai Pong]

My plan was to define $a(\nu)$ and $\phi(\nu)$ in a structure, and from that structure define (1), (2), (4), and prove (3) and (5) (as suggested here). as mentioned $a(\nu)$ should be a distribution, so one can have dirac-delta functions etc.

One could then also define a function which takes a $V(t)$ to this structure and show that under certain conditions it is an inverse of (1), probably via Fourier transform api but again this is something I don't know how to at the moment.

[Kenny Lau]

ZhiKai Pong said:

Hilbert transform is just from a real function to another real function

surely you need to be integrable?

[ZhiKai Pong]

(see this is what a mathematician immediately thinks, but in physics and engineering this is always just assumed and we almost never think about this :( )

[ZhiKai Pong]

Kenny Lau said:

surely you need to be integrable?

I wouldn't disagree, but the truth is I don't know lol

[ZhiKai Pong]

(isSchwartzMap integrable?)

[Joseph Tooby-Smith]

Yep, docs#SchwartzMap.integrable, but note that the dirac delta function is not a SchwartzMap but is rather in the dual space of SchwartzMap's.

[ZhiKai Pong]

I think the issue with cosine should in principle be the same with taking the Fourier transform of a periodic function, which on its own is not square integrable, but there is a trick that takes a full period, set everything else to zero and take the Fourier transform of the truncated function instead (at least that's how I was taught). If there's an example showing how this is done I think that'll be very useful

[ZhiKai Pong]

image.png
image.png
image.png
image.png
For completeness I'm including those screenshots here for the full exposition. I think at the moment I'll probably ignore the parts about stationary random processes, and show eq (19) holds (time average of complex representation equals the time average of the original real signal). I think there's the more general result that the inner product of two real signals can be calculated by the complex inner product, but I'm not so sure on this one.

[ZhiKai Pong]

15.0_pp_554_632_Interference_and_diffraction_with_partially_coherent_light.pdf
Apologies if anything's unclear, maybe it's easier if I just upload the chapter, what I'm looking for is essentially section 10.2

[ZhiKai Pong]

(but also I'm fully aware that my mathematical understanding of this is very lacking, so I've put this aside for the moment and am not in a hurry to formalize this)

[Joseph Tooby-Smith]

To complicate things further, under this framework I also want to represent a simple cos(ω*t) with Complex.exp (Complex.I*ω*t) (where ω = 2πν). Just from the formula this seems to work if a(ν) is just the Dirac delta, and this makes me think a(ν) should be SchwartzMap. However I think cos isn't square integrable and I'm reading on how people work around this

The same thing happens in quantum mechanics, you have wave-functions like $e^{i k x}$, which are not square integrable. What people do there, and I think what may be possible here, is to consider two different spaces of functions.

1. The first space is SchwartzMap or something similar.
2. The second space is the dual of SchwartzMap.

then e.g. $e^{i k x}$, the dirac delta function, the cosine etc, all live in the second (more general and larger) space, whilst all the 'physical' functions actually live in the first space (smaller) space.

Maybe something similar could be done here with SchwartzMap maybe replaced to something larger like smooth square-integrable functions. (I don't know if smooth square-integrable functions is a nice function space, e.g. whether it has a good topology etc).

[ZhiKai Pong]

I think we can start with some concrete examples - for example let's calculate the fourier transform of a single cosine, and see how that should look like

[Joseph Tooby-Smith]

Problem is that the fourier transform of a cosine contains dirac deltas (which may be the point).

[ZhiKai Pong]

yes that's what I'm thinking :)

[ZhiKai Pong]

looking at SchwartzMap.fourierTransformCLM is just very overwhelming and I have no idea what it's saying (what's a BorelSpace, what is V and E etc.)

noncomputable def SchwartzMap.fourierTransformCLM(𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] :
SchwartzMap V E →L[𝕜] SchwartzMap V E

I kind of know the Fourier transform can be viewed as a transformation between a function space and its dual space, but this statement had no significance to me whatsoever for performing calculations. I understand it is important and will take time to learn but at the same time this is what I mentioned about this being probably too abstract for an engineer/physicist and PhysLean should try to bridge this gap

[Kevin Buzzard]

docs#BorelSpace is a true-false statement, not a space. BorelSpace V means "the measure space structure on V and the topology on V are compatible"

[Joseph Tooby-Smith]

ZhiKai Pong said:

looking at SchwartzMap.fourierTransformCLM is just very overwhelming and I have no idea what it's saying (what's a BorelSpace, what is V and E etc.)

noncomputable def SchwartzMap.fourierTransformCLM(𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] :
SchwartzMap V E →L[𝕜] SchwartzMap V E

I kind of know the Fourier transform can be viewed as a transformation between a function space and its dual space, but this statement had no significance to me whatsoever for performing calculations. I understand it is important and will take time to learn but at the same time this is what I mentioned about this being probably too abstract for an engineer/physicist and PhysLean should try to bridge this gap

I agree with this, although I think it is in general going to be very difficult to do - but no one said any of this was meant to be easy :).

I think one thing we can do to help (although does not solve the problem fully) is to pick a couple of files, maybe one for each area of physics, and make it an 'entry' point to the project or that area, by writing really careful and full documentation, maybe with examples. For example, SpaceAndTime.Space.Basic could be used, with better documentation and examples etc, as an entry point of the project. We could then collate these entry points into a list for people to reference.

Obviously one could do something like this outside of the project (which is something I tried to do with https://notes.physlean.com), but one quickly runs into dependency issues etc. when things are changed.

[Kenny Lau]

https://web.abo.fi/fak/mnf/mate/kurser/fourieranalys/chap3.pdf

I don't know if I'm saying something redundant here, but here's a pdf talking about Fourier transform of distributions. Does this look helpful?

[Joseph Tooby-Smith]

@Kenny Lau Would I be correct in drawing the following conclusion from that note: If I work with distributions, I never have to worry about any of the following:

1. Whether or not a derivative exists, since it always does.
2. Whether or not the fourier transform exists, since it always does.

If so - seems like they should be a lot lot easier to work with in general then working with functions ℝ → ℂ, for example.

Also every function I could possibly think of working with in physics, describes a distribution:

• The dirac delta function
• The potential $1/r^2$ (even though it's not smooth).
• A Heaviside step function
• Functions like $e^{ikx}$ etc.

Also, not sure how accurate this is, but if I think of the test functions (the Schwartz maps) as ways I can sample things in the physical world, then a distribution also makes sense physically, since all it is doing is assigning to each of these ways I can sample the world a value in a nice way.

[Joseph Tooby-Smith]

(If this is all correct, it may be worth building a physics-style API around distributions, to make things look as 'safe' as possible).

[Kenny Lau]

@Joseph Tooby-Smith i'm not an expert but those claims seem true to me

[Kenny Lau]

image.png

image.png

[Kenny Lau]

These are the sources of your claims

[Kenny Lau]

(I think there's a typo in 3.27 where S in "distribution f in S" should be S')

[Joseph Tooby-Smith]

Thanks for finding these!

[ZhiKai Pong]

I've started to look at this, is this the correct syntax for stating what I think it's saying?
(fourier transform of constant function is the dirac delta)

lemma fourierTransform_of_const_eq_diracDelta :
    fourierTransform ℝ ℂ (const ℂ ℝ 1) = (diracDelta ℂ 0) := by
  sorry

I'll try to see whether I can use what's available to prove this, and hopefully build up the API required along the way if needed

[ZhiKai Pong]

(or if this is actually straightforward please let me know, trying to lean my way through the new definitions in the file and don't really have a feeling about this yet)

[Kenny Lau]

are these in distributions?

[ZhiKai Pong]

yes, in the distribution file you defined a while ago

[ZhiKai Pong]

maybe I'm misinterpreting your question: the const part is just a function fun x => 1, but then the fourierTransform is defined as (E →d[ℂ] F) →ₗ[ℂ] (E →d[ℂ] F), and since diracDelta is a distribution I have to use this definition? it's possible I'm misunderstanding something here

[Kenny Lau]

yeah this should be fine