variations of Urysohn's lemma

Stream: mathlib4

[Yoh Tanimoto]

I saw that rieszContentAux does not have the proof that rieszContent is a Borel measure on X. For this purpose, following Rudin "Real and complex analysis", one needs certain variations of Urysohn's lemma. I wrote them here.
https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/urysohn.lean

Will this be useful? @Yury G. Kudryashov

I could make a pull request, but I think the file needs some refactoring, in particular, one should be able to use prod_mem in the induction, but I haven't found a way. Could someone help?

[Yury G. Kudryashov]

If you'll open a PR (even with sorrys), it will be much easier for other people to comment/review: e.g., one can switch to your branch, get olean cache, and fix a sorry or two.

[Filippo A. E. Nuccio]

The WIP tag for PR (and possibly also the help-needed) are precisely designed for this.

[Yoh Tanimoto]

thanks for your comments!
Just PRed #12266

[Sébastien Gouëzel]

Are you aware that we already have some material on contents, like docs#MeasureTheory.Content.measure_eq_content_of_regular (and all this file), which shows how a content automatically gives a measure under quite minimal assumptions? I guess the idea of the initial authors was to check these abstract assumptions for their Riesz content, instead of redoing everything by hand.

[Sébastien Gouëzel]

(The standard reference for this approach is Halmos' book on measure theory, instead of Rudin).

[Yoh Tanimoto]

ah no, I wasn't! Thank you very much, I was wondering why rieszContentAux remained at that point. But it seems that additivity is missing?

[Sébastien Gouëzel]

Yes, you are right, additivity is missing, there are definitely things that still have to be done!

[Yoh Tanimoto]

ok, if no one else is working on it, I will try to do that (I did it to some extent following Rudin, but it shouldn't be to difficult to adapt to MeasureTheory.Content.measure_eq_content_of_regular

[Yoh Tanimoto]

@Jesse Reimann @Kalle Kytölä is there any plan to expand rieszContentAux?

[Kalle Kytölä]

I am very sorry that this has stalled.

Jesse wrote a proof of the Riesz representation theorem on compact Hausdorff spaces in Lean3 in 2022. The intention was (and still is) to PR that to Mathlib. The proof used NNReal-valued bounded continuous functions (partly because nonnegativity is used in measure theory and partly to phrase the positive linear functional assumption concisely).

The main unsatisfactory thing about the implemented proof was related to the fact that with NNReal values, docs#BoundedContinuousFunction has no (truncated) subtraction or multiplication, so those were built in ad hoc ways in the proof (they are used slightly more in Riesz proof compared to for example the characterizations of weak convergence of probability measures, but both would benefit from having subtraction and multiplication). We therefore intended to first generalize the type-classes in docs#BoundedContinuousFunction.instSub and docs#BoundedContinuousFunction.instMul before fully porting the content from Lean3 to Lean4 and PRing. (I'll ask a question below on the best ways to do that with the current state.)

Unfortunately we have not yet gotten to it (the semester and other things got in the way soon after Mathlib4 came into proper existence).

[Kalle Kytölä]

My planned refactors to allow subtraction and multiplication of bounded continuous nonnegative functions involved introducing type classes HasBoundedSub, HasBoundedMul (perhaps with better naming) and perhaps refactoring the boundedness assumption in docs#BoundedContinuousFunction to use docs#Bornology.IsBounded. We discussed these a bit with @Anatole Dedecker in the summer. But actually since the summer, some metric boundedness phrasings were changed in Mathlib4, so I don't know (and have not thought about it much) what is currently the best way to generalize the subtraction and multiplication in BoundedContinuousFunction.

[Kalle Kytölä]

I'm in a workshop with lectures to prepare for another week + epsilon, but after that I would have a bit more time to think about what is the best way. But I also do not want to hold back any alternative approaches to Riesz representation theorem which are satisfactorily implemented and don't suffer from the NNReal-valuedness issue that we had in our approach! (Although I would still think those issues are worth addressing even just as general improvements of Mathlib.)

[Yoh Tanimoto]

I see, thanks for clarifying the background! Actually I am trying to write everything under Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f), because I didn't know until today that it was better to use EEReal for the measure theory. I think I will see how far I can go with this.

[Yoh Tanimoto]

On the other hand, it is natural to use Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f) when one wants to apply this to prove, for example, the spectral decomposition in infinite dimensional Hilbert space (or even ℂ)

