How do I make a Wikipedia-style metric space in Lean?

Stream: Is there code for X?

[Lars Ericson]

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]

@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 so-called "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]

@Johan Commelin I mean in the practical sense that I could have d1(x,y) = abs(x-y)or d2(x,y)=\sqrt((x-y)^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]

@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]

People have been working on lp spaces recently, if I'm not mistaken.

[Patrick Massot]

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]

Did you watch all LFTCM2020 videos? One of them is about redoing metric spaces from scratch.

[Patrick Massot]

Lars Ericson said:

I mean in the practical sense that I could have d1(x,y) = abs(x-y)or d2(x,y)=\sqrt((x-y)^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]

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]

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 Wikipedia-style metric space" which wouldn't be covered by what you pointed out in mathlib).

[Lars Ericson]

@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(x-y), d2(x,y)=EuclidNorm(x-y) and d3(x,y)=TaxiCabNorm(x-y). 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]

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]

In this setting it would be better to read metric_space as "metric".

[Reid Barton]

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]

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]

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]

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]

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]

That's why I didn't suggest writing instances but defs (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]

@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/extending-the-concept-of-distribution-function-to-any-totally-or-partially-order/3782009

[Lars Ericson]

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 well-founded way.

[Lars Ericson]

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]

Just don't use the word instance, and instead write def foo : metric_space (ℝ × ℝ) := ..., def bar : metric_space (ℝ × ℝ) := ..., etc

[Yakov Pechersky]

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 defs

[Yakov Pechersky]

Oh Reid said the same thing

[Patrick Massot]

And I already said it this morning, I even posted the corresponding code with only Prop sorries.

[Yakov Pechersky]

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]

Is there a category of metric spaces?

[Bhavik Mehta]

Not in Lean as far as I know

[Lars Ericson]

@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 #checks 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]

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]

You can write @metric_space.dist, some number of underscores, then m1

[Kevin Buzzard]

I was going to say that, but unknown identifier 'metric_space.dist'.

[Reid Barton]

oh rip

[Reid Barton]

it's in a superclass, that makes it quite awkward

[Reid Barton]

wait no yes

[Kevin Buzzard]

To make matters worse, there's an instance of has_dist (ℝ × ℝ) ;-)

[Reid Barton]

Anyways, I guess you already know that points in a metric space have a distance--so I'm not sure what you hope to gain from these #checks

[Lars Ericson]

@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]

I agree that it is full of errors

[Lars Ericson]

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]

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]

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 sorrys in metric_space_instance so it's not really usable as-is. 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 Wikipedia-ify this more:

• Use structure
• Make a class for metric, which mathlib doesn't, and put the focus on d.

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)) for a 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) for X ⊆ M of metric space (M,d)
• Cauchy-complete metric space
• Measure μ: A→ [0,∞)
• Measurable space (S,Σ)
• Measurable function f
• Pullback f⁻¹: Σ → A
• Push-forward 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 function T:ℝ→ [0,1] maybe a/k/a inverse distribution function F^-X of distribution function F_X
• Real distribution space (ℝ, B(ℝ), μ_x, F_X) from distribution μ_x on real-valued 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]

You could try to build up your theory for R^n first

[Eric Wieser]

Are you looking for docs#premetric_space, which has fewer fields?

[Yakov Pechersky]

Also, mathlib has a some of what you indicated, like intervals, Borel measure

[Lars Ericson]

@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 higher-level goals:

1. 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.

2. 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.

3. 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]

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]

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]

@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/Sigma-algebra>
* <https://en.wikipedia.org/wiki/Dynkin_system>

[Thomas Browning]

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]

@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 zero-dimensional (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 slug-fest where mathematicians constantly fought over how to express things and what to focus on. You can see the blow-by-blow 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]

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]

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:

1. Make X = {1,2,3}
2. Make A1 = {X, ∅}
3. Make A2 = set.powerset(X)
4. Prove that measurable_space A1 and measurable_space A2

Is this possible? I don't know how to do this.

[Lars Ericson]

Actually for X={1,2,3} I have a solution.

I was concerned about getting a "true set" and not a "set-like 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]

import data.finset.basic

#check ({1, 2, 3} : finset ℕ)

[Lars Ericson]

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]

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]

I don't have a type error for your

import data.finset.basic

def S : set ℕ := ({1, 2, 3} : finset ℕ)

#check S

[Yakov Pechersky]

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]

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: 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:

1. Make X = {1,2,3}
2. Make A1 = {X, ∅}
3. Make A2 = set.powerset(X)
4. Prove that measurable_space A1 and measurable_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]

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:
Screenshot-from-2020-12-03-16-38-34.png

[Lars Ericson]

@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]

no

[Mario Carneiro]

a proof would be #check (by apply_instance : measurable_space A1)

[Mario Carneiro]

all that typechecking the statement does is ensure that A1 can be treated as a type

[Lars Ericson]

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]

yes, there's a big difference between stating a theorem and proving it!

[Yakov Pechersky]

Oh btw I have a typo, I used \top, which is set.univ instead of \bot, which is the empty set

[Alex J. Best]

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]

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]

it would be nice to prove these by proving roughly (⊥ : measurable_space X) = A1

[Alex J. Best]

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]

there is docs#measurable_space.is_measurable_bot_iff but there is still some unwrapping to get the pair formulation

[Lars Ericson]

Thank you @Yakov Pechersky @Alex J. Best @Mario Carneiro this now gives a very clear guide for how to use mathlib.

[Lars Ericson]

