Zulip Chat Archive
Stream: Is there code for X?
Topic: How do I make a Wikipediastyle metric space in Lean?
Lars Ericson (Dec 02 2020 at 04:57):
Metric space in Lean takes a single type as argument, for example
import topology.metric_space.basic
variable M: Type
variable S: metric_space(M)
It tells me this: "Each metric space induces a canonical uniform_space and hence a canonical topological_space. This is enforced in the type class definition, by extending the uniform_space structure. When instantiating a metric_space structure, the uniformity fields are not necessary, they will be filled in by default. In the same way, each metric space induces an emetric space structure. It is included in the structure, but filled in by default."
I would like to come at this from a different direction. I want to supply M
with a metric d
, following the Wikipedia definition in which M
is any set (or just Type
), and d:MxM→ ℝ
has 3 properties:
import topology.metric_space.basic data.real.basic
variable M: Type
variable S: metric_space(M)
variable d: Y → (Y → ℝ)
variables x y : Y
def identity_of_indiscernibles := d x y = 0 ↔ x = y
def symmetry := d x y = d y x
def subadditivity := d x z ≤ d x y + d y z
def metric :=
identity_of_indiscernibles ∧
symmetry ∧
subadditivity
So a couple of hopefully very basic questions:
Q1. Where is metric
in mathlib
?
Q2. Suppose multiple distinct choices d
of metric are suitable for a given set M
. So in this case it is not sufficient to say
variable S: metric_space(M)
I need to be able to differentiate
variable d1: metric
variable d2: metric
variable S1: metric_space M d1
variable S2: metric_space M d2
Is there "this kind" of metric space in mathlib
, or do I have to start from scratch or from some other direction?
Johan Commelin (Dec 02 2020 at 05:52):
@Lars Ericson (Re Q1: I don't think we have that exact concept.) What do you mean with "multiple distinct choices of d
"?
Should they induce the same topology? If not, you can write S1 : metric_space M
and S2 : metric_space M
, but using those will be annoying.
What people typically do, is introduce a socalled "type synonym". For example, if X : Type
and linear_order X
, then order_dual X
is a type with the opposite order. By definition order_dual X := X
, but because they are not syntactically equal, the can carry different instances of the same type class.
Lars Ericson (Dec 02 2020 at 05:58):
@Johan Commelin I mean in the practical sense that I could have d1(x,y) = abs(xy)
or d2(x,y)=\sqrt((xy)^2)
and they are not quite the same.
These are my multiple distinct choices. You could call them L1 norm, L2 norm and so on. So I want to distinguish two metric spaces, S1=(d1,R)
and S2=(d2,R)
and reason about them separately, but have both rely on the concept that a metric space is a set with a metric. I am coming at this from a very basic perspective. So for example my proof that d1 is a metric might differ slightly from my proof that d2 is a metric.
Johan Commelin (Dec 02 2020 at 06:48):
@Lars Ericson The short answer is that with the current setup in mathlib, you can use metric_space
for what you want, but it might become painful. One option to alleviate the pain is to use type synonyms.
Johan Commelin (Dec 02 2020 at 06:48):
People have been working on lp spaces recently, if I'm not mistaken.
Patrick Massot (Dec 02 2020 at 07:57):
Lars, handling iterated conjunctions turns out to be painful. Having a structure with three fields is much more convenient than a definition like your metric
. With your definition of metric, if you have P : metric M d x y z
, you access symmetry as P.2.1
(or P.right.left
). With a structure having a second field names symm
you could have P.symm
for instance.
Patrick Massot (Dec 02 2020 at 07:58):
Did you watch all LFTCM2020 videos? One of them is about redoing metric spaces from scratch.
Patrick Massot (Dec 02 2020 at 08:02):
Lars Ericson said:
I mean in the practical sense that I could have
d1(x,y) = abs(xy)
ord2(x,y)=\sqrt((xy)^2)
and they are not quite the same.
What is the type of x
and y
in the above sentence? I have a hard time guessing an answer that would make d1
and d2
"not quite the same", unless you mean not defeq.
Patrick Massot (Dec 02 2020 at 08:21):
Note that if you don't like type aliases (which can be pretty tricky for the elaborator, hence for the user) then you always have the possibility to completely bypass type class resolution. For instance:
import topology.metric_space.basic
noncomputable theory
def m1 : metric_space (ℝ × ℝ) :=
{ dist := λ x y, max (abs (x.1  y.1)) (abs (x.2  y.2)),
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
def m2 : metric_space (ℝ × ℝ) :=
{ dist := λ x y, real.sqrt ((x.1  y.1)^2 + (x.2  y.2)^2),
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
def t1 : topological_space (ℝ × ℝ) := m1.to_uniform_space.to_topological_space
def t2 : topological_space (ℝ × ℝ) := m2.to_uniform_space.to_topological_space
local notation `cont` := @continuous _ _
variables f : ℝ × ℝ → ℝ × ℝ
#check cont t1 t2 f
Patrick Massot (Dec 02 2020 at 08:23):
In the last line cont t1 t2 f
means f
is continuous from topology t1
(induced by metric structure m1
) to topology t2
(induced by metric structure m2
). Is this what you wanted (I still don't understand what you call "having a Wikipediastyle metric space" which wouldn't be covered by what you pointed out in mathlib).
Lars Ericson (Dec 02 2020 at 13:27):
@Patrick Massot, by "Wikipedia style", I mean the definition which is "A metric space is an ordered pair (M,d)
where M
is a set and d
is a metric on M
". The Wikipedia definition focuses on d and describes the properties that d
must have, when supplied with M
, so that the pair (M,d)
 two elements together, separate and distinct  comprises a metric space.
When I first looked at topology.metric_space.basic, the first line structure metric_space (α : Type u)
confused me, as a beginner, because it looked like M
, as α
, was the only thing being described, and that d
was implied from M
. So that would only give me one d
, the implied one.
Looking at it again, I see that α
is constrained to have a distance function. However, as a beginner, I don't see the mechanics of how I supply distinct d
for a given M
so I can build different metric spaces on the same M
. For example, suppose M=ℝ × ℝ
, the real plane. Now suppose I have three norms, AbsNorm(m)
, EuclidNorm(m)
and TaxiCabNorm(m)
, and I define d1(x,y)=AbsNorm(xy)
, d2(x,y)=EuclidNorm(xy)
and d3(x,y)=TaxiCabNorm(xy)
. There are x,y
such that d1
, d2
and d3
take on different values, so that sense S1=(M,d1)
and S2=(M,d2)
will be different metric spaces.
So in summary my happy place for this task is where I can state M
and d
separately and mechanically prove that (M,d)
taken together comprise a metric space.
Thank you for the reference to the LFTCM2020 videos. I will watch them and then come back to the chat afterwards if I am still confused.
Reid Barton (Dec 02 2020 at 13:34):
Lean (and math) is happiest with one instance per type, but you can write something like def euclid_norm_metric_space : metric_space M := [...]
.
Reid Barton (Dec 02 2020 at 13:34):
In this setting it would be better to read metric_space
as "metric".
Reid Barton (Dec 02 2020 at 13:36):
When we write variables {M : Type} [metric_space M]
, we read it as "Let M be a metric space", but the actual values of the type metric_space M
are metrics on M (or "metric space structures on M").
Patrick Massot (Dec 02 2020 at 14:54):
Lars, when you write $(M, d)$ on paper, you are hiding the fact that $d$ has to satisfy a bunch of conditions that appear nowhere in this notation. In mathlib we chose to package together $d$ and proofs of these condition in a term whose type is called metric_space M
.
Patrick Massot (Dec 02 2020 at 14:55):
If you want to package things even more and get a type whose terms will look like $(M, d)$ then you can write
def MetricSpace := Σ α, metric_space α
example : MetricSpace := ⟨ℝ, by apply_instance⟩
Patrick Massot (Dec 02 2020 at 14:55):
Here a term with type MetricSpace
will be a (dependent) pair where the first component is a type and the second one is a metric structure (distance + conditions) on it.
Patrick Massot (Dec 02 2020 at 14:57):
Reid, we shouldn't hide the fact that those type aliases tend to very easily confuse the Lean 3 elaborator. Anyway, we don't have enough information about what Lars actually wants to do to provide good advice.
Reid Barton (Dec 02 2020 at 15:18):
That's why I didn't suggest writing instance
s but def
s (although I guess it wasn't very clear because I assumed Lars already has a type M
on which to define these metrics).
Lars Ericson (Dec 02 2020 at 16:07):
@Reid Barton , in the Wikipedia style definition, the focus is on d
, and any type M
for which d: M × M→ ℝ
is defined and has the 3 desired properties will do. So I don't need to define a particular M
, I need to define the expectations of d
, which I did above. I may supply ℝ × ℝ
as an M
for a suitable metric d
.
@Patrick Massot what I want to do in this case is what I said: Make two instances of metric space, one for Euclidean distance and one for Taxicab distance. Just that. It's the same as if I wanted to reason about 3+2 or 1+9, it's two separate things and I want to explore each one separately.
My longer term goal is to fill out my "Straw Man Answer" to this StackExchange question: https://math.stackexchange.com/questions/3780089/extendingtheconceptofdistributionfunctiontoanytotallyorpartiallyorder/3782009
Lars Ericson (Dec 02 2020 at 16:08):
So in general if I have Normal distribution and Poisson distribution or Norm(1,3) or Norm(0,1), I want to be able to declare and reason about these distinct objects separately in a wellfounded way.
Lars Ericson (Dec 02 2020 at 16:11):
The possibility that my goal may not fit with the design of mathlib
is maybe hinted at in this comment: "Note that there are two ways of formalising the axiom that an arbitrary union of open sets is open: one could either ask that given a set of open sets, their union is open, or one could ask that given a function from some index set I to the set of open sets, the union of the values of the function is open. Mathlib goes for the first one."
Reid Barton (Dec 02 2020 at 16:11):
Just don't use the word instance
, and instead write def foo : metric_space (ℝ × ℝ) := ...
, def bar : metric_space (ℝ × ℝ) := ...
, etc
Yakov Pechersky (Dec 02 2020 at 16:12):
In this case, "make two instances of metric space" means make the two separate def
, and in later proofs, instead of saying
lemma something_about_my_metric [metric_space ℝ × ℝ] : ... := ...
you say
lemma something_about_my_metric (my_metric : metric_space ℝ × ℝ) : ... := ...
and you provide explicitly one of your def
s
Yakov Pechersky (Dec 02 2020 at 16:12):
Oh Reid said the same thing
Patrick Massot (Dec 02 2020 at 16:47):
And I already said it this morning, I even posted the corresponding code with only Prop sorries.
Yakov Pechersky (Dec 02 2020 at 16:52):
And Patrick, your sigma type example is precisely what the "any type M
" desiratum Lars is about. Thanks for sharing it  it's helped me understand better how sigma types are useful and where they're appropriate.
Kevin Buzzard (Dec 02 2020 at 16:58):
Is there a category of metric spaces?
Bhavik Mehta (Dec 02 2020 at 16:59):
Not in Lean as far as I know
Lars Ericson (Dec 02 2020 at 18:32):
@Patrick Massot thank you for the def m1
and m2
example. I am trying it out:
import data.real.basic topology.metric_space.basic
noncomputable theory
def m1 : metric_space (ℝ × ℝ) :=
{ dist := λ x y, max (abs (x.1  y.1)) (abs (x.2  y.2)),
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
variables a b : ℝ × ℝ
#check a  a : ℝ × ℝ
#check b  b : ℝ × ℝ
#check m1.dist  dist : ℝ × ℝ → ℝ × ℝ → ℝ
#check m1.dist a b
At the bottom the first 3 #check
s give me expected results. The 3rd #check
, to access and apply the metric, gives me the error
invalid field notation, function 'has_dist.dist' does not have explicit argument with type (has_dist ...)
What do I need to fix to apply the function?
Lars Ericson (Dec 02 2020 at 19:16):
Actually it looks like I can fix this by defining m1.dist
external to m1
:
import data.real.basic topology.metric_space.basic
noncomputable theory
def d1 : ℝ × ℝ → ℝ × ℝ → ℝ :=
λ x y, max (abs (x.1  y.1)) (abs (x.2  y.2))
def m1 : metric_space (ℝ × ℝ) :=
{ dist := d1,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
variables a b : ℝ × ℝ
#check a  a : ℝ × ℝ
#check b  b : ℝ × ℝ
#check m1.dist  dist : ℝ × ℝ → ℝ × ℝ → ℝ
#check m1.dist a b  ERROR
#check d1  d1 : ℝ × ℝ → ℝ × ℝ → ℝ
#check d1 a b  d1 a b : ℝ
Reid Barton (Dec 02 2020 at 19:17):
You can write @metric_space.dist
, some number of underscores, then m1
Kevin Buzzard (Dec 02 2020 at 19:19):
I was going to say that, but unknown identifier 'metric_space.dist'
.
Reid Barton (Dec 02 2020 at 19:20):
oh rip
Reid Barton (Dec 02 2020 at 19:20):
it's in a superclass, that makes it quite awkward
Reid Barton (Dec 02 2020 at 19:20):
wait no yes
Kevin Buzzard (Dec 02 2020 at 19:22):
To make matters worse, there's an instance of has_dist (ℝ × ℝ)
;)
Reid Barton (Dec 02 2020 at 19:23):
Anyways, I guess you already know that points in a metric space have a distanceso I'm not sure what you hope to gain from these #check
s
Lars Ericson (Dec 02 2020 at 20:02):
@Kevin Buzzard @Reid Barton I would rewrite the above example as follows, but it's full of errors:
import data.real.basic topology.metric_space.basic
noncomputable theory
universe u
def metric_signature : Π (α : Type u) := α → α → ℝ  ERROR
#check metric_signature  ERROR
constant M : ℝ × ℝ
#check metric_signature M  ERROR
def d : metric_signature M :=
λ x y, max (abs (x.1  y.1)) (abs (x.2  y.2))
def metric_space_instance : (M : Type) (d : metric_signature M ) : metric_space (M) :=  just wrong starting with : metric_space(M)
{ dist := d,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
In other words I want to make a version of metric_space(M)
called metric_space_instance M d
. Is this possible?
Reid Barton (Dec 02 2020 at 20:03):
I agree that it is full of errors
Lars Ericson (Dec 02 2020 at 23:42):
Fixed. This gives me the sense of the Wiki definition which is (M,d)
. I understand it's not mathlib
onic but at least it typechecks.
import data.real.basic topology.metric_space.basic
noncomputable theory
def metric_signature (α: Type) := α → α → ℝ
def metric_space_instance (M : Type) (d : metric_signature M ) : metric_space (M) :=
{ dist := d,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
def M : Type := ℝ × ℝ
def d_taxicab : metric_signature M :=
λ x y, (abs (x.1  y.1)) + (abs (x.2  y.2))
def d_euclid : metric_signature M :=
λ x y, real.sqrt ((x.1  y.1)^2 + (x.2  y.2)^2),
def S_taxicab := metric_space_instance M d_taxicab
def S_euclid:= metric_space_instance M d_euclid
#check S_taxicab  S_taxicab : metric_space M
#check S_euclid  S_euclid : metric_space M
Yakov Pechersky (Dec 02 2020 at 23:52):
How do you plan to use these? How do you know that they're valid? Because this also typechecks:
import data.real.basic topology.metric_space.basic
noncomputable theory
def metric_signature (α: Type) := α → α → ℝ
def metric_space_instance (M : Type) (d : metric_signature M ) : metric_space (M) :=
{ dist := d,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }
notation `M` := ℝ × ℝ
def d_nonsensical : metric_signature M :=
λ x y, 1
def S_nonsensical : metric_space M := metric_space_instance M d_nonsensical
#check S_nonsensical  S_nonsensical : metric_space M
#exit
Lars Ericson (Dec 03 2020 at 00:44):
Thanks @Yakov Pechersky I take your point. The correctness of the metric
is in the axioms of metric_space
. Wikipedia only lists 3 properties and focusses on d
. metric_space
also focusses on d
internally and lists more than 3 axioms:
(dist_self : ∀ x : α, dist x x = 0)
(eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
(dist_comm : ∀ x y : α, dist x y = dist y x)
(dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
(edist : α → α → ennreal := λx y, ennreal.of_real (dist x y))
(edist_dist : ∀ x y : α, edist x y = ennreal.of_real (dist x y) . control_laws_tac)
(to_uniform_space : uniform_space α := uniform_space_of_dist dist dist_self dist_comm dist_triangle)
(uniformity_dist : 𝓤 α = ⨅ ε>0, 𝓟 {p:α×α  dist p.1 p.2 < ε} . control_laws_tac)
There are a bunch of sorry
s in metric_space_instance
so it's not really usable asis. I was really just trying to get at how Wikipedia presents the structure (M,d)
, not just M
with an assumed d
. There are a couple of directions I could go to Wikipediaify this more:
 Use
structure
 Make a
class
formetric
, whichmathlib
doesn't, and put the focus ond
.
In the long run for the project I am doing, I have a long stack of definitions I need to assemble, namely:
 Inhabited set
 Sample space: inhabited set
 Algebra
 σalgebra
 Event space A
 Family of sets A
 Σ(A) the sigma algebra generated by a family of sets A
 σadditive function
 Topological space
 Homeomorphism
 Separable topological space
 Metric
 Metric space
 Open set U on a metric space
 Open sets O(F) of a family F
 Closed set X on a metric space
 Clopen set
ℝ
 Real closed/open intervals
[a,b]
,(a,b)
,[a,b)
,(a,b]
,(0,1)
,[0,1]
,[0,∞)
.  Real metric
dR: ℝ × ℝ → [0,∞)
 Borel σalgebra
B(M)
of metric space(M,d)
 Borel σalgebra
B(ℝ)
 Borel σalgebra
B((a,b))
fora b : ℝ
 Borel set
X ∈ B(M)
of metric space(M,d)
 Finite Borel measure
μ: B(M) → [0,∞)
of metric space(M,d)
 Borel probability measure
μ: B(M) → [0,1]
 Diameter
diam(X)
forX ⊆ M
of metric space(M,d)
 Cauchycomplete metric space
 Measure
μ: A→ [0,∞)
 Measurable space
(S,Σ)
 Measurable function
f
 Pullback
f⁻¹: Σ → A
 Pushforward measure
f(μ): T → [0,∞)
 Measure space
(S,Σ,μ)
 Finite measure
p: A→[0,∞)
 Lebesgue σalgebra
L(ℝ)
 Lebesgue outer measure
λ⋆ : L(ℝ) → [0,∞)
 Lebesgue measure
λ : L(ℝ) → [0,∞)
 Polish measurable space
 Probability measure
p: Σ → [0,1]
 Probability space
(Ω,A,P)
 Random variable
(Ω,A,P)→(S,Σ)
from probability space to measure space  Distribution
μ_X : Σ → [0,1]
 Distribution space
(S,Σ ,μ_X )
 Distribution function
F_X: ℝ→ [0,1]
 Quantile function
T:[0,1]→ ereal
of functionT:ℝ→ [0,1]
maybe a/k/a inverse distribution functionF^X
of distribution functionF_X
 Real distribution space
(ℝ, B(ℝ), μ_x, F_X)
from distributionμ_x
on realvalued random variable on(Ω,A,P)
 Steinhaus space
 Discrete random variable
 Continuous random variable
 Continuous random variable density function
 Uniform continuous random variable
 Exponential continuous random variable
 Normal continuous random variable
 Construction of i.i.d random sequences from individual numbers in
ℝ
 Stochastic kernel
 Almost surely
 Version
 Transition kernel
 Transition probability kernel
 Regular version
 Conditional expectation
 Stochastic process
Yakov Pechersky (Dec 03 2020 at 00:51):
You could try to build up your theory for R^n
first
Eric Wieser (Dec 03 2020 at 00:56):
Are you looking for docs#premetric_space, which has fewer fields?
Yakov Pechersky (Dec 03 2020 at 00:59):
Also, mathlib has a some of what you indicated, like intervals, Borel measure
Lars Ericson (Dec 03 2020 at 01:10):
@Eric Wieser I would like to use everything already defined in mathlib
but where the literature I'm reading expresses a metric space as a structure (M,d)
or a probability space as a structure (Ω,A,P)
, I want to keep that style of definition. I also want to learn how to make classes of functions. In the case of metric_space
, the class is "about" theM
in the metric space structure (M,d)
. I want to understand how to, instead, make a class which is "about" the function d
. Similarly if I describe the Gaussian probability distribution, I want to be able to talk about Gaussian random variables, which are functions from probability space to measure space. I want to be able to construct and talk about Gaussian RV, Normal RV and so on.
I've got 3 higherlevel goals:

Typically the notion of
(Ω,A,P)
is invoked and then forgotten about when talking about probability distributions. I had a long back and forth about this on Stack Exchange. I was looking for "the" canonical probability space underlying continuous distributions on the reals. The feedback I got was that you can "carry" continuous RVs like uniform, Gaussian and so on a lot of different ways, the simplest one being the Steinhaus space. Once you know you can carry them all with many or with that one, the topic becomes boring for most people, because the probability space just acts as a kind of index set into the event space. One index set is as good as another as long as it spans the space. Nevertheless, I wanted to make it more concrete in the Lean sense of having a correct stack of types and stating and supporting axioms and theorems about the construction. 
I noticed along the way that the idea of a distribution function, typically only defined for the reals, should probably extend to any measurable space. So, another Stack Exchange question. Nobody cares about this. I just thought it was interesting. I thought it would be interesting to see if, building up the machinery in a provably correct way in Lean, I could show that indeed the idea of a distribution function naturally extends to any measurable space, it doesn't just have to be on the reals.

The bigger challenge is to formalize the definitions leading up to a Wiener stochastic process and the definition of Ito and Stratonovich integrals. This is probably a lot harder. However the answers to my Stack Exchange question on probability space went there and sketched it out. So maybe it's not that hard. That would also be interesting to do.
Lars Ericson (Dec 03 2020 at 01:13):
premetric_space
has 3 axioms but it's a different 3 axioms from the Wikipedia presentation for metric space. https://en.wikipedia.org/wiki/Metric_(mathematics)#Premetrics
Johan Commelin (Dec 03 2020 at 05:32):
Lars Ericson said:
Eric Wieser I would like to use everything already defined in
mathlib
but where the literature I'm reading expresses a metric space as a structure(M,d)
or a probability space as a structure(Ω,A,P)
, I want to keep that style of definition.
I think you might be making your life very hard. Sometimes there are very good reasons for formal libraries to deviate from the standard definitions in maths literature. The reason that mathlib includes the topology/uniformity in the definition of a metric space, is because otherwise you'll infer two topologies on a product metric space, and Lean can't tell they are equal. These are the kind of implementation details where you have to "be like water" (as Bruce Lee said). If you start fighting the system, life will become very hard.
Lars Ericson (Dec 03 2020 at 06:09):
@Johan Commelin I'm not trying to fight the system. At my beginner skill level, I find it easier to understand axiomatic definitions that say X is a thing comprised of these specific parts which follow this list of axioms. In that spirit, if you look at this old definition of σalgebra from 2017:
variables {X : Type} (σ : set (set X))
class sigma_algebra :=
(univ_mem : univ ∈ σ)
(closed_under_comp : ∀ s, s ∈ σ → univ \ s ∈ σ)
(closed_under_countable_union : ∀ f : ℕ → set X, (∀ n, f n ∈ σ) → countable_union f ∈ σ)
it is more like that. Today, if I look for σalgebra in mathlib
, what I find is that σalgebra
exists 19 times in the comments, and 0 times in the code:
...
σalgebras on a fixed set `α` form a complete lattice. Here we order
σalgebras by writing `m₁ ≤ m₂` if every set which is `m₁`measurable is
also `m₂`measurable (that is, `m₁` is a subset of `m₂`). In particular, any
collection of subsets of `α` generates a smallest σalgebra which
contains all of them. A function `f : α → β` induces a Galois connection
between the lattices of σalgebras on `α` and `β`.
...
I am a programmer, not a mathematician. It is frustrating for me not to be able to be able to be able to build a specific object of type σalgebra
, when σalgebra
is one of the central building blocks of the theory I am trying to encode in Lean. I find it a lot harder to learn or even apply a piece of code where the building blocks I want to pick up and put down exist only very implicitly in a structure which focuses at the top level on representing one major idea, like measurable space, while at the same time relegating explicit mention of a subsidiary idea like σalgebra to the comments.
I am happier when I can constructively engage with each of the components in the stack that I listed above in an individual sense on the component's own terms. I want to be able to play with σalgebras explicitly on their own terms before seeing them subsumed as purely implicit features of larger structures. That is, I want to be able to stop and understand each building block idea on it's own terms as I go along, and then see that building block idea explicitly expressed in the construction of the next idea. However, based on the 2017/2020 comparison, it seems that as the code evolves, the major ideas get a lot more implicit structure packed into them and factored out in somewhat novel ways (compared to the Wikipedia presentation). I guess this is to achieve higher levels of generality or categorization in the design. However, that more general/categorical breakdown makes it harder to see the old trees from the old forest.
I understand that in a sense you are discovering less ambiguous and more rigorous ways of presenting mathematical ideas than exist in the "standard definitions". To that extent you should be maybe pushing for changes in the standard usage, so that the standard presentation conforms more to the way things are factored out in Lean than the way they have been presented in the past.
One kind of "activist" way to do that would be to go into Wikipedia and simply change or augment the definitions you see in Wikipedia to fit the way ideas are newly presented in mathlib
. This is a reasonable suggestion because
 Anybody can edit Wikipedia
 You are a family member of Wikipedia in the sense that lines 53 to 57 of the
mathlib
code formeasurable_space
look like this:
## References
* <https://en.wikipedia.org/wiki/Measurable_space>
* <https://en.wikipedia.org/wiki/Sigmaalgebra>
* <https://en.wikipedia.org/wiki/Dynkin_system>
Thomas Browning (Dec 03 2020 at 06:35):
Lars Ericson said:
To that extent you should be maybe pushing for changes in the standard usage, so that the standard presentation conforms more to the way things are factored out in Lean than the way they have been presented in the past.
I don't necessarily think so. Take the issue of filters for example. I'm not super familiar with Lean's real analysis library, but I think that a lot of stuff (e.g., limits) is done using filters. In the context of formalizing mathematics, filters are a great way to go. In the context of learning limits for the first time, filters are a terrible way to go. I think that a lot of freshmen calculus students would get very mad if we rewrote the Wikipedia limits page in terms of filters.
Lars Ericson (Dec 03 2020 at 14:38):
@Thomas Browning that's not what I'm saying. I love simple axiomatic definitions like the ones you usually see for group, and ring. However, while looking at probability space definitions in various course notes on the Internet, I discovered that those simple, clear cut, building block style definitions are the exception, not the rule, in mathematics and not just in mathlib
. So maybe 1% of math is presented that way, and the other 99% at the professional mathematician level is presented by a shifting and evolving set of alternative expressions. For example, consider Stone space in Wikipedia. It doesn't have one definition, it has 4:
 X is homeomorphic to the projective limit (in the category of topological spaces) of an inverse system of finite discrete spaces;
 X is compact and totally separated;
 X is compact, T0 , and zerodimensional (in the sense of the small inductive dimension);
 X is coherent and Hausdorff.
Also, if you look at the history of probability theory, it was a century long slugfest where mathematicians constantly fought over how to express things and what to focus on. You can see the blowbyblow in The origins and legacy of Kolmogorov's Grundbegriffe. Math changes all the time.
Regarding undergraduates getting annoyed if you changed a definition in Wikipedia: Don't worry about it. I have gotten hammered in Zulip for making broad untestable assertions about large populations, but I will go ahead and do it again: There is no undergraduate on the planet who is motivated to study metric spaces who will be bothered if you add an alternate presentation of metric spaces as a section in the Wikipedia page. I have been a Wikipedia editor since 2008. Wikipedia can also be quite contentious. If you make an edit on the Metric Space page and you find that it leads to enormous controversy, I will come and defend you. However, I will make another prediction: Nobody will notice. On Wikipedia, the kind of page that will attract the most serious, sustained and concentrated attention is this one. Metric space, no so much.
Eric Wieser (Dec 03 2020 at 14:46):
Lars Ericson said:
In that spirit, if you look at this old definition of σalgebra from 2017:
variables {X : Type} (σ : set (set X)) class sigma_algebra := (univ_mem : univ ∈ σ) (closed_under_comp : ∀ s, s ∈ σ → univ \ s ∈ σ) (closed_under_countable_union : ∀ f : ℕ → set X, (∀ n, f n ∈ σ) → countable_union f ∈ σ)
it is more like that. Today, if I look for σalgebra in
mathlib
, what I find is thatσalgebra
exists 19 times in the comments, and 0 times in the code
If you look at measurable_space
, you'll see it's almost exactly this definition, just under a different name:
structure measurable_space (α : Type*) :=
(is_measurable' : set α → Prop)
(is_measurable_empty : is_measurable' ∅)
(is_measurable_compl : ∀ s, is_measurable' s → is_measurable' sᶜ)
(is_measurable_Union : ∀ f : ℕ → set α, (∀ i, is_measurable' (f i)) → is_measurable' (⋃ i, f i))
Remember that in lean, σ : set (set α)
and is_measurable' : set α → Prop
are definitionally equal, and so are s ∈ σ
and is_measurable' s
.
Lars Ericson (Dec 03 2020 at 20:35):
Thank you @Eric Wieser. Translating these finite measurable space examples using mathlib
will really help me understand how to use the library: Given X={1,2,3}
, two instances of σalgebra are A1={X,∅}
and A2=P(X)
. I don't know how to make a particular finite set in Lean. This is not discussed in TPIL. Logic and Proof doesn't have a finite set example. I need to do the following steps:
 Make
X = {1,2,3}
 Make
A1 = {X, ∅}
 Make
A2 = set.powerset(X)
 Prove that
measurable_space A1
andmeasurable_space A2
Is this possible? I don't know how to do this.
Lars Ericson (Dec 03 2020 at 21:13):
Actually for X={1,2,3}
I have a solution.
I was concerned about getting a "true set
" and not a "setlike object" that might not fit with measurable_space
.
I found the docs. This seems like a back door (only fits my example) but it gets me there:
def S : set ℕ := {n : ℕ  0 < n ∧ n ≤ 3}
Yakov Pechersky (Dec 03 2020 at 21:23):
import data.finset.basic
#check ({1, 2, 3} : finset ℕ)
Lars Ericson (Dec 03 2020 at 21:26):
Thanks @Yakov Pechersky will finset
unify with set
? This is needed to apply to measurable_space
. For example, this does not work:
import data.finset.basic
def S : set ℕ := ({1, 2, 3} : finset ℕ)  type error here and no automatic coercion
#check S
Also how do I prove set membership. For example according to the definition of ∈ , this should work, but does not:
def S : set ℕ := {n : ℕ  0 < n ∧ n ≤ 3}
example : 1 ∈ S :=
begin
exact S 1,
end
It fails with error
invalid type ascription, term has type
Prop : Type
but is expected to have type
1 ∈ S : Prop
state:
⊢ 1 ∈ S
I am a little fuzzy about the status of my definition S
.
Yakov Pechersky (Dec 03 2020 at 21:30):
import data.finset.basic
import tactic.dec_trivial
def S : set ℕ := {n : ℕ  0 < n ∧ n ≤ 3}
example : 1 ∈ S := set.left_mem_Icc.mpr (show 1 ≤ 3, from dec_trivial)
Yakov Pechersky (Dec 03 2020 at 21:32):
I don't have a type error for your
import data.finset.basic
def S : set ℕ := ({1, 2, 3} : finset ℕ)
#check S
Yakov Pechersky (Dec 03 2020 at 21:36):
import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
def A1 : set (set ℕ) := {X, ⊤}
def A2 : set (set ℕ) := set.powerset X
#reduce X
#reduce A1
#reduce A2
Mario Carneiro (Dec 03 2020 at 21:37):
Lars Ericson said:
Thank you Eric Wieser. Translating these finite measurable space examples using
mathlib
will really help me understand how to use the library: GivenX={1,2,3}
, two instances of σalgebra areA1={X,∅}
andA2=P(X)
. I don't know how to make a particular finite set in Lean. This is not discussed in TPIL. Logic and Proof doesn't have a finite set example. I need to do the following steps:
 Make
X = {1,2,3}
 Make
A1 = {X, ∅}
 Make
A2 = set.powerset(X)
 Prove that
measurable_space A1
andmeasurable_space A2
Is this possible? I don't know how to do this.
The easiest way to prove specific theorems is to generalize them to something that doesn't have the "example" flavor. Under what assumptions does this theorem hold?
Lars Ericson (Dec 03 2020 at 21:38):
Thank you @Yakov Pechersky ! This works on Lean Community Web Editor:
import data.finset.basic
import measure_theory.measurable_space
def S : set ℕ := ({1, 2, 3} : finset ℕ)
#check S
#check measurable_space S
When I try it on my local VS Code copy of Lean, installed yesterday, I get this:
Screenshotfrom20201203163834.png
Lars Ericson (Dec 03 2020 at 21:41):
@Yakov Pechersky @Mario Carneiro is it correct to say that if #check doesn't complain, then A1 and A2 have been proven to be measurable spaces, just by passing the typecheck?
import data.finset.basic
import measure_theory.measurable_space
def X : set ℕ := ({1, 2, 3} : finset ℕ)
def A1 : set (set ℕ) := {X, ⊤}
def A2 : set (set ℕ) := set.powerset X
#check measurable_space A1
#check measurable_space A2
Mario Carneiro (Dec 03 2020 at 21:41):
no
Mario Carneiro (Dec 03 2020 at 21:42):
a proof would be #check (by apply_instance : measurable_space A1)
Mario Carneiro (Dec 03 2020 at 21:42):
all that typechecking the statement does is ensure that A1
can be treated as a type
Lars Ericson (Dec 03 2020 at 21:43):
Thanks. Then not quite done yet because that yields
tactic.mk_instance failed to generate instance for
measurable_space ↥A1
state:
⊢ measurable_space ↥A1
even though it passes the type check.
Mario Carneiro (Dec 03 2020 at 21:43):
yes, there's a big difference between stating a theorem and proving it!
Yakov Pechersky (Dec 03 2020 at 21:44):
Oh btw I have a typo, I used \top
, which is set.univ
instead of \bot
, which is the empty set
Alex J. Best (Dec 03 2020 at 21:46):
The last part requires a bit more proof, like mario says though, A1 and A2 giving the measurable sets of a measurable space doesn't really require the base type to be fin 3
def X:Type := fin 3
def A1 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def A2 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
instance : measurable_space X :=
{ is_measurable' := A1,
is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp,sorry },
Alex J. Best (Dec 03 2020 at 21:47):
The A2 version is easier
instance meas2 : measurable_space X :=
{ is_measurable' := A2,
is_measurable_empty := by {rw A2, finish},
is_measurable_compl := assume a h, by {rw A2 at *, finish},
is_measurable_Union := assume f hf, by {rw A2 at *, simp, }, }
Mario Carneiro (Dec 03 2020 at 21:47):
it would be nice to prove these by proving roughly (⊥ : measurable_space X) = A1
Alex J. Best (Dec 03 2020 at 21:47):
These are not efficient proofs, I'm just using tactic#finish which can solve a lot of goals automatically to avoid thinking about what's needed too hard here.
Mario Carneiro (Dec 03 2020 at 21:48):
there is docs#measurable_space.is_measurable_bot_iff but there is still some unwrapping to get the pair formulation
Lars Ericson (Dec 03 2020 at 21:50):
Thank you @Yakov Pechersky @Alex J. Best @Mario Carneiro this now gives a very clear guide for how to use mathlib
.
Lars Ericson (Dec 03 2020 at 21:58):
In looking at this today I found these slides by Sylvie Boldo on Lebesgue integration in Coq. Is it fair to say that mathlib
at a same level of development for Lebesgue integral? In particular she proved a few theorems Fatou_Lebesgue
, LInt_p_plus
and LInt_p_with_adapted_seq
and I was wondering if you have those defined in Lebesgue integral
Lars Ericson (Dec 03 2020 at 22:09):
@Thomas Browning on the changing story of math, I came across this picture today in Wikipedia: 1024pxMagma_to_group4.svg.png
mathlib
has magma
. I'd never heard of it before today. It's not in Mac Lane and Birkhoff. The term was coined in 1965. Saunders Mac Lane did not take notice. So that's a concrete example of terminology and methodology shifts in mathematics. Which is evidence for the idea that if mathlib
has a different factoring and terminology for the underlying "state of nature" which you think is a better way of presenting that state of nature, you should really feel free to go ahead and explain things that way in Wikipedia.
Yakov Pechersky (Dec 03 2020 at 22:12):
https://ncatlab.org/nlab/show/measurable+space
Alex J. Best (Dec 03 2020 at 22:12):
magma
in mathlib would just be has_mul
a binary operation with no axioms
Alex J. Best (Dec 03 2020 at 22:15):
Then the arrows in your picture are instances in lean like, docs#semigroup.to_has_mul, docs#monoid.to_semigroup, docs#group.to_monoid
Yakov Pechersky (Dec 03 2020 at 22:15):
Wikipedia is not the only place to find references and descriptions of terms, but is just meant to be an easy reference with links to more indepth explanations. nLab is one such more indepth reference.
Lars Ericson (Dec 03 2020 at 22:23):
@Yakov Pechersky it might be best practice to replace Wikipedia references in the mathlib
source with nLab pages.
Mario Carneiro (Dec 03 2020 at 22:34):
magmas are popular in France I believe, because Bourbaki liked it
Mario Carneiro (Dec 03 2020 at 22:35):
Lars Ericson said:
Yakov Pechersky it might be best practice to replace Wikipedia references in the
mathlib
source with nLab pages.
No, I don't think so. nLab has a tendency for being inscrutable to nonexperts
Mario Carneiro (Dec 03 2020 at 22:36):
wikipedia is much more appropriate for linking to core concepts in an undergraduate curriculum
Mario Carneiro (Dec 03 2020 at 22:38):
Also all the constructive detours in nLab are quite irrelevant for mathlib
Adam Topaz (Dec 03 2020 at 22:45):
Mario Carneiro said:
No, I don't think so. nLab has a tendency for being inscrutable to nonexperts
Sometimes also for experts...
Lars Ericson (Dec 04 2020 at 15:26):
Suppose that the proofs for A1 and A2 happened to be identical. (I know that that may not be the case here, it is a hypothetical.) If so, what is the proper Lean syntax and style to do something like this:
def ms_proof (X: Type) (A: set X → Prop) :=
{ is_measurable' := A1,
is_measurable_empty := by { rw A1, finish } ,
is_measurable_compl := assume a h, by { rw A1 at *, sorry, },
is_measurable_Union := assume f hf, by { rw A1 at *, sorry, },
}
instance M1 : measurable_space X := ms_proof X A1
instance M2 : measurable_space X := ms_proof X A2
Mario Carneiro (Dec 04 2020 at 15:27):
that depends on what kind of identical you mean
Mario Carneiro (Dec 04 2020 at 15:27):
if they are defeq you can just reuse the proof
Mario Carneiro (Dec 04 2020 at 15:28):
if they are textually the same but are actually proving different things you can usually use a tactic
Mario Carneiro (Dec 04 2020 at 15:30):
but it's also possible for an example like this one that there is simply a generalization to be had, where you prove a general theorem and just instantiate it twice. This is preferable if you can do it, reserving the tactic approach for proofs that are very significantly different and only look similar because the same automation is used (e.g. there are many theorems about complexes proved by ext; simp
which have nothing to do with one another despite sharing the same proof text)
Lars Ericson (Dec 04 2020 at 15:43):
@Mario Carneiro I'm supposing that I have a general theorem and I'm instantiating it twice. However, syntactically, I don't think I'm proving a theorem in this case, I am building a structure. measurable_space
is a structure with 4 fields. I am guessing that the body of the instance assignment:
instance M1 : measurable_space X := body
has to evaluate to a measurable_space
structure with 4 fields. I don't know if that is a correct understanding of the type of body
. If so, then I should be able to say
def ms_proof (X: Type) (A: set X → Prop) : measurable_space X :=
{ is_measurable' := A1,
is_measurable_empty := by { rw A1, finish } ,
is_measurable_compl := assume a h, by { rw A1 at *, sorry, },
is_measurable_Union := assume f hf, by { rw A1 at *, sorry, },
}
However Lean is throwing up a bunch of errors when I do this:
Screenshotfrom20201204104144.png
Hence the question, what is the right way to do this so that I get significant reuse of code but the purpose of the code is to instantiate a structure with 4 fields.
Mario Carneiro (Dec 04 2020 at 15:47):
Shouldn't you be using A
instead of A1
? Lean is complaining that A1
is a function on the wrong type, the def X := fin 3
rather than the variable (X : Type)
in the theorem
Mario Carneiro (Dec 04 2020 at 15:48):
there isn't a really big difference between theorems and definitions in lean, the syntax is exactly the same except for the initial keyword
Mario Carneiro (Dec 04 2020 at 15:49):
Your two instances M1
and M2
are a bad idea btw because instances are supposed to be unique per type
Mario Carneiro (Dec 04 2020 at 15:50):
you can make them a def
instead if you want to prove the theorem without making it the canonical measurable space on X
Lars Ericson (Dec 04 2020 at 15:51):
Thank you @Mario Carneiro removing that typo this works:
def ms_proof (X: Type) (A: set X → Prop) : measurable_space X :=
{ is_measurable' := A,
is_measurable_empty := by sorry ,
is_measurable_compl := by sorry ,
is_measurable_Union := by sorry ,
}
instance M1 : measurable_space X := ms_proof X A1
instance M2 : measurable_space X := ms_proof X A2
If I change the def
to theorem
I get a message at the instance
lines
failed to generate bytecode for 'M1'
code generation failed, VM does not have code for 'ms_proof'
Lars Ericson (Dec 04 2020 at 15:53):
For this particular example the proofs will probably end up being different. I was just curious what the right way was in case the proofs were the same. However, even if the proofs are the same, the underlying sigma algebras are different by construction, so I want to call them different instances of measurable_space
, even if the proof happens to go the same for the different sigma algebras. Either that or I'm misunderstanding what instance
is supposed to represent, other than "an instance".
Mario Carneiro (Dec 04 2020 at 16:01):
An instance should usually be a def
rather than a theorem
. The general rule is: if you are "constructing data", more specifically if the type that you are constructing is not a Prop
(in this case measurable_space X : Type
), then it should be def
, otherwise theorem
Mario Carneiro (Dec 04 2020 at 16:01):
if you don't follow this rule you get the "code generation failed" error
Mario Carneiro (Dec 04 2020 at 16:03):
What you are describing, that there are multiple nonequivalent members of measurable_space X
, is what def
is about
Mario Carneiro (Dec 04 2020 at 16:04):
instance
is for when the type, even if it is not literally a singleton, nevertheless has a "canonical element": for example the collection of all field structures on the reals is very far from a singleton yet when people use the reals as a field they really only mean one field structure, and instance
encodes that "canonical choice" of structure. You can't have two canonical choices for the same type
Mario Carneiro (Dec 04 2020 at 16:06):
In the case of measurable_space X
, there is no canonical measurable space in general, even though there are two generically definable measurable spaces, top and bottom
Lars Ericson (Dec 04 2020 at 16:06):
Each of the components is actually a theorem that the given set satisfies the required properties. So taken together it's 4 proofs. If they happen to be the same proof for two different sets then it seems like I am defining a category. Is that overstating the case? Again, hypothetical on the proofs requiring the same set of tactics (even if the tactics like finish
resolve to different sequences "under the hood").
Mario Carneiro (Dec 04 2020 at 16:06):
For measurable_space real
, you could take the set of lebesgue measurable sets as canonical, or perhaps the borel measurable sets
Mario Carneiro (Dec 04 2020 at 16:07):
It's not a category in the mathematical sense, it's just a general theorem
Mario Carneiro (Dec 04 2020 at 16:07):
or def
I should say
Lars Ericson (Dec 04 2020 at 16:14):
A1
and A2
are different sets, so ms_proof X A1
and ms_proof X A2
are proofs about two different measurable spaces. Even though X
is the same, the sigma algebras are different. In Wikipedia style, the measurable spaces are (X,A1)
and (X,A2)
. This is two different spaces. Maybe in NCat style, X
is the measurable space and A1
and A2
are sigma algebras that it has. However, if that were the case, then I should have a structure sigma_algebra
so that I can distingiush A1
and A2
as instances of sigma_algebra
. But that is not the mathlib
design. So given the design, I should really be comfortable using instance
for M1
and M2
.
Eric Wieser (Dec 04 2020 at 16:17):
It's not clear how to plan to proceed without those sorry
s filled out
Eric Wieser (Dec 04 2020 at 16:17):
Because right now, they're impossible to fill
Eric Wieser (Dec 04 2020 at 16:22):
Your current statement is "every set of sets on X is a measure", but that's not true
Mario Carneiro (Dec 04 2020 at 16:25):
I should have a structure sigma_algebra so that I can distingiush A1 and A2 as instances of sigma_algebra.
sigma_algebra
in mathlib is spelled measurable_space
Mario Carneiro (Dec 04 2020 at 16:26):
We already have proofs that \top : measurable_space X
and \bot : measurable_space X
, I think that covers your use cases already
Yakov Pechersky (Dec 04 2020 at 16:28):
I think an issue here is one should not read instance
as "instance" in the sense that "this term is a single possible instance of this type". Instead instance
means "infer this instantiation of this type for ALL mentions of this type".
Lars Ericson (Dec 04 2020 at 16:49):
@Yakov Pechersky thanks I will use def
in preference to instance
wherever possible.
@Eric Wieser I stated that I was exploring the hypothetical of a situation where the proofs for A1 and A2 happened to be the same. In which case I was looking for a way to factor code for identical structure proofsofcorrectness (each structure component is a proof). I understand that these are not the same proof. Also though there is the ambiguous case where a tactic like simp
or finish
works but if you looked at the expanded sequence, these tactics found different proofs at a finegrained level.
In the case of these A1 and A2, the proof of A2 has a sorry
in is_measurable_Union
. Otherwise they would be textually the same proof.
Lars Ericson (Dec 04 2020 at 16:58):
@Mario Carneiro I get that sigma_algebra
in mathlib
is spelled measurable_space
. However measurable_space
only takes the "carrier set" X
as an explicit argument. The sigma algebra that it verifies is there as the proof that X
is is_measurable'
. If I were to look at two different objects M
that had type measurable_space X
, I would not know if they were "about" A1
or "about" A2
. If the rest of what I do depends on whether I have A1
or A2
underneath, then I am going to want to know that I proved the measurable_space
of X
for that A1 or A2.
Mario Carneiro (Dec 04 2020 at 17:00):
It is the type of all sigma algebras
Mario Carneiro (Dec 04 2020 at 17:01):
an element of that type is a sigma algebra. You can tell which one it is because you have an element of the type, in the same way that you can tell the difference between 1 : real
and 4 : real
even thoughthey have the same type
Yakov Pechersky (Dec 04 2020 at 17:01):
lemma something_about_A1 {X : Type} (sigma : measurable_space X) (h : sigma.is_measurable' = A1) : ... := ...
?
Lars Ericson (Dec 04 2020 at 17:06):
@Mario Carneiro in probability theory A1
and A2
would represent two different event spaces with different granularity. Propositions about one event space may not be equally valid on a differently constructed event space. So really 1: (X,A1)
and 1:(X,A2)
are not the same thing at all.
Mario Carneiro (Dec 04 2020 at 18:55):
What does 1: (X,A1)
mean? (X, A1)
is not a type, it is a sigma algebra. Is 1
supposed to represent a measurable set?
Mario Carneiro (Dec 04 2020 at 18:57):
The idea here is that the elements of measurable_space X
are themselves objects that you can manipulate, like what you have written (X, A1)
. For example you can prove (\bot : measurable_space X) <= \top
, or @is_measurable X \bot A > @is_measurable X \top A
and other things like that
Lars Ericson (Dec 04 2020 at 19:37):
@Mario Carneiro I was abusing notation there. You were talking about 1: real
and 2: real
and real is real. I am thinking of sigma algebras as event spaces for a probability space. I was just trying to express, notationally, that X with A1 and X with A2 are not the same. Depending on the granularity of the event space you can either discern or not discern more or less about the outcome. This means that what you can assert and compute the probability of is different for different sigma algebras. Clearly A1 and A2 are different sigma algebras . I need to be able to talk about them individually. That's not easy in the current setup.
Also as it turns out the proof of X with A1 is different from the proof of X with A2. We don't really have a proof of X with A1 in the sketch by @Alex J. Best , there is a sorry
in the is_measurable_Union
:
def X:Type := fin 3
def A1 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def A2 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
instance : measurable_space X :=
{ is_measurable' := A1,
is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp, sorry },
So the two spaces X
with A1
and X
with A2
are different both in how they are proven to be measurable spaces and in what, as event spaces, the sigma algebras A1
and A2
allow you to express.
Also, consider how mathlib
describes the situation: "A measurable space is a set equipped with a σalgebra, a collection of subsets closed under complementation and countable union. " A set. Equipped with a σalgebra. Two different things. Taken together, they make a 3rd thing. However, the way the "API" of measurable_space
is presented, it is hard to distinguish the presence of the second thing. It's like saying a pair (a,b)
has two parts a
and b
, but all pairs starting with a
are isomorphic in some sense, so we'll prioritize the a
and bury the b
, and whenever we print the pair (a,b)
, we are only going to print (a,...)
. I'm sorry, I just don't get it. Clearly it is elegant to people who have more insight and training than I do. I accept that. But for me, I just don't get it. It's OK that I don't get it. Don't worry about it. But I don't get it.
Mario Carneiro (Dec 04 2020 at 19:38):
The b
is only buried if you want it to be
Mario Carneiro (Dec 04 2020 at 19:38):
like I've been saying, measurable_space X
is a type, that has elements, that you can use in expressions
Mario Carneiro (Dec 04 2020 at 19:39):
you don't have to always use them as instances
Mario Carneiro (Dec 04 2020 at 19:40):
it's like this: (a : Type) (b : measurable_space a)
, see no burying
Mario Carneiro (Dec 04 2020 at 19:41):
The reason measurable_space
is a class is because it is also common to want to fix a measure space or probability space X
when talking about this stuff
Mario Carneiro (Dec 04 2020 at 19:43):
The proof of the theorems you are talking about in mathlib are done like this:
instance : complete_lattice (measurable_space α) :=
gi_generate_from.lift_complete_lattice
lemma is_measurable_bot_iff {s : set α} : @is_measurable α ⊥ s ↔ (s = ∅ ∨ s = univ) :=
let b : measurable_space α :=
{ is_measurable' := λ s, s = ∅ ∨ s = univ,
is_measurable_empty := or.inl rfl,
is_measurable_compl := by simp [or_imp_distrib] {contextual := tt},
is_measurable_Union := assume f hf, classical.by_cases
(assume h : ∃i, f i = univ,
let ⟨i, hi⟩ := h in
or.inr $ eq_univ_of_univ_subset $ hi ▸ le_supr f i)
(assume h : ¬ ∃i, f i = univ,
or.inl $ eq_empty_of_subset_empty $ Union_subset $ assume i,
(hf i).elim (by simp {contextual := tt}) (assume hi, false.elim $ h ⟨i, hi⟩)) } in
have b = ⊥, from bot_unique $ assume s hs,
hs.elim (λ s, s.symm ▸ @is_measurable_empty _ ⊥) (λ s, s.symm ▸ @is_measurable.univ _ ⊥),
this ▸ iff.rfl
@[simp] theorem is_measurable_top {s : set α} : @is_measurable _ ⊤ s := trivial
Mario Carneiro (Dec 04 2020 at 19:45):
Here we are starting from a much more powerful fact, that the space of all sigma algebras is a complete lattice, which immediately gives us Sup
, Inf
, sup
, inf
, top
and bot
Mario Carneiro (Dec 04 2020 at 19:45):
and then we prove post hoc that the top
and bot
so defined are in fact univ
and {empty, univ}
respectively
Mario Carneiro (Dec 04 2020 at 19:55):
import data.finset.basic
import measure_theory.measurable_space
def X : Type := fin 3
def A1 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def A2 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
def measurable_space.copy {α} (c : measurable_space α)
(P : set α → Prop) (eq_P : ∀ s, P s ↔ @is_measurable _ c s) :
measurable_space α :=
begin
replace eq_P : P = c.is_measurable' := by ext; apply eq_P,
refine { is_measurable' := P, .. },
all_goals { abstract { subst_vars, casesI c, assumption } }
end
theorem measurable_space.copy_eq {α} (c P eq_P) :
@measurable_space.copy α c P eq_P = c :=
measurable_space.ext eq_P
def foo1 : measurable_space X :=
measurable_space.copy ⊥ A1 $
by simp [measurable_space.is_measurable_bot_iff, A1, eq_comm, or.comm]
def foo2 : measurable_space X :=
measurable_space.copy ⊤ A2 $ by simp [A2]
theorem foo1_eq : foo1 = ⊥ := measurable_space.copy_eq _ _ _
theorem foo2_eq : foo2 = ⊤ := measurable_space.copy_eq _ _ _
Lars Ericson (Dec 04 2020 at 20:17):
@Mario Carneiro thank you for being patient with me.
To move to the next part, we have
def X:Type := fin 3
def A1 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def A2 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
How do I get the size of an element of A1 or A2? Or even X
? When I look at the definition of fin N
, it is not clear that N
is retained:
def fin (n : ℕ) := {i : ℕ // i < n}
I want to be able to define a metric
on A1
which is just the size of the finite set. This is not correct but I'm trying to get here:
def SubSet (X: Type) := set X → Prop
def size (X: Type) (F: SubSet X) := sorry
def finite_set_measure_of(X: Type): SubSet X → ennreal := λ F, size X F
def M1_measure : measure M1 := finite_set_measure_of X
instance M1_MS : measure_space M1 :=
{ to_measurable_space := M1,
volume := M1_measure }
Mario Carneiro (Dec 04 2020 at 20:18):
That's not a metric, I guess you mean a measure
Mario Carneiro (Dec 04 2020 at 20:19):
the measure is called docs#measure_theory.measure.count in mathlib
Mario Carneiro (Dec 04 2020 at 20:20):
It is defined by (infinite) summing 1 over the set
Mario Carneiro (Dec 04 2020 at 20:21):
If you happen to know the set is finite you can use finset.card
to get the cardinality
Mario Carneiro (Dec 04 2020 at 20:22):
You can also use cardinal.mk
to get the cardinality of an infinite set but for measures you really just want this to cap out at infinity so the infinite sum on ennreal
is the easiest thing to implement
Mario Carneiro (Dec 04 2020 at 20:23):
the proof that fin n
has size n
is docs#fintype.card_fin
Mario Carneiro (Dec 04 2020 at 20:34):
You can do this, but it doesn't yield a very fun goal:
def M1 : measurable_space X :=
measurable_space.copy ⊥ A1 $
by simp [measurable_space.is_measurable_bot_iff, A1, eq_comm, or.comm]
def M2 : measurable_space X :=
measurable_space.copy ⊤ A2 $ by simp [A2]
theorem M1_eq : M1 = ⊥ := measurable_space.copy_eq _ _ _
theorem M2_eq : M2 = ⊤ := measurable_space.copy_eq _ _ _
instance : fintype X := fin.fintype _
noncomputable instance foo (s : set X) : fintype s := by classical; apply_instance
noncomputable def M1_measure : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
(λ s _, finset.card s.to_finset)
(by simp)
(λ x h a, begin
simp,
sorry
end)
Mario Carneiro (Dec 04 2020 at 20:35):
you have to prove that finite cardinalities are countably additive
Lars Ericson (Dec 04 2020 at 21:01):
I added the M1_MS
to declare the measure_space
to go with the measure
. My copy of Lean, downloaded yesterday, doesn't know measurable_space.copy
, measurable_space.copy_eq
and measure_space
itself, though that is declared here:
Screenshotfrom20201204155745.png
Yakov Pechersky (Dec 04 2020 at 21:09):
That's because Mario defined it above:
import data.finset.basic
import measure_theory.measurable_space
def X : Type := fin 3
def A1 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def A2 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
def measurable_space.copy {α} (c : measurable_space α)
(P : set α → Prop) (eq_P : ∀ s, P s ↔ @is_measurable _ c s) :
measurable_space α :=
begin
replace eq_P : P = c.is_measurable' := by ext; apply eq_P,
refine { is_measurable' := P, .. },
all_goals { abstract { subst_vars, casesI c, assumption } }
end
theorem measurable_space.copy_eq {α} (c P eq_P) :
@measurable_space.copy α c P eq_P = c :=
measurable_space.ext eq_P
def foo1 : measurable_space X :=
measurable_space.copy ⊥ A1 $
by simp [measurable_space.is_measurable_bot_iff, A1, eq_comm, or.comm]
def foo2 : measurable_space X :=
measurable_space.copy ⊤ A2 $ by simp [A2]
theorem foo1_eq : foo1 = ⊥ := measurable_space.copy_eq _ _ _
theorem foo2_eq : foo2 = ⊤ := measurable_space.copy_eq _ _ _
Lars Ericson (Dec 04 2020 at 21:28):
@Yakov Pechersky restricting to A1, that looks like this. I haven't got the measure_space
declaration quite right yet:
import data.finset.basic
import measure_theory.measurable_space
import measure_theory.measure_space
open measure_theory
def X : Type := fin 3
def A1 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def measurable_space.copy {α} (c : measurable_space α)
(P : set α → Prop) (eq_P : ∀ s, P s ↔ @is_measurable _ c s) :
measurable_space α :=
begin
replace eq_P : P = c.is_measurable' := by ext; apply eq_P,
refine { is_measurable' := P, .. },
all_goals { abstract { subst_vars, casesI c, assumption } }
end
theorem measurable_space.copy_eq {α} (c P eq_P) :
@measurable_space.copy α c P eq_P = c :=
measurable_space.ext eq_P
def M1 : measurable_space X :=
measurable_space.copy ⊥ A1 $
by { simp [measurable_space.is_measurable_bot_iff,
A1,
eq_comm,
or.comm],
sorry }
theorem M1_eq : M1 = ⊥ := measurable_space.copy_eq _ _ _
instance : fintype X := fin.fintype _
noncomputable instance foo (s : set X) : fintype s := by classical; apply_instance
noncomputable def M1_measure : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
(λ s _, finset.card s.to_finset)
(by simp)
(λ x h a, begin
simp,
sorry
end)
instance M1_MS : measure_space M1 :=
{ to_measurable_space := M1_eq,
volume := M1_measure }
Lars Ericson (Dec 04 2020 at 23:05):
The documentation is confusing because at the top level it says this:
structure measure_theory.measure_space (α : Type u_1) : Type u_1
to_measurable_space : measurable_space α
volume : measure_theory.measure α
I read this as meaning that I should supply an instance with two fields, to_measurable_space
and volume
. However, if I look at the source, it says something different:
class measure_space (α : Type*) extends measurable_space α :=
(volume : measure α)
I read this as meaning that I have to do everything I did for a measurable_space
, and also supply a volume
. In that case, based on example above in this thread:
instance : measurable_space X :=
{ is_measurable' := A1,
is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp, sorry },
I should be saying something like
instance : measure_space X :=
{ is_measurable' := A1,
is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp, sorry ,
volume := M1_measure
On the third hand, if I look at the supplied instances in the docs:
measure_theory.real.measure_space
measure_theory.measure.prod.measure_space
The first one is declared as
instance real.measure_space : measure_space ℝ :=
⟨{to_outer_measure := lebesgue_outer,
m_Union := λ f hf, lebesgue_outer.Union_eq_of_caratheodory $
λ i, borel_le_lebesgue_measurable _ (hf i),
trimmed := lebesgue_outer_trim }⟩
and the second one as:
instance prod.measure_space {α β} [measure_space α] [measure_space β] : measure_space (α × β) :=
{ volume := volume.prod volume }
So real.measure_space
supplies values for fields to_outer_measure
and m_Union
and trimmed
, none of which are mentioned in the class definitions of measurable_space
and subclass measure
. prod.measure_space
supplies a value for volume
but nothing for
is_measurable'
, is_measurable_empty
, is_measurable_compl
and is_measurable_Union
.
Reid Barton (Dec 04 2020 at 23:07):
Creating a field to_measurable_space
is how extends measurable_space
works. Ideally the documentation could detect this and turn it back into extends
for display purposes, but I'm not sure how easy that is in general.
Lars Ericson (Dec 06 2020 at 03:26):
In the end the following is what gets at what was bothering me best:
import measure_theory.measurable_space
def X : Type := fin 3
def A : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
structure σ_algebra (X : Type*) (A : set X → Prop) :=
(carrier_set : Type*)
(algebra : set X → Prop)
(is_measurable_empty : A ∅)
(is_measurable_compl : ∀ s, A s → A sᶜ)
(is_measurable_Union : ∀ f : ℕ → set X, (∀ i, A (f i)) → A (⋃ i, f i))
attribute [class] σ_algebra
instance XA: σ_algebra X A :=
{ carrier_set := X,
algebra := A,
is_measurable_empty := by {rw A, finish},
is_measurable_compl := assume a h, by {rw A at *, finish},
is_measurable_Union := assume f hf, by {rw A at *, simp },
}
#check XA  XA : σ_algebra X A
def to_measurable_space (X : Type) (A : set X → Prop) (XA : σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := A,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
instance M : measurable_space X := to_measurable_space X A XA
#check M  M : measurable_space X
I would like to take this a little bit further and be able to say:
def to_measurable_space1 (XA : σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := XA.algebra,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
instance M1 : measurable_space X := to_measurable_space1 XA
#check M1  M : measurable_space X
Unfortunately this yields a host of errors. To make this work I think I would need to utilize/adapt @Yakov Pechersky 's measurable_space.copy
. It seems to be textually rewriting the proof and then rerunning the proof through the proof engine. I don't understand it yet but I will study it now.
Screenshotfrom20201205222654.png
Yakov Pechersky (Dec 06 2020 at 05:25):
Just for reference, Mario wrote the measurable_space.copy
code. You're still using instance
in places where def
seems most appropriate. You're not relying on any typeclass inferring, so attribute [class] ...
is also not doing anything. On top of that, you're mixing names of definitions and names of variables. In the to_measurable_space1
, the error at is_measurable_empty
says that it cannot understand that XA.algebra
is the same as A
. And for that particular definition that you're trying to make, that would not have to be the case, because you're supplying any possible XA : σ_algebra X A
. That variable could have been called anything else. If you want to just use the XA
you defined above, you would really have to say
def to_measurable_space1 : measurable_space X :=
{ is_measurable' := XA.algebra,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
instance M1 : measurable_space X := to_measurable_space1
#check M1  M : measurable_space X
Lars Ericson (Dec 06 2020 at 14:23):
Thank you @Yakov Pechersky and @Mario Carneiro .
In my example above, I put in the attribute [class] ...
because if you take it out, you can an error from Lean in the example as stated.
If I look at the Lean reference manual, section 3.3, there is no mathematical overload to the definition of class
. A class
is just what we think of in Python or C++: It's a way of describing a record with fields. So:
class cls := (val : ℕ )
instance cls_five : cls := ⟨5⟩
#reduce cls_five  {val := 5}
Given that, if I have a definition of σ_algebra
with 5 fields I don't know why I should be reluctant to make an instance of it and populate the fields. I don't get why I should make that a def
.
@Yakov Pechersky , your version of to_measurable_space1
is constant and depends on XA
. I want to define XA
as a parameter to a function to_measurable_space1
. XA
is an instance of a class. So to some extent, it is a data object, not a definition. Given that Lean understands every other field reference to XA
than the first one, I don't know why it is complaining about the first field reference. A
is not mentioned on its own at all in the definition:
def to_measurable_space1 (XA : σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := XA.algebra,  Not OK
is_measurable_empty := XA.is_measurable_empty,  OK
is_measurable_compl := XA.is_measurable_compl,  OK
is_measurable_Union := XA.is_measurable_Union,  OK
}
I'm not trying to be difficult, I just don't understand the mechanics here. I know that if I (redundantly, as far as I can tell) present X
and X
along with XA
which has XA.carrier_set = X
and XA.algebra = A
, then things are fine. If I have to do that, I don't mind it. I just don't understand exactly why it is failing.
Mario Carneiro (Dec 06 2020 at 14:24):
If I look at the Lean reference manual, section 3.3, there is no mathematical overload to the definition of class. A class is just what we think of in Python or C++: It's a way of describing a record with fields.
No, that would be structure
Mario Carneiro (Dec 06 2020 at 14:24):
Lean's class
is inherited from Haskell's use as "type class"
Mario Carneiro (Dec 06 2020 at 14:29):
Recommended reading: http://learnyouahaskell.com/makingourowntypesandtypeclasses#typeclasses102
Mario Carneiro (Dec 06 2020 at 14:30):
Typeclasses have pretty much nothing to do with classes in languages like Java or Python. This confuses many people, so I want you to forget everything you know about classes in imperative languages right now.
Julian Berman (Dec 06 2020 at 14:34):
(we'd call them interfaces or protocols in Python if that's where you came from, and yeah it confused me too for a bit)
Lars Ericson (Dec 06 2020 at 14:35):
OK...but my example (before you get to to_measurable_space1
) does what I want (allows me to reuse my definition of sigma algebra) in measurable_space) where, for reasons of my own taste, I have pulled out the definition of sigma algebra from measurable_space. And the example doesn't go through (Lean won't allow it), unless I bless the sigma algebra structure
as a type class.
Thank you for the Haskell reference, I will read it now. I'm not sure that it will make me want to undo my pullout of sigma algebra as a construction from measure_space, because I like that I can see X and A on the same line in the #check XA  XA : σ_algebra X A
.
Reid Barton (Dec 06 2020 at 14:40):
I think it's actually reasonable to pull out σ_algebra
(though by mathlib conventions we would call it is_σ_algebra
; this linguistic viewpoint seems to confuse you repeatedly), but if you build more stuff on top of this you pretty quickly will want to work with the measurable_space
version.
Reid Barton (Dec 06 2020 at 14:43):
Actually I guess what you seem confused about is something else, namely the difference between writing down a type (or proposition) and writing down a term/proof of it
Reid Barton (Dec 06 2020 at 14:50):
which is fair enougha new user pleased to find that Lean accepts #check 2 + 2 = 4
might be dismayed to learn it is equally accepting of #check 2 + 2 = 5
Adam Topaz (Dec 06 2020 at 14:52):
Reid watch out... Twitter might come after you...
Mario Carneiro (Dec 06 2020 at 15:04):
"but lean checked the proof! It says it right there in the name"
Lars Ericson (Dec 06 2020 at 19:01):
@Yakov Pechersky @Reid Barton @Mario Carneiro @Julian Berman @Adam Topaz thanks, I have read the Haskell and narrowed down my point of confusion. This works, without type class attribute, and using instance
instead of def
and adding is_
:
import measure_theory.measurable_space
def X : Type := fin 3
def A : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
structure is_σ_algebra (X : Type*) (A : set X → Prop) :=
(carrier_set : Type*)
(algebra : set X → Prop)
(is_measurable_empty : A ∅)
(is_measurable_compl : ∀ s, A s → A sᶜ)
(is_measurable_Union : ∀ f : ℕ → set X, (∀ i, A (f i)) → A (⋃ i, f i))
def XA: is_σ_algebra X A :=
{ carrier_set := X,
algebra := A,
is_measurable_empty := by {rw A, finish},
is_measurable_compl := assume a h, by {rw A at *, finish},
is_measurable_Union := assume f hf, by {rw A at *, simp },
}
#check XA  XA : is_σ_algebra X A
def to_measurable_space (X : Type) (A : set X → Prop) (XA : is_σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := A,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
def M : measurable_space X := to_measurable_space X A XA
#check M  M : measurable_space X
This doesn't work, because even though X
and A
are defined in the namespace of the declaration and could be seen as typevalued identifiers, they are not available in the signature for some scoping reason:
def to_measurable_space (XA : is_σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := XA.algebra,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
I wouldn't have expected it to work myself except that I didn't notice that X and A are free in XA : is_σ_algebra X A
. Now that I see they are free, it makes complete sense to have to include them in the signature of to_measurable_space
. However, what is a little confusing as a usage constraint is that while this works:
def to_measurable_space (X : Type) (A : set X → Prop) (XA : σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := A,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
This does not work:
def to_measurable_space (X : Type) (A : set X → Prop) (XA : σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := XA.algebra,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
even though it should be clear from the construction of XA
that the value of A
is the same as the value of XA.algebra
. That is expecting too much of Lean I guess, so I won't whinge about it, I will just stay with is_measurable' := A
. But, for the record, i was not confusing types and values. What is getting assigned here is the value A
of type set X → Prop
to field is_measurable'
. Since by construction the value of A
and the value of XA.algebra
are identical. This should work. It doesn't. I don't completely understand why. But it is not because I am confused about something at the level of #check 2+2=5
. Reading the error messages, Lean is trying to prove something which should be, in some sense, obvious "by construction":
Display GoalDisplay Messages
25:0: error:
don't know how to synthesize placeholder (?is_measurable_empty)
context:
X : Type,
A : set X → Prop,
XA : is_σ_algebra X A
⊢ XA.algebra ∅
25:0: error:
don't know how to synthesize placeholder (?is_measurable_compl)
context:
X : Type,
A : set X → Prop,
XA : is_σ_algebra X A
⊢ ∀ (s : set X), XA.algebra s → XA.algebra sᶜ
25:0: error:
don't know how to synthesize placeholder (?is_measurable_Union)
context:
X : Type,
A : set X → Prop,
XA : is_σ_algebra X A
⊢ ∀ (f : ℕ → set X), (∀ (i : ℕ), XA.algebra (f i)) → XA.algebra (⋃ (i : ℕ), f i)
Mario Carneiro (Dec 06 2020 at 19:01):
your pings are multiplying
Mario Carneiro (Dec 06 2020 at 19:02):
you don't need to ping everyone in the conversation every time you say something. People who are watching the chat will respond anyway
Lars Ericson (Dec 06 2020 at 19:03):
OK I was trying to be polite. I will skip pings going forward!
Mario Carneiro (Dec 06 2020 at 19:04):
structure is_σ_algebra (X : Type*) (A : set X → Prop) := (carrier_set : Type*) (algebra : set X → Prop) (is_measurable_empty : A ∅) (is_measurable_compl : ∀ s, A s → A sᶜ) (is_measurable_Union : ∀ f : ℕ → set X, (∀ i, A (f i)) → A (⋃ i, f i))
this should not have the carrier_set
and algebra
fields
Lars Ericson (Dec 06 2020 at 21:05):
The main reason I declared the structure is to keep track of those two objects. Do those fields come for free if I leave them out? I.e. when I make an instance of a parameterized structure, are the values of the parameters that I used to create the structure available as an operation on the structure instance? They are not available as fields, for example
structure foo (X: Type) := {}
def bar : Type := foo ℕ
#check bar.X  unknown identifier 'bar.X'
Mario Carneiro (Dec 06 2020 at 21:16):
They are available by necessity because you have to pass them in
Mario Carneiro (Dec 06 2020 at 21:16):
You don't need bar.X
, you just use nat
Lars Ericson (Dec 06 2020 at 21:27):
They are available but not encapsulated. There are times in the life of a programmer when, even though the elements of a record are available on their own, it is convenient to pass around the record itself and then, at a later time, make use of its fields, without having to carry around the entire environment in which the record was created.
Alex J. Best (Dec 06 2020 at 21:28):
You can define your own helper function if you like
structure foo (X: Type) :=
(a : fin 7 × X)
def foo.X {X: Type} (h : foo X) := X
def bar : foo ℕ := sorry
#check bar.X
example : bar.X = ℕ := rfl
Eric Wieser (Dec 06 2020 at 21:37):
Note that in the original construction, there is no guarantee that X
and carrier_set
are equal.
Lars Ericson (Dec 06 2020 at 21:38):
OK
structure is_σ_algebra (X : Type*) (A : set X → Prop) :=
(is_measurable_empty : A ∅)
(is_measurable_compl : ∀ s, A s → A sᶜ)
(is_measurable_Union : ∀ f : ℕ → set X, (∀ i, A (f i)) → A (⋃ i, f i))
def is_σ_algebra.carrier_set {X: Type*} {A : set X → Prop} := X
def is_σ_algebra.algebra {X: Type*} {A : set X → Prop} := A
Eric Wieser (Dec 06 2020 at 21:38):
Which makes carrier_set
useless, because the other fields contain only proofs about X
Eric Wieser (Dec 06 2020 at 21:39):
Your new version might work better with abbreviation
instead of def
Eric Wieser (Dec 06 2020 at 21:40):
But as mentioned above, it's very hard to construct an example where those fields are useful
Alex J. Best (Dec 06 2020 at 21:41):
You want a term is_σ_algebra
to be an argument of those functions otherwise how will you ever call them?
Lars Ericson (Dec 06 2020 at 21:41):
Sorry working on it
Lars Ericson (Dec 06 2020 at 21:44):
Here we go:
import measure_theory.measurable_space
structure is_σ_algebra (X : Type*) (A : set X → Prop) :=
(is_measurable_empty : A ∅)
(is_measurable_compl : ∀ s, A s → A sᶜ)
(is_measurable_Union : ∀ f : ℕ → set X, (∀ i, A (f i)) → A (⋃ i, f i))
def is_σ_algebra.carrier_set {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A):= X
def is_σ_algebra.algebra {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A) := A
def to_measurable_space {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := A,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
 Example 1
def X : Type := fin 3
def A1 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
def XA1: is_σ_algebra X A1 :=
{ is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp },
}
#check XA1  XA : is_σ_algebra X A
#check is_σ_algebra.carrier_set XA1  XA1.carrier_set : Type
def M1 : measurable_space X := to_measurable_space XA1
#check M1
 Example 2
def A2 : set X → Prop := λ a, a ∈ ({⊤ , ∅} : set (set X))
def XA2: is_σ_algebra X A2 :=
{ is_measurable_empty := by {rw A2, finish},
is_measurable_compl := assume a h, by {rw A2 at *, finish},
is_measurable_Union := assume f hf, by {rw A2 at *, simp, sorry },
}
def M2 : measurable_space X := to_measurable_space XA2
Yakov Pechersky (Dec 06 2020 at 21:48):
You are still referring to A
in the body of to_measurable_space
. Why not do this? (Apart from whether or not it will be useful downstream...)
def to_measurable_space {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := XA.algebra,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
This uses the def is_σ_algebra.algebra {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A) := A
that you just defined, using projection notation.
Lars Ericson (Dec 06 2020 at 23:29):
Thank you. This is the definition I have wanted all along but, prior to declaring is_σ_algebra.algebra
, it did not go through.
Lars Ericson (Dec 06 2020 at 23:53):
But now I can't get down to measure_space
. Here is the full example up to measure_space
:
import measure_theory.measurable_space
import data.real.ennreal
import measure_theory.measure_space
open measure_theory
structure is_σ_algebra (X : Type*) (A : set X → Prop) :=
(is_measurable_empty : A ∅)
(is_measurable_compl : ∀ s, A s → A sᶜ)
(is_measurable_Union : ∀ f : ℕ → set X, (∀ i, A (f i)) → A (⋃ i, f i))
def is_σ_algebra.carrier_set {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A):= X
def is_σ_algebra.algebra {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A) := A
def to_measurable_space {X: Type*} {A : set X → Prop} (XA : is_σ_algebra X A) : (measurable_space X) :=
{ is_measurable' := XA.algebra,
is_measurable_empty := XA.is_measurable_empty,
is_measurable_compl := XA.is_measurable_compl,
is_measurable_Union := XA.is_measurable_Union,
}
def X : Type := fin 3
def A1 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))
def XA1: is_σ_algebra X A1 :=
{ is_measurable_empty := by {rw A1, finish},
is_measurable_compl := assume a h, by {rw A1 at *, finish},
is_measurable_Union := assume f hf, by {rw A1 at *, simp },
}
#check XA1  XA : is_σ_algebra X A
#check is_σ_algebra.carrier_set XA1  XA1.carrier_set : Type
def M1 : measurable_space X := to_measurable_space XA1
instance XFT : fintype X := fin.fintype _
noncomputable instance foo (s : set X) : fintype s := by classical; apply_instance
noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
(λ s _, finset.card s.to_finset)
(by simp)
(λ x h a, begin
simp,
sorry
end)
#check M1  M1 : measurable_space X
#check μ_M1  μ_M1 : measure X
def M1_MS : measure_space M1 := { to_measurable_space := M1, volume := μ_M1 }
This error is very confusing:
type mismatch at field 'to_measurable_space'
M1
has type
measurable_space X : Type
but is expected to have type
measurable_space ⁇ : Type ?
Similarly confusing:
type mismatch at field 'volume'
μ_M1
has type
measure X : Type
but is expected to have type
measure ⁇ : Type ?
The definition is:
class measure_space (α : Type*) extends measurable_space α :=
(volume : measure α)
export measure_space (volume)
If I leave out the to_measurable_space
field in the hopes that it gets automatically derived since measure_space
is an extension of measurable_space
, I still get a problem with just
def M1_MS : measure_space M1 := { volume := μ_M1 }
I still get the error
type mismatch at application
measure_space M2
term
M2
has type
measurable_space X : Type
but is expected to have type
Type ? : Type (?+1)
I am totally stumped here.
Lars Ericson (Dec 07 2020 at 00:23):
I think this is the part where I have to go back and undo removing the type class attribute, and maybe undo using instance versus def, because it worked before.
Last updated: May 07 2021 at 21:10 UTC