[Sébastien Gouëzel]

There is also the issue that, currently, the linear functional is defined on bounded continuous functions. However, for Riesz-Markov-Kakutani on locally compact spaces, one should rather work with linear functionals on continuous functions with compact support. I don't know if we even have the bundled version of this space!

[Kalle Kytölä]

Yes, the main reasons we chose BoundedContinuousFunction in the compact case was that (a) it matches with weak convergence of finite measures and (b) it had a good topology instance already so for example stating that every positive linear functional automatically became continuous did not involve introducing any new topologies.

But indeed for locally compact spaces one can no longer use BoundedContinuousFunction. We did not do the locally compact case (just thought a bit about the reduction of that to the compact case), and did not think about whether the implementation should bundle continuity and compact support. I suppose @Jireh Loreaux will soon face such choices in the C*-algebra theory?

[Jireh Loreaux]

How do you mean? Note: we do have docs#ZeroAtInftyContinuousMap in case that's what you're referring to.

[Jireh Loreaux]

In general I won't need the space of continuous functions with compact support (at least not until people want to start doing noncommutative geometry, but that's a long way of I think)

[Yoh Tanimoto]

I wrote the density of the space of compactly supported continuous functions in C₀ here
https://github.com/yoh-tanimoto/mathlib4/blob/master/yoh/C_c/C_c.lean

If it's useful, I will add it to docs#ZeroAtInftyContinuousMap

[Yoh Tanimoto]

just PRed the linear-functional version #12290

[Jireh Loreaux]

@Yoh Tanimoto, certainly the density result would be nice. Although I think it can be written a bit more concisely. For example, there's no need to get an actual sequence. You can just start with an arbitrary epsilon and then get a function with compact support within that epsilon. This will simplify the proof a bunch. The existence of a sequence (if we wanted it at some point, would follow from the fact that the space is first countable; it's even metrizable).

[Jireh Loreaux]

I'll have some comments on #12290. But first, a question: where do you need the space to be Normal? I would have expected that locally compact Hausdorff (which implies locally normal) to be enough.

[Yoh Tanimoto]

OK, thanks for your comment! I will remove the part taking the sequence. May I add you as a reviewer to #12290?

As for #11290, I use NormalSpace X wherever I apply the version of Urysohn's lemma #12266 that uses normal_separation. Maybe that can be done with weaker assumption?

[Jireh Loreaux]

Yoh Tanimoto said:

May I add you as a reviewer to #12290?

sure

[Jireh Loreaux]

My point is that, without having actually read the proof in any detail, I suspect it suffices to apply this lemma after you have already restricted yourself to a compact subset of your space (in which case, for closed sets within this set, the normal separation would be valid without assuming NormalSpace X).

[Yoh Tanimoto]

OK, I will check the proof of my lemma

[Vincent Beffara]

Sébastien Gouëzel said:

There is also the issue that, currently, the linear functional is defined on bounded continuous functions. However, for Riesz-Markov-Kakutani on locally compact spaces, one should rather work with linear functionals on continuous functions with compact support. I don't know if we even have the bundled version of this space!

A bundled version of ContDiff and then a few restrictions of that (adding HasCompactSupport or something about integrability of iterated derivatives) would have been useful to me as well recently, I started a bare-bones version for PNT+ for functions defined on \R but a proper version with appropriate generality would likely have its place in Mathlib

[Anatole Dedecker]

Vincent Beffara said:

Sébastien Gouëzel said:

There is also the issue that, currently, the linear functional is defined on bounded continuous functions. However, for Riesz-Markov-Kakutani on locally compact spaces, one should rather work with linear functionals on continuous functions with compact support. I don't know if we even have the bundled version of this space!

A bundled version of ContDiff and then a few restrictions of that (adding HasCompactSupport or something about integrability of iterated derivatives) would have been useful to me as well recently, I started a bare-bones version for PNT+ for functions defined on \R but a proper version with appropriate generality would likely have its place in Mathlib

I did a start on that this summer in branch#AD_tests_functions, which depend on the (very out of date) #5912. The main pitfall I fell into (outside of slow continuous linear map instances, which were terrible at the time and are not fully solved AFAIK) is that I wanted to be able to choose the differentiability degree, to be able to state the isomorphism between "distributions with order less than $n$" and "distributions where you only require the test functions to be $C^n$", and ENat arithmetics made me give up...