In looking at this today I found these slides by Sylvie Boldo on Lebesgue integration in Coq. Is it fair to say that mathlibat 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]

@Thomas Browning on the changing story of math, I came across this picture today in Wikipedia: 1024px-Magma_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]

https://ncatlab.org/nlab/show/measurable+space

[Alex J. Best]

magma in mathlib would just be has_mul a binary operation with no axioms

[Alex J. Best]

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]

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 in-depth explanations. nLab is one such more in-depth reference.

[Lars Ericson]

@Yakov Pechersky it might be best practice to replace Wikipedia references in the mathlib source with nLab pages.

[Mario Carneiro]

magmas are popular in France I believe, because Bourbaki liked it

[Mario Carneiro]

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 non-experts

[Mario Carneiro]

wikipedia is much more appropriate for linking to core concepts in an undergraduate curriculum

[Mario Carneiro]

Also all the constructive detours in nLab are quite irrelevant for mathlib

[Adam Topaz]

Mario Carneiro said:

No, I don't think so. nLab has a tendency for being inscrutable to non-experts

Sometimes also for experts...

[Lars Ericson]

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]

that depends on what kind of identical you mean

[Mario Carneiro]

if they are defeq you can just reuse the proof

[Mario Carneiro]

if they are textually the same but are actually proving different things you can usually use a tactic

[Mario Carneiro]

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]

@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:
Screenshot-from-2020-12-04-10-41-44.png

Hence the question, what is the right way to do this so that I get significant re-use of code but the purpose of the code is to instantiate a structure with 4 fields.

[Mario Carneiro]

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]

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]

Your two instances M1 and M2 are a bad idea btw because instances are supposed to be unique per type

[Mario Carneiro]

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]

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]

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]

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]

if you don't follow this rule you get the "code generation failed" error

[Mario Carneiro]

What you are describing, that there are multiple non-equivalent members of measurable_space X, is what def is about

[Mario Carneiro]

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]

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]

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]

For measurable_space real, you could take the set of lebesgue measurable sets as canonical, or perhaps the borel measurable sets

[Mario Carneiro]

It's not a category in the mathematical sense, it's just a general theorem

[Mario Carneiro]

or def I should say

[Lars Ericson]

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]

It's not clear how to plan to proceed without those sorrys filled out

[Eric Wieser]

Because right now, they're impossible to fill

[Eric Wieser]

Your current statement is "every set of sets on X is a measure", but that's not true

[Mario Carneiro]

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]

We already have proofs that \top : measurable_space X and \bot : measurable_space X, I think that covers your use cases already

[Yakov Pechersky]

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]

@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 proofs-of-correctness (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 fine-grained 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]

@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]

It is the type of all sigma algebras

[Mario Carneiro]

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]

lemma something_about_A1 {X : Type} (sigma : measurable_space X) (h : sigma.is_measurable' = A1) : ... := ...

?

[Lars Ericson]

@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]

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]

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]

@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]

The b is only buried if you want it to be

[Mario Carneiro]

like I've been saying, measurable_space X is a type, that has elements, that you can use in expressions

[Mario Carneiro]

you don't have to always use them as instances

[Mario Carneiro]

it's like this: (a : Type) (b : measurable_space a), see no burying

[Mario Carneiro]

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]

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]

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]

and then we prove post hoc that the top and bot so defined are in fact univ and {empty, univ} respectively

[Mario Carneiro]

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]

@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]

That's not a metric, I guess you mean a measure

[Mario Carneiro]

the measure is called docs#measure_theory.measure.count in mathlib

[Mario Carneiro]

It is defined by (infinite) summing 1 over the set

[Mario Carneiro]

If you happen to know the set is finite you can use finset.card to get the cardinality

[Mario Carneiro]

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]

the proof that fin n has size n is docs#fintype.card_fin

[Mario Carneiro]

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]

you have to prove that finite cardinalities are countably additive

[Lars Ericson]

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:
Screenshot-from-2020-12-04-15-57-45.png

[Yakov Pechersky]

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]

@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]

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]

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]

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 re-running the proof through the proof engine. I don't understand it yet but I will study it now.

Screenshot-from-2020-12-05-22-26-54.png

[Yakov Pechersky]

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]

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]

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]

Lean's class is inherited from Haskell's use as "type class"

[Mario Carneiro]

Recommended reading: http://learnyouahaskell.com/making-our-own-types-and-typeclasses#typeclasses-102

[Mario Carneiro]

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]

(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]

OK...but my example (before you get to to_measurable_space1) does what I want (allows me to re-use 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 pull-out 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]

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]

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]

which is fair enough--a 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]

Reid watch out... Twitter might come after you...

[Mario Carneiro]

"but lean checked the proof! It says it right there in the name"

[Lars Ericson]

@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 type-valued 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]

your pings are multiplying

[Mario Carneiro]

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]

OK I was trying to be polite. I will skip pings going forward!

[Mario Carneiro]

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]

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]

They are available by necessity because you have to pass them in

[Mario Carneiro]

You don't need bar.X, you just use nat

[Lars Ericson]

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]

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]

Note that in the original construction, there is no guarantee that X and carrier_set are equal.

[Lars Ericson]

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]

Which makes carrier_set useless, because the other fields contain only proofs about X

[Eric Wieser]

Your new version might work better with abbreviation instead of def

[Eric Wieser]

But as mentioned above, it's very hard to construct an example where those fields are useful

[Alex J. Best]

You want a term is_σ_algebra to be an argument of those functions otherwise how will you ever call them?

[Lars Ericson]

Sorry working on it

[Lars Ericson]

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]

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]

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]

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]

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.