Measures on R^n

Stream: new members

[jsodd]

I was trying to understand how measure theory is formalised in Lean, so I wanted to prove something about measures on R^n. As a first step, I needed measurability of linear functionals, but I couldn't make it work. Here's an example:

import Mathlib

open MeasureTheory

variable {n : Type} [Fintype n]
abbrev V := n → ℝ
variable {l : V →L[ℝ] ℝ}

#check ContinuousLinearMap.measurable l

I've tried matching the type manually (I guess I'm really not supposed to do that, but I see no other option) as follows:

variable [h₁ : NormedAddCommGroup V]
variable [h₂ : @NormedSpace ℝ V _ h₁.toSeminormedAddCommGroup]
variable {h₃ : OpensMeasurableSpace V}

#check @ContinuousLinearMap.measurable ℝ _ V h₁ h₂ _ h₃

but Lean says that

  h₃
has type
  @OpensMeasurableSpace V Pi.topologicalSpace MeasurableSpace.pi : Prop
but is expected to have type
  @OpensMeasurableSpace V UniformSpace.toTopologicalSpace MeasurableSpace.pi : Prop

What should be the right way to set up simple Borel measures on R^n?

[Daniel Weber]

The problem is that this abbreviation needs n as an argument. This works:

import Mathlib

open MeasureTheory

variable {n : Type} [Fintype n]
variable {l : (n → ℝ) →L[ℝ] ℝ}

#check ContinuousLinearMap.measurable l

[jsodd]

Thank you very much! Is there some way to label R^n as I tried to avoid writing the definition every time?

[Daniel Weber]

I think you can use local notation for that

[Daniel Weber]

Something really weird is going on here:

import Mathlib

open MeasureTheory

variable {n : Type} [Fintype n]
local notation "V" => n → ℝ
variable {l : V →L[ℝ] ℝ}

-- declaration uses 'sorry'
example : Measurable l := ContinuousLinearMap.measurable l

I think someone who knows more about the internals is needed

[Daniel Weber]

here is a Mathlib-free minimization

variable (n : Type)
local notation "V" => n → Nat
variable (l : V)

-- l : sorryAx (Sort ?u.631) true → Nat
#check l

[Daniel Weber]

Adding a type ascription makes it fail earlier, but only if something it written after it:

variable (n : Type)
local notation "V" => (n → Nat : Type)
-- unknown constant 'n✝'
variable (l : V)

#check 1

[Etienne Marion]

(deleted)

[jsodd]

Hmm, it's a bit awkward to write n → ℝ all the time... Ideally, I'd call it just ℝ^n, but I understand that it's again the limitations of parsing/pretty printing. Strange that it's wrong here

[Etienne Marion]

Maybe notations cannot be used for types

[jsodd]

Yeah, I guess... Should there be a type for R^n then? It's a super common thing.

[Etienne Marion]

Well I don’t think you would gain a lot, because you would still have to write n everywhere

[jsodd]

Is there a reason why we use n → ℝ for vectors instead of Mathlib.Data.Vectors?

[Etienne Marion]

I don’t know, but if I had to guess I would say that maybe these are rather intended for things about computations and other cs stuff, while n \to \R is more mathematical

[jsodd]

It would be nice to be able to use the usual mathematical notation for $X^Y = \{ f \colon Y \to X \}$. Such as in $\R^\R$

[jsodd]

Maybe there's some way to set up an instance of HPow

[jsodd]

Now that I think of it, it does sound a bit useless... But the $R^n$ notation is too common and occurs too often.

[Kevin Buzzard]

(two $ signs in Zulip for entering TeX maths mode)

[Luigi Massacci]

I'm unclear as to why you find $X^Y$ clearer than $Y \to X$, if anything I've always found the latter to be one of the most elegant notational tricks of type theory

[Luigi Massacci]

And it's quite understandable too

[jsodd]

I agree, yes. Just wanted to write $\mathbb{R}^n$, but I understand why it's done this way

[Eric Wieser]

Do you want to write R^n or R^Fin n for n : Nat?

[jsodd]

@Eric Wieser I already convinced myself that $n \to \R$ looks good, but to answer your question, I'd write R^n for n : Fintype. This way it agrees with the convention $X^Y = \{ f \colon Y \to X \}$.

On the other hand, it would be interesting to know whether Lean is capable of doing things like this. But this question is by no means important, so...

[Luigi Massacci]

I hadn’t actually noticed that you were writing Fintype n, which is positively bizarre. Using $n$ as a symbol for a set (/type) as opposed to a number is bound to generate confusion. It reminds me of the following paragraph by Halmos in How to write Mathematics:

As history progresses, more and more symbols get frozen. The standard examples are $e$, $i$ and $\pi$, and, of course, 0,1,2,3,... (Who would dare write “Let 6 be a group.”?) A few other letters are almost frozen: many readers would fell offended if “$n$” were used for a complex number, “$\varepsilon$” for a positive integer, and “$z$” for a topological space. (A mathematician’s nightmare is a sequence $n_\varepsilon$ that tends to 0 as $\varepsilon$ becomes infinite.)

[Luigi Massacci]

I think this is what @Eric Wieser was pointing out to you

[jsodd]

$$6 = \{ \varnothing, \{ \varnothing \}, \{ \varnothing, \{ \varnothing \} \}, \{ \varnothing, \{ \varnothing, \{ \varnothing \} \} \},\{ \varnothing, \{ \varnothing, \{ \varnothing, \{ \varnothing \} \} \} \}, \{ \varnothing, \{ \var nothing, \{ \varnothing, \{ \varnothing, \{ \varnothing \} \} \} \} \} \}$$

[Ruben Van de Velde]

n and m are pretty common for fintypes in mathlib, for example for $m\times n$ matrices

[Luigi Massacci]

I completely forgot about matrices using that notation. Though I would argue that is not quite the same situation nvm that was an indefensible position.

[jsodd]

Zulip doesn't like what I wrote, so here's the picture
image.png

[jsodd]

https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers

[Luigi Massacci]

jsodd said:

https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers

Yes of course, but the point of type theory is in part avoiding the absurdities of set-theoretic encodings…

[Luigi Massacci]

But I will retract my complaint anyway

[jsodd]

My point is: even though 6 is most certainly not a group, it may well be a set

[Kevin Buzzard]

The fact that you think that it's reasonable to think that 6 is a set is in my opinion evidence that you have lost track of mathematics and have become infected by set theory. One of my favourite things about type theory is that 6 means 6, it's not encoded as a set :-)

[Kevin Buzzard]

I should probably add that ten years ago I also thought that it was reasonable to think of 6 as a set, because I knew of no other way of setting up mathematics!

[jsodd]

Well, I'm clearly neither set- nor type- theorist, and you probably know that for an outsider of the foundations of mathematics most of these questions seem irrelevant. 6 as a type, 6 as a set, whatever... And although the notion of 6 as an archetypal set of 6 elements corresponds well to how I think about it, I won't hold onto it too tightly.

[jsodd]

But I'll take note that referring to numbers as sets is dangerous among type theorists :smile:

[Kevin Buzzard]

In type theory, numbers are terms not types, which somehow seems more sensible to me.