[Anatole Dedecker]

Note that the continuous case will have to be done independently because its assumptions are way weaker. The reason I didn't start with this is that the algebraic boilerplate gets super long if we want to have assumptions as fine as for docs#ContinuousMap, but this is a bad reason, and I'd be happy to help setting it up if needed.

[Anatole Dedecker]

Also, some note about the only mathematically interesting thing, which is defining the topology: in the context of distribution theory, the natural topology to put on test functions is not the supremum of the topologies when you fix the compact set, it's the "locally convex enveloppe" of it. I don't know if one wants to do the same thing in the continuous case (maybe it doesn't change anything, I haven't thought about it).

[Anatole Dedecker]

And is that choice of topology consistent across different areas of mathematics, or is it really specific to distribution theory ?

[Anatole Dedecker]

Yoh Tanimoto said:

On the other hand, it is natural to use Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f) when one wants to apply this to prove, for example, the spectral decomposition in infinite dimensional Hilbert space (or even ℂ)

I think I agree with this. In general I'm not a big fan of abusing the NNReal-modules trick, e.g to talk about pointed convex cones, or other positivity constraints, but I do recognize that it allows for some nice code-factorization. In this case though, intuitively I would say we don't gain anything from it, even on the interface with measure theory, since one still has to convert between docs#NNReal and docs#ENNReal anyway.

That said, I remember that Kalle had good arguments when we talked about it last summer. I don't remember them exactly, but I'm ready to be convinced again.

[Yoh Tanimoto]

@Jireh Loreaux updated, added a version that finds g in an neighbourhood and commented out the version taking a sequence.
https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/C_c/C_c.lean

[Yoh Tanimoto]

@Jireh Loreaux @Anatole Dedecker to remove the NormalSpace assumption and use only LocallyCompactSpace and T2Space, I guess I will need something like

import Mathlib

example {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X}
    (H1 : IsCompact s) (H2 : IsCompact t) (H3 : Disjoint s t) :
    SeparatedNhds s t := by
  sorry

example {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X}
    (H1 : IsCompact t) (H2 : x ∉ t) :
    ∃ (U : Set X), ∃ (V : Set X), IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ t ⊆ U ∧ Disjoint U V := by
  sorry

Are there such lemmas already in mathlib? I couldn't find in the file Mathlib.Topology.Separation

[Anatole Dedecker]

I don't know if we have these exact results, but they follow easily from docs#IsCompact.disjoint_nhdsSet_left and docs#IsCompact.disjoint_nhdsSet_right. Let me look if I find something more direct

[Yoh Tanimoto]

ah ok, it was in that file on Compact sets, thanks!

[Dean Young]

@Yoh Tanimoto one might want a version using trinary. It would also be nice to see it used in Gel'fand duality.

[Jireh Loreaux]

I don't understand that comment. Also, note we already have Gelfand duality.

[Dean Young]

@Jireh Loreaux Let X be a compact Hausdorff topological space, in which we have that, for any closed disjoint subsets C₁ and C₂, there are open disjoint neighborhoods containing each.

Lemma: let x,y : X be distinct points. There is a continuous function f : X ⭢ [0,1] such that f x = 0 and f y = 1.

The proposed proof-strategy is to define trinary-nth-digit-functions dₙ : X ⭢ {0,1,2} such that, defining the function f : X ⭢ [0,1] such that f has trinary expansion d₀d₁d₂..., f is continuous, f x = 0, and f y = 1, using induction.

The use of trinary reflects two ends and a middle arising from the condition involving disjoint neighborhoods and use of closures where appropriate.

[Dean Young]

Given this lemma, we can conclude that φ : X ⭢ C*-alg(C(X,ℝ),ℝ) is injective using that φ x and φ y are different on the f shown to exist in the lemma.

[Dean Young]

Thanks for letting me know about the Gel'fand proof being in there. For surjectivity of φ : X ⭢ C*-alg(C(X,ℝ),ℝ), I think I like something like this: fix ν : C*-alg(C(X,ℝ),ℝ), which we aim to show is contained in the image of φ define p x := ∃(f : X ⭢ [0,∞)),ν f = 0,(∃ U : Neighborhood(x),∀(y : U),f y = 0).

