spaces of measures / R

Stream: condensed mathematics

[Johan Commelin]

Do I understand correctly that we do not yet have a definition of $\mathcal M_{p}(S)$ as comphausly filtered pseudo-normed group in Lean?

[Johan Commelin]

@Filippo A. E. Nuccio is working hard on Thm 6.9. Once we have that, we want to show that $\mathcal M_p(S)$ is a quotient of $\mathcal M(S, \Z((T))_{r'})$ (for suitable $r'$). I think this space of "integral Laurent measures" is more or less completely formalized.

[Filippo A. E. Nuccio]

I confess I have a bit lost track of what was going on outside of Thm 6.9, so I can't be of much help. I honestly don't even know if we already have that $\mathbb{R}$ is a comphaus_bla (which I will need soon, at any rate). I remember @Adam Topaz pushed something last week, though.

[Adam Topaz]

Last week I proved that CompHaus..._1 has all limits.

[Adam Topaz]

Still nothing about comhaus_filt... For M_p(S) with S finite

[Johan Commelin]

@Adam Topaz At some point you formalized $\overline{\mathcal M}_{r'}(S)$ as presheaf, I think.
Thats everything coming after: https://github.com/leanprover-community/lean-liquid/blob/master/src/Mbar/Mbar_le.lean#L501

Should this be refactored to make use of the new CompHaus..._1 stuff?

[Johan Commelin]

I think if we have a functor Fintype => CompHaus... then it can be extended to Profinte => CompHaus_1 quite formally, right?

[Adam Topaz]

Yeah, that's the idea.

[Adam Topaz]

We have the stuff in for_mathlib/Profinite/extend.lean

[Johan Commelin]

Marvellous!

[Johan Commelin]

So, do I understand correctly that we should now copypasta the Laurent measures directory, and build a version over the reals?

[Adam Topaz]

There is one missing thing in that extend.lean file: that the extension of a functor from Fintype preserves filtered colimits.

[Johan Commelin]

Also, can we state 9.4 for profinite S already?

[Adam Topaz]

I don't know if we will actually need that, but it's what's left to have a more or less complete api

[Johan Commelin]

I'll try to define Mbar.functor : Profinite => ProFiltPseuNormGrp_1 using your machinery.

[Adam Topaz]

We don't have ProFilt..._1, but we probably should :wink:

[Johan Commelin]

We actually need to target ProFiltPseuNormGrpWithTinv r'

[Johan Commelin]

I hope that it has all the right limits :sweat_smile:

[Adam Topaz]

It should, as long as the basic structure mimics the definition of CompHaus...\_1 (including the exhaustive condition, and the strictness of morphisms)

[Johan Commelin]

maps are strict, but the filtration isn't exhaustive, as of now.

[Adam Topaz]

The Tinv automorphism will not be an automorphism in the category itself, but we can still encode it in some other way

[Adam Topaz]

Johan Commelin said:

maps are strict, but the filtration isn't exhaustive, as of now.

the exhaustive condition is required to define the lift for a limit.

[Johan Commelin]

For 9.4, we really need the Tinv, also in the case of profinite S.

[Johan Commelin]

So we cannot make do with some "easier" category of comphaus filtered stuff or so.

[Johan Commelin]

I don't think the Tinv will cause much trouble though. We just need to add the exhaustion to the conditions.

[Adam Topaz]

No, it shouldn't. It should be possible to mimic what I've done in the comphaus case for the profinite_with_Tinv case.

[Adam Topaz]

I'm looking at the definition of the hom's now.

[Adam Topaz]

In fact, we can redefine these as

structure profinitely_filtered_pseudo_normed_group_with_Tinv_hom (r' : ℝ≥0) (M₁ M₂ : Type*)
  [profinitely_filtered_pseudo_normed_group_with_Tinv r' M₁]
  [profinitely_filtered_pseudo_normed_group_with_Tinv r' M₂]
  extends strict_comphaus_filtered_pseudo_normed_group_hom M₁ M₂ :=
(map_Tinv' : ∀ x, to_fun (Tinv x) = Tinv (to_fun x))

which is defeq-ish to the previous definition

[Johan Commelin]

Sure, makes sense.

[Johan Commelin]

@Adam Topaz I just pushed a new file Mbar/functor.lean containing

/-- `Mbar r' S` extends to a functor in `S`, for profinite `S`. -/
def functor : Profinite ⥤ ProFiltPseuNormGrpWithTinv r' :=
Profinite.extend (fintype_functor r')

and 1 sorry.

[Johan Commelin]

The sorry is about those limits existing.

[Johan Commelin]

Are you exhaustifying those objects atm? I guess this might imply a whole bunch of fixes throughout the library...

[Adam Topaz]

Yeah, that sorry won't be true without exhaustifyingg.

[Adam Topaz]

I have a meeting soon, but I can try to exhaustify after that :)

[Adam Topaz]

We'll have to figure out how to handle products at some point... the current ad-hoc construction doesn't give a categorical product unless the index set is finite.

[Johan Commelin]

But we only need finite products, right?

[Johan Commelin]

Problem solved? :stuck_out_tongue_wink:

[Adam Topaz]

I've added:

instance : limits.has_limits ProFiltPseuNormGrp₁.{u} :=
has_limits_of_has_limits_creates_limits to_CHFPNG₁

[Adam Topaz]

For the Tinv stuff, I think the best thing to now do is to prove that the functor from ProFilt...WithTinv to ProFiltPseuNormGrp₁ creates limits.

[Adam Topaz]

Hmm... it looks like exhaustifying ProFiltPseuNormGrpWithTinv is going to be a nontrivial refactor, and I don't think I have enough time for this today. If anyone wants to take it on, please do so!

[Johan Commelin]

It might be easier to just create a new category. Then the proof of 9.4 can use non-exhaustive objects.

[Johan Commelin]

We can always clean up later.

[Johan Commelin]

@Adam Topaz I've pushed src/real_measures.lean. I haven't done the topology yet.

[Johan Commelin]

Whoops! Never push code before breakfast :see_no_evil: :face_palm:
The definition is all wrong.

[Adam Topaz]

Looks good! How hard is proving the comphaus_filtered_pseudo_normed_group instance? Does mathlib know that the l^p ball is compact?

[Adam Topaz]

Oh, one more think (looking at the commented out code): We want the functor to take place in CompHausFiltPseuNormGrp_1 which is the category with limits, so map_hom should be in strict_comphaus_filtered_pseudo_normed_group_hom

[Adam Topaz]

Johan Commelin said:

It might be easier to just create a new category. Then the proof of 9.4 can use non-exhaustive objects.

Sure, that's probably the easiest approach. I'll try to do this later today.

[Adam Topaz]

So the diagram of all of these categories will look like this:

 CompHausFilt_1 --------> CompHausFilt ---------> Cond (Ab)
    ^                          ^
    |                          |
ProFinFilt_1   --------> ProFinFilt
    ^                         ^
    |                         |
ProFinFiltWithTinv_1 --> ProFinFiltWithTinv

The left hand side have an exhaustive filtration with strict morphisms, and will all have limits, and the middle column need not be exhaustive.

[Johan Commelin]

Looks good!

[Johan Commelin]

Adam Topaz said:

Looks good! How hard is proving the comphaus_filtered_pseudo_normed_group instance? Does mathlib know that the l^p ball is compact?

I have no idea. I'll find out in the next few hours (-;

[Johan Commelin]

I killed some sorries. Time to start thinking about the topology.

[Johan Commelin]

instance pfpng_real_measures : comphaus_filtered_pseudo_normed_group (ℳ p S) :=

is sorry free, except for compactness.

[Johan Commelin]

compactness is converging. but first I'll have dinner

[Johan Commelin]

done

[Johan Commelin]

def functor (p : ℝ≥0) [fact (0 < p)] [fact (p ≤ 1)] : Fintype.{u} ⥤ CompHausFiltPseuNormGrp.{u} :=
{ obj := λ S, CompHausFiltPseuNormGrp.of $ ℳ p S,
...

is now sorry free

[Adam Topaz]

We need it in CompHausFiltPseuNormGrp_1 ;) (so we can take limits)

[Johan Commelin]

yeah, but I imagine that will be an easy tweak (-;

[Johan Commelin]

I just pushed

[Adam Topaz]

Sure, it should be easy enough to tweak. Do you want me to do it?

[Johan Commelin]

@Adam Topaz I'm almost done

[Johan Commelin]

@Adam Topaz I pushed the strictification

[Johan Commelin]

Btw, I'm making ℳ p S local notation, so that we can use the same notation for the actual condensed abelian group.

[Johan Commelin]

With a bit of luck, the statement of the challenge will look very similar to what is written in the blogpost.

[Adam Topaz]

The following is now sorry-free:

instance : limits.has_limits (ProFiltPseuNormGrpWithTinv₁.{u} r) :=
has_limits_of_has_limits_creates_limits (to_PFPNG₁ r)

[Filippo A. E. Nuccio]

I was trying to define the following coercion

instance : has_coe ℝ (ℳ S) := { coe := λ a s, a }

to view a real number as the constant function on S. Although Lean does not complain on the nose, I get an error while doing

variable (a : ℝ)
#check ((λ s : S, a) : (ℳ S)) -- this works
#check (a : (ℳ S)) -- this does not work: it runs for a minute or so and then says "maximum class-instance
--resolution depth has been reached  (the limit can be increased by setting option
-- 'class.instance_max_depth') (the class-instance resolution trace can be visualized by
-- setting option 'trace.class_instances')"

Any idea?

[Riccardo Brasca]

Maybe there is a loop. Where can I test this?

[Riccardo Brasca]

I mean, in which file of LTE

[Filippo A. E. Nuccio]

I have just tried to introduce it in laurent_measures/add_stable.lean, the above code is commented on lines 32-34 of the version on master

[Riccardo Brasca]

#check (↑a : (ℳ S)) works, so it should be something related to automatically insert ↑

[Filippo A. E. Nuccio]

Oh, thanks! That's weird, no?

[Riccardo Brasca]

Mmh, maybe you should use docs#has_coe_to_fun

[Filippo A. E. Nuccio]

Ok, let me try. I confess I never understood the difference.

[Yaël Dillies]

coe_fn can be inserted where a function is expected. coe can't. Namely, coe_fn f x will elaborate while coe f x won't. But here that doesn't seem to be the problem because Lean isn't expecting a function as you aren't doing a x but just a (it just so happens that the expected type is a type of functions, but you aren't using it as such).

[Riccardo Brasca]

It's just a random try, I don't understand what's going on either

[Filippo A. E. Nuccio]

I see, but I ran into an even earlier problem: if I try

instance : has_coe_to_fun ℝ (ℳ S) := {coe := λ a s, a }

it requires me to add an out_parameter

[Yaël Dillies]

That's not how you use has_coe_to_fun.

[Riccardo Brasca]

It's probably something like instance : has_coe_to_fun ℝ (λ _, ℳ S) := ⟨λ a s, a⟩, but it doesn't work

[Yaël Dillies]

I'm not sure what ℳ is, but has_coe_to_fun ℝ (λ _, ℳ S) will get you closer.

[Filippo A. E. Nuccio]

I see, I guess I see the difference (and agree that I don't need it here). Yet, I don't understand why has_coe requires the upper-arrow, whereas it can normally detect it automagically.

[Filippo A. E. Nuccio]

It is not a huge deal, just a bit odd.

[Riccardo Brasca]

Just to clarify, ℳ is defined by

def real_measures (p : ℝ≥0) (S : Fintype) := S → ℝ
parameter {p : ℝ≥0}
local notation `ℳ` := real_measures p

[Yaël Dillies]

Ah so ℳ is the one that should get a fun_like instance!

[Reid Barton]

has_coe_to_fun seems like a red herring here

[Filippo A. E. Nuccio]

Well, I am very happy with has_coe indeed.

[Reid Barton]

What happens with #check (a : (ℳ S)) if you don't define any new instance?

[Filippo A. E. Nuccio]

Let me try

[Filippo A. E. Nuccio]

invalid type ascription, term has type
ℝ : Type
but is expected to have type
real_measures p S : Type u

[Filippo A. E. Nuccio]

Well, but the has_coe works, as Riccardo pointed out. The funny behaviour is with the arrow, I find.

[Riccardo Brasca]

I am trying with set_option trace.class_instances true (I've named the instance foo). There is a

[class_instances] (2) ?x_13 : has_coe ℝ ?x_12 := @foo ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19
[class_instances] (3) ?x_18 : fact (1 / 2 < 1) := _inst_4
[class_instances] caching instance for fact (1 / 2 < 1)
_inst_4
[class_instances] (3) ?x_17 : fact (0 < 1 / 2) := _inst_4
failed is_def_eq
[class_instances] (3) ?x_17 : fact (0 < 1 / 2) := _inst_3
[class_instances] caching instance for fact (0 < 1 / 2)
_inst_3
[class_instances] (3) ?x_16 : fact (?x_14 < 1) := _inst_4
failed is_def_eq
[class_instances] (3) ?x_16 : fact (?x_14 < 1) := _inst_3
failed is_def_eq
[class_instances] (3) ?x_16 : fact (?x_14 < 1) := _inst_2
[class_instances] caching instance for fact (p < 1)
_inst_2
[class_instances] (3) ?x_15 : fact (0 < p) := _inst_4
failed is_def_eq
[class_instances] (3) ?x_15 : fact (0 < p) := _inst_3
failed is_def_eq
[class_instances] (3) ?x_15 : fact (0 < p) := _inst_2
failed is_def_eq
[class_instances] (3) ?x_15 : fact (0 < p) := _inst_1
[class_instances] caching instance for fact (0 < p)
_inst_1

[Riccardo Brasca]

That looks promising

[Filippo A. E. Nuccio]

Promising :thinking: ?

[Reid Barton]

Maybe using has_coe_t would work

[Riccardo Brasca]

Mmh, maybe the problem is coming from all the fact. At the beginning there is

parmeter {p : ℝ≥0}
local notation `r` := @r p
local notation `ℳ` := real_measures p
local notation `ℒ` := laurent_measures r
variable [fact (0 < p)]
variable [fact (p < 1)]
variable [fact (0 < (1/2 : ℝ))]
variable [fact ((1/2 : ℝ) < 1)]

variable {S : Fintype.{u}}

local notation `ϖ` := Fintype.of (punit : Type u)

def θ_section (g : ℳ S) : (ℒ S) := ⟨ϑ_section (1 / 2 : ℝ) r p S g,
  summable_ϑ_section (1 / 2 : ℝ) r p S g⟩

instance foo : has_coe ℝ (ℳ S) := { coe := λ a s, a }

[Riccardo Brasca]

And there are lines like

[class_instances] (3) ?x_399 : has_coe (real_measures (@«r» (↑2 * p * p * p)) ?x_19) ?x_396 := @ray_vector.has_coe ?x_431 ?x_432 ?x_433

Even forgetting about ray_vector.has_coe, the fact that it is trying with p * p * p doesn't look good.

[Reid Barton]

variable [fact (0 < (1/2 : ℝ))]

I'm not even sure what this does considering it mentions no variables

[Reid Barton]

Does that mean it is included in all definitions?

[Filippo A. E. Nuccio]

It is, or in most of them. I was not very happy with this line, but the problem is that some construction relies on a parameter r together with two facts that 0 < r and r < 1. And here I am specializing to r=1/2 so Lean asks for the corresponding facts.

[Riccardo Brasca]

I think so, in the infoview of

example : true :=
begin

end

I see

_inst_3: fact (0 < 1 / 2)
_inst_4: fact (1 / 2 < 1)
⊢ true

[Yakov Pechersky]

What if you move the has_coe declaration before the variables lines that set up the facts?

[Filippo A. E. Nuccio]

Let me try

[Riccardo Brasca]

Oh, this works!

[Filippo A. E. Nuccio]

YES!

[Filippo A. E. Nuccio]

It works

[Filippo A. E. Nuccio]

Great.

[Yakov Pechersky]

The issue is that since you mention p (implicitly because it is a parameter), any instance constraint becomes part of the constraints of the has_coe.

[Filippo A. E. Nuccio]

Ah, I see.

[Filippo A. E. Nuccio]

Thanks

[Yakov Pechersky]

So we do the regular mathlib thing, where the definition works on all values

[Yakov Pechersky]

Thanks to Reid for suggesting the TC trace

[Reid Barton]

I don't think I suggested that but I was about to when it appeared!

[Yakov Pechersky]

And Riccardo for being proactive on it too :-)

[Yaël Dillies]

Shouldn't

variable [fact (0 < (1/2 : ℝ))]

rather be

instance : fact (0 < (1/2 : ℝ)) := ⟨one_half_pos⟩

[Filippo A. E. Nuccio]

Yes, it should. You are right

[Kevin Buzzard]

The whole fact thing is completely out of control in LTE and I seem to spend half my life writing fact.elim infer_instance to extract a proof that 0<r when I could just be writing hr.

[Kevin Buzzard]

The variables are particularly problematic as we've just seen.

[Johan Commelin]

fact.out _ is shorter.

[Johan Commelin]

If you have [hr : fact blah] you can also write hr.1.

[Kevin Buzzard]

yeah but we don't because they're unnamed variables!

[Kevin Buzzard]

I am not at all convinced by this fact approach

[Kevin Buzzard]

I am not clear about what problem it is supposed to be solving. If we have (r : R) [fact (r < 1)] then r is explicit. If we have (hr : r < 1) then we can make r implicit and just use hr instead of r (one character longer). Why get your hands dirty with facts? We saw above an unpleasant consequence.

[Kevin Buzzard]

Maybe I missed the part where they were actually useful, but the fact remains that I spent the last week working around them because random lemmas ask for the proofs explicitly.

[Johan Commelin]

We have a bunch of files

src/facts/int.lean  src/facts/nnreal.lean  src/facts/normed_group.lean

that contain lots of trivialities. The idea is that those trivialities are applied transparently.

[Johan Commelin]

I think that in the first part, this really worked well, and was used a lot.

[Kevin Buzzard]

Aha

[Kevin Buzzard]

OK so indeed I can report that fact.out _ is far more powerful than what I was doing with fact.elim _. The point is that, rightly or wrongly, there is a ton of basic inequality stuff which the type class inference system has been taught; fact.elim demands you input the fact, but fact.out gets type class inference to find it for you. This is a very devious trick and one I had not properly understood until now. Did you guys get the green light from the CS people to do this??

[Reid Barton]

It's not mathlib policy compatible, and wouldn't scale to a library the size of mathlib in its current form

[Reid Barton]

You can get basically the same effect with a tactic that uses apply_rules