Lusin's theorem

Stream: mathlib4

[Cris Salvi]

Has Lusin's theorem been formalised?

For reference, it states that given any measurable function f and any ε > 0, there exists a compact set K such that the measure of the complement of K is less than ε, and the function f is continuous when restricted to K.

[Ruben Van de Velde]

grep finds

Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:Then, we show Lusin's theorem that two disjoint analytic sets can be separated by Borel sets.
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:We then prove the Lusin-Souslin theorem that a continuous injective image of a Borel subset of
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:/-- The hard part of the Lusin separation theorem saying that two disjoint analytic sets are
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:/-- The **Lusin separation theorem**: if two analytic sets are disjoint, then they are contained in
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:/-- The **Lusin-Souslin theorem**: the range of a continuous injective function defined on a Polish
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:  -- their images, by injectivity of `f` and the Lusin separation theorem.
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:/-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a Polish space, then its image under
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean:/-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a standard Borel space,
Mathlib/MeasureTheory/Function/Jacobian.lean:The measurability of `f '' s` follows from the deep Lusin-Souslin theorem ensuring that, in a
Mathlib/MeasureTheory/Function/Jacobian.lean:Lusin-Souslin theorem.
Mathlib/Topology/MetricSpace/Polish.lean:  set is clopenable. Once the Lusin-Souslin theorem is proved using analytic sets, we will even

Do you mean any of those?

[Yury G. Kudryashov]

@loogle Measurable, ContinuousOn, Exists

[loogle]

:shrug: nothing found

[Yury G. Kudryashov]

@Sébastien Gouëzel Do you know what related results are already in the library?

[Antoine Chambert-Loir]

Ruben Van de Velde said:

grep finds
(...)
Do you mean any of those?

No, this is another theorem by Lusin.
https://en.wikipedia.org/wiki/Lusin%27s_theorem
Vs
https://en.wikipedia.org/wiki/Lusin%27s_separation_theorem

[Kexing Ying]

I know that one of @Kevin Buzzard’s student formalized it. I don’t know if it is publicly available anywhere

[Kevin Buzzard]

I'm in a field for a week with no computer but I don't know which student. If it was for a project for my course then it could well have been lean 3, it might have been poorly-written and it will not be made publically available without the students' consent (and if they've since left Imperial then this might be hard to get)

[Cris Salvi]

Thanks @Kevin Buzzard. If at any point you happen to identify the student, maybe I could get in touch to ask a few questions.

[Kevin Buzzard]

My advice is just to formalise the book proof and forget the fact that someone might have done it before.