Lemma: there is x such that ¬ p x. For a contradiction, suppose that ∀(x:X),p x . Using compactness of X, we can conclude that there are finitely many functions f₁,...,fₙ : X ⭢ ℝ, whose zero-sets cover X, and which have ν fᵢ ≠ 0. Define Πᵢ fᵢ. Then 0 ≠ Πᵢ ν(fᵢ) = ν (Πᵢ fᵢ )= ν (0) = 0, which contradiction shows the lemma.

From the lemma we have an x such that ¬ p x for this ν. It follows that ν = φ x.

A similar proof can be found here.

Edit: Jireh pointed out that this should be balanced ternary. It has an error as is.

[Jireh Loreaux]

It's still not clear to me what you're trying to do. What is φ? From what you wrote, it definitely seems like you're trying to construct one of the natural isomorphisms in Gelfand duality, but as I said, we already have it: docs#WeakDual.CharacterSpace.homeoEval. We also have docs#gelfandStarTransform, and the naturality is included in that file too.

[Dean Young]

@Jireh Loreaux The two goals are the first lemma concerning separation with use of trinary and proving Gel'fand duality. The mentioned φ is the same as the one you mention, with the construction skipped here, and no naturality shown either.

Overall I was interested in the use of trinary and how it related to the normal separation condition.

It's possible I misread the topic (it's a variation of the proof and not the result). To sum it up, the use of trinary and construction of dᵢ is potentially easier than other approaches.

[Yoh Tanimoto]

Do you mean you would like to use trinary to prove Urysohn's lemma?

[Jireh Loreaux]

(just FYI: it's ternary)

[Ron Z.]

@Yoh Tanimoto it looks like a proof of Urysohn's lemma which uses trinary in the construction of a functional f : X ⭢ [0,1], constructing each digit dᵢ separately.

[Yoh Tanimoto]

ok, I'm not sure if mathlib wants the same theorem with a different proof.
What is your thought? @Yury G. Kudryashov

[Ron Z.]

You might have to modify it to use binary. Let X be a normal topological space, so that for any disjoint closed subsets C₁,C₂, you can take the interior of the complement of the neighborhood of C₁ instead of just any neighborhood. This suggests binary.

[Dean Young]

@Ron Z. sorry, you're right. They have to be binary digits, and the C₁ and C₂ in question have to have closures which cover in some way. That makes me think it must be not much different than the proof they have.

[Yury G. Kudryashov]

I don't think that we want 2 proofs of exactly the same theorem. However, if you have a proof that implies the currently available versions of the theorem as well as some new versions, then we can drop the old proof.

[Yury G. Kudryashov]

Note: I'm not an expert in this area of math (I mean, I don't know what versions are true, what's the right generality to cover many versions in few theorems etc). I've just fomalized a version of Urysohn's lemma I needed for a partition of unity.

[Dean Young]

@Jireh Loreaux Sorry, I think you must be right.

@Yoh Tanimoto He's saying that the logic matches the use of balanced ternary: https://en.wikipedia.org/wiki/Balanced_ternary

In the function from ternary expansions to the interval, two functions I → I are featured, while expansions ending in all 0s or all 1s are not allowed. These end in T (terminates).

It seems like there are versions related to barycentric subdivision as well. I'll keep these thoughts around and return to the thread if these simplicial analogues amount to anything.

[Jireh Loreaux]

no, all I was saying is that the English term for base 3 is "ternary", not "trinary", nothing more. I've given no real thought to the rest of the construction.

But as Yury said, unless this construction does something for us that we can't already do (e.g., gives more general theorems, give additional theorems, or unifies and simplifies proof techniques), then we don't actually need a second proof.

That's not to say that you shouldn't pursue this if it interests you! Only that in the end it may not end up in Mathlib.

[Dean Young]

@Jireh Loreaux ok, thanks professor Loreaux.

[Kalle Kytölä]

Pertaining to the hiccups that made Riesz-Markov-Kakutani PRs on compact Hausdorff spaces stall originally, and as far as I understand, also in Yoh Tanimoto's recent attempt to use ℝ≥0 values:

I made #12559 which enables subtraction for nonnegative bounded continuous functions. If the model (new type class BoundedSub and otherwise minimal changes) is considered reasonable, I will do a similar PR to enable also multiplication of nonnegative bounded continuous functions.

[Yoh Tanimoto]

I made #12402 for the type of compactly supported functions and #12459 which is needed for additivity. It would be nice to have some more stuff such as HMul C(X, ℝ) C_c(X, ℝ) C_c(X, ℝ).

[Jireh Loreaux]

@Yoh Tanimoto for #12402, I've been meaning to comment but I've been a bit busy on another project. We'll want to topologize the compactly supported functions with the inductive limit topology, and then ensure that the metric you put on them generates that same topology definitionally. Unfortunately, I fear this is not an entirely trivial task.

[Jireh Loreaux]

@Anatole Dedecker do I remember that you had some work on the topology for compactly supported continuous functions, or was that for smooth test functions?

[Yoh Tanimoto]

@Jireh Loreaux sorry, I didn't mean to hurry you, and thanks for reviewing!
Do we want the inductive limit topology or the uniform topology? For some applications, I think the uniform topology is more natural for C_c.

[Jireh Loreaux]

I would have expected the inductive limit topology would be the more natural one most of the time, but maybe others disagree.

[Jireh Loreaux]

Because it's the one induced by the inclusion in the continuous functions, which has the compact-open topology.

[Anatole Dedecker]

I want to catch up everything more properly (here and everywhere else, sorry for people waiting for any kind of answer for me) so I'm just passing by.

Jireh Loreaux said:

Anatole Dedecker do I remember that you had some work on the topology for compactly supported continuous functions, or was that for smooth test functions?

It was for smooth test functions but it wasn't completed. Anyways, I have quite clear ideas about how to do it (for the inductive limit topology), so as soon as I get a bit more organized (which is soon, hopefully) I'd be happy to help with that.

Jireh Loreaux said:

I would have expected the inductive limit topology would be the more natural one most of the time, but maybe others disagree.

I agree with Jireh here (modulo the point I raised here), and I think if we want the uniform one we would use the subtype of docs#BoundedContinuousFunction instead ? But this is a bit of a naive answer maybe.

Jireh Loreaux said:

Because it's the one induced by the inclusion in the continuous functions, which has the compact-open topology.

I don't think it does ? Or am I misunderstanding what you mean by inductive limit topology ?

[Yoh Tanimoto]

I think C_c can be equipped with the compact-open topology, if it can also carry separately the uniform metric (or maybe a coercion to BoundedContinuousFunction or ZeroAtInftyContinuousMaps?)

[Sébastien Gouëzel]

Am I right that, for Riesz-Markov-Kakutani, one doesn't need to put any topology on C_c?

[Jireh Loreaux]

Anatole Dedecker said:

Jireh Loreaux said:

Because it's the one induced by the inclusion in the continuous functions, which has the compact-open topology.

I don't think it does ? Or am I misunderstanding what you mean by inductive limit topology ?

Oops! You're right. Sorry.

[Yoh Tanimoto]

Sébastien Gouëzel said:

Am I right that, for Riesz-Markov-Kakutani, one doesn't need to put any topology on C_c?

For RMK you are right! I just want to apply it to the proof of the spectral theorem and for this it would be nice if C_c were equipped with the uniform metric.

[Jireh Loreaux]

In that case you probably want to work with the subtype of bounded continuous functions with compact support. You can bundle it as an ideal.

[Jireh Loreaux]

Exactly which proof are you planning to follow for the spectral theorem? I'm asking because we'll likely want a version that works in any von Neumann algebra, not just all bounded operators. (And there's still a lot of von Neumann algebra theory that needs to be developed.)

[Yoh Tanimoto]

Jireh Loreaux said:

In that case you probably want to work with the subtype of bounded continuous functions with compact support. You can bundle it as an ideal.

Ah, I thought about defining a subtype, but I didn't know how to bundle operations (that C_cis closed under sum and product for example). By ideal do you mean this (and the product with ContinuousMap remains in C_c`)? Is there an example I can follow?

I tend to follow Rudin "Functional Analysis", but I would welcome if you have suggestions. I agree that it would be nice to have a version applicable to von Neumann algebras! I think the following version is the best? If A is a ((un)bounded) self-adojint operator on a Hilbert space H, then there is a measure space M, μ and a unitary U : H → MeasureTheory.Lp 2 μ such that U * A * (star U) is a multiplication operator?

[Yoh Tanimoto]

by the way, if one wants to define the support of a distribution ϕ, is it reasonable to restrict to a finite-dimensional vector spaces? I would define it as the complement of the union of all open sets U where any test function supported in U is annihilated by ϕ. But then I would need that such a union has the same property. It can be done if I assume LocallyCompactSpace for the vector space, but then it is finite dimensional. @Anatole Dedecker @Moritz Doll

[Jireh Loreaux]

Yoh Tanimoto said:

By ideal do you mean this (and the product with ContinuousMap remains in C_c`)? Is there an example I can follow?

No, I mean the product of a compactly supported function and a bounded continuous function is compactly supported. Of course, the same is true of continuous functions, but you get the wrong topology if you make it a subtype of those.

[Jireh Loreaux]

Yoh Tanimoto said:

If A is a ((un)bounded) self-adojint operator on a Hilbert space H, then there is a measure space M, μ and a unitary U : H → MeasureTheory.Lp 2 μ such that U * A * (star U) is a multiplication operator?

No, I don't think that is the standard version we should have (although having it in addiiton to the primary one would be okay). Also, you're going to run into major headaches with unbounded operators. Perhaps @Moritz Doll has already thought about that quite a bit.

For the bounded operators though, we'll want the Borel functional calculus, and I think we should proceed by defining projection-valued measures. But there's lots of work to do before we get there.

[Yoh Tanimoto]

Jireh Loreaux said:

No, I mean the product of a compactly supported function and a bounded continuous function is compactly supported. Of course, the same is true of continuous functions, but you get the wrong topology if you make it a subtype of those.

yes, but how do you implement it, do you have to use a constructor every time like `⟨f.1 * g.1, HasCompactSupport_mul f.2 g.2⟩or is there any better way?

[Jireh Loreaux]

just try making a term of type Ideal (α →ᵇ β) with carrier { f | HasCompactSupport f}. Then (after doing that) you can add some constructor which takes a continuous function, and a function with compact support, and produces a bounded continuous function, and you can show that this too has compact support (so it is in the ideal).

[Yoh Tanimoto]

Jireh Loreaux said:

No, I don't think that is the standard version we should have (although having it in addiiton to the primary one would be okay). Also, you're going to run into major headaches with unbounded operators. Perhaps Moritz Doll has already thought about that quite a bit.

For the bounded operators though, we'll want the Borel functional calculus, and I think we should proceed by defining projection-valued measures. But there's lots of work to do before we get there.

Yes, for that one would like to define weak/strong operator topologies as well.

[Yoh Tanimoto]

Jireh Loreaux said:

just try making a term of type Ideal (α →ᵇ β) with carrier { f | HasCompactSupport f}. Then (after doing that) you can add some constructor which takes a continuous function, and a function with compact support, and produces a bounded continuous function, and you can show that this too has compact support (so it is in the ideal).

mmm ok, I started to define C_c as an extension of ContinuousMap by following the way of ZeroAtInfty, and @Sébastien Gouëzel seemed to like it (#12290). Should I change to this?

[Jireh Loreaux]

It's not that I think you should change it. We should definitely have a separate C_c type, but that one should be equipped with the inductive limit topology (IMHO), and so you can't equip it with the uniform metric. So we should have both the separate type, and this ideal in the bounded continuous functions. And after we have both, we can have an algebra isomorphism between them.

[Yoh Tanimoto]

ah ok!

[Anatole Dedecker]

Yoh Tanimoto said:

by the way, if one wants to define the support of a distribution ϕ, is it reasonable to restrict to a finite-dimensional vector spaces? I would define it as the complement of the union of all open sets U where any test function supported in U is annihilated by ϕ. But then I would need that such a union has the same property. It can be done if I assume LocallyCompactSpace for the vector space, but then it is finite dimensional. Anatole Dedecker Moritz Doll

I feel like I'm about to say something stupid, but nontrivial test functions do not exist outside of finite dimensional vector spaces anyway, right ? Because it would give you a nonempty open set contained in a compact set.

[Yoh Tanimoto]

sorry, I was sloppy about "test function" and "Schwartz function". If we mean by "test function" a smooth function with compact support, then yes!

so I should have said as follows:  "I would define it as the complement of the union of all open sets U where any Schwartz function supported in U is annihilated by ϕ"

[Yoh Tanimoto]

I made this #12459, but it gets a lint error "2800 file contains 2615 lines, try to split it up". What should I do? @Anatole Dedecker

[Ruben Van de Velde]

Update the exceptions file

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/blob/master/scripts/style-exceptions.txt

[Yoh Tanimoto]

thank you, it worked!