thm 69

Stream: condensed mathematics

[Johan Commelin]

@Filippo A. E. Nuccio I saw that you are working on thm69.lean. I think you can gain a lot from using coercions from nnreal to real, instead of writing r'.1. I imagine that simp and norm_cast will work better if you use coercions.

[Johan Commelin]

Also, can't some of those results be proved by staying in nnreal?

[Filippo A. E. Nuccio]

@Johan Commelin Thanks! You're certainly right, and indeed I am refactoring almost everything by staying in nnreal.

[Johan Commelin]

I guess nat_floor forces you to use a ring. I wonder if it could be generalised to semirings, so that it works for nnreal too

[Filippo A. E. Nuccio]

I think too, you're right. The problem with staying in nnreal is that, sometimes things become $0$ (when they're negative), so any expression of the form x-y can be a bit painful. But I hope I can work this out.

[Yaël Dillies]

wink wink https://github.com/leanprover-community/mathlib/tree/floorsemiring wink wink

[Filippo A. E. Nuccio]

At any rate I agree that staying in nnreal is the best option.

[Filippo A. E. Nuccio]

@Yaël Dillies Ah good, you're generalising nat_floor to semirings?

[Yaël Dillies]

Yes. This was waiting for has_ordered_sub to come into existence, and it did. So I could come back to it, but I'm already very busy with locally finite orders and successor orders.

[Filippo A. E. Nuccio]

It would help me, indeed (I was able to make it do in a couple of cases, but if you're building a general API it will be better): that being said, I can survive for the time being, so take it easy! :wink:

[Yaël Dillies]

(btw if anyone wants to merge #9119 or another one of my PRs, that'll make my life easier :innocent: )

[Yaël Dillies]

As a second thought, I think I can unify nat_floor and floor once we have succ_order. floorand nat_floor are basically thin wrappers around galois_connection (but specialized ones) and their main uses come from the fact that n + 1 is the smallest thing bigger than n, which is the gist of succ_order.

[Filippo A. E. Nuccio]

Your love for Galois connections at its best...

[Yaël Dillies]

Or maybe nat_floor/floor should stay as they are because one of the adjoints is nat.cast/int.cast.

[Filippo A. E. Nuccio]

As a mathematician, I would say that not having floor because succ_order takes care of it would sound strange, even if it makes perfect sense in Lean. But I might be too old-minded...

[Johan Commelin]

Yaël Dillies said:

Or maybe nat_floor/floor should stay as they are because one of the adjoints is nat.cast/int.cast.

I think they should stay. But it would be good if nat_floor works for semirings.

[Filippo A. E. Nuccio]

@Johan Commelin I will try to push something a bit later to show how things look like staying in nnreal as much as possible.

[Yaël Dillies]

That's not quite what I meant. I meant that what makes floor interesting is that:

1. It is the lower adjoint of the coercion ℤ → α.
2. ℤ is a succ_order.

and what makes nat_floor interesting is that:

1. It is the lower adjoint of the coercion ℕ → α.
2. ℕ is a succ_order.

Those are very much the same thing, except that their common generalization would need to take the coercion as an explicit argument, which I think is not worth it.

[Filippo A. E. Nuccio]

@Johan Commelin I am now at the point where specializing r'=1/2 (or actually, r'=a/b : rat (positive and smaller than 1) would make my life easier. I confess that it was not completely clear to me to what extent this won't be a problem .

[Filippo A. E. Nuccio]

I would believe that the fact that r'=a/b : rat is OK makes the whole argument work, since we can use arbitrary small r'. At any rate, is this version enough, on your opinion?

theorem θ_surj (r' : ℚ) [fact (r' > 0)] [fact (r' < 1)]  (r : ℝ≥0) [fact (r ≠ 0)] [fact (r < 1)]  (h_rr' : r' < r):
∀ x : ℝ, ∃ (F : laurent_measures r (Fintype.of punit)), (θ r' r F) = x :=

Here θ takes an F which is r-convergent and evaluates T to r'.

[Johan Commelin]

@Filippo A. E. Nuccio Yes, feel free to specialize to a rational number, or even 1/2 when you really start needing it.

[Johan Commelin]

It's not clear to me whether laurent_measures r (Fintype.of punit) is the best way to talk about $\Z((T))_r$. It's quite a mouthful, and it means that you will always have to evaluate at punit.star.

[Johan Commelin]

It might be worth it to build the ring convergernt_laurent_series r

[Filippo A. E. Nuccio]

Thanks for the answer about r'!

[Filippo A. E. Nuccio]

Concerning laurent_measures r (Fintype.of punit)It is a indeed mouthful, you're right, but it felt to me more in the spirit of condensed Math. I'm happy at any rate to build convergent_laurent_series r: this is basically what the construction def laurent_measures.to_Rfct tries to do, so I just need to build the type out of it. But just to be clear, do you simply want to create the type of laurent_measures evaluated at r (together with a comm_ring instance) or do you think we'll need to show an iso with a subring of the Laurent series as now in mathlib?

[Johan Commelin]

I haven't yet thought about that too much

[Johan Commelin]

Maybe just continue working with the punit thingy for now.

[Filippo A. E. Nuccio]

OK, it will be easy to modify later - thanks.

[Filippo A. E. Nuccio]

Finally this

lemma has_sum_x : has_sum (λ i, (⌊(((y ξ x i) / ξ ^ i) : ℝ)⌋ : ℝ) * (ξ ^ i)) x

is sorry-free in thm71

[Johan Commelin]

Wonderful! That was quite an adventure (-;

[Filippo A. E. Nuccio]

Yeah, sorry it took that long. I am now properly stating that $\theta$ is surjective.

[Johan Commelin]

You should push your TeX write up to the blueprint repo!

[Johan Commelin]

Do you have write access already?

[Filippo A. E. Nuccio]

Ok, I will (I think I have access, I kind of remember I have once modified a comma or a misprint - I will check later).

[Filippo A. E. Nuccio]

BTW: How do I create a def with dot notation in a namespace? The deflaurent_measures.to_Rfct used to work (so that F.to_Rfct was accepted) as long as everything was (wrongly) in _root_ by now that everything is in the namespace thm71 it is not recognized. It must be a stupid tweak but I can't figure out how to make it work.

[Johan Commelin]

@Filippo A. E. Nuccio Well, not everything was wrongly in _root_ apparently.

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/import.20clash.3F/near/255430475 showed that certain pretty generic names were ending up in _root_. Those needed to be put in a namespace.

[Filippo A. E. Nuccio]

Ah, I see: you mean that only generic ones need to be "protected" by something particular, like laurent_measures.blabla does not and it is safer to put it in _root_?

[Johan Commelin]

It's not safer to put them in _root_ but it's safe enough. And the big upshot is that it will make dot-notation work again.

[Yaël Dillies]

Can't you simply append thm71? Or is the problem that you need the same def accross different theorem namespaces?

[Filippo A. E. Nuccio]

I tried but somewhat could not make it work. I certainly don't need the same def across different namespaces.

[Filippo A. E. Nuccio]

The

theorem θ_surjective (r : ℝ≥0) [fact (r < 1)] [fact (0 < ξ)] [fact (ξ < 1)]  :
∃ (F : laurent_measures r (Fintype.of punit)), (θ ξ r F) = x :=

is also sorry-free. @Johan Commelin : would you agree in deleting the first lines (15 to 55) with the "old" approach?

[Adam Topaz]

This is great! But I'm a little confused -- where can I find the assumption that $\xi < r$?

[Adam Topaz]

(I assume $\xi$ corresponds to $r'$ from Analytic.pdf?)

[Adam Topaz]

Oh, I guess that assumption is not needed for the surjectivity. Nice! (I suppose we will need this when we go to prove that $\theta$ is a morphism.

[Johan Commelin]

@Filippo A. E. Nuccio Great work!

And yes, those lines 15-55 can now be removed. How about src/laurent_measures/thm69_bad.lean? Do you want to keep that around?

[Filippo A. E. Nuccio]

If that is not a problem, I'd like to keep it around until we/I finish the construction of the SES, because there were some ideas there which might be relevant. I will delete it at that point.

[Filippo A. E. Nuccio]

I am also removing the lines in question.

[Filippo A. E. Nuccio]

@Adam Topaz Yes, indeed: $\xi$ is the $r'$ (when discussing with @Johan Commelin it was a bit of an headache to distinguish the two, so I picked up a different name); and the assumption $xi < r$ is not needed for surjectivity, since the series surjecting to any given $x$ can be chosen to converge on the whole open unit disk.

[Filippo A. E. Nuccio]

OK, I am now trying to set up the route to produce the SES. I think that we still need the

instance : comphaus_filtered_pseudo_normed_group ℝ :=

bcause the apply_instance doesn't find anything for ℝ. And then the second point will be to prove the

lemma foo : comphaus_filtered_pseudo_normed_group_hom θ

@Adam Topaz @Johan Commelin can you confirm these are the next steps?What troubles me is that at a certain point we will need to move away from laurent_measures supported on the singleton to general profinite S but I can't see when.

[Johan Commelin]

We need a map from laurent_measures r S to real_measure p S, right? So why would you need

instance : comphaus_filtered_pseudo_normed_group ℝ :=

[Johan Commelin]

I don't think we actually need the map $ℤ((T))_r → ℝ$. I'm suggesting we move on to the modules right away.

[Filippo A. E. Nuccio]

Ah, I see - I guess this is the point.

[Filippo A. E. Nuccio]

Are you suggesting that we construct the right arrow in

$$0 \to \mathcal M(S, \Z((T))_{r'}) \xrightarrow{\cdot f_x} \mathcal M(S, \Z((T))_{r'}) \to \mathcal M_{p'}(S) \to 0$$

and prove its surjectivity as first step? And this for every profinite $S$?

[Johan Commelin]

I guess we first do it for finite S, and hopefully magic will extend it to profinite S.

[Filippo A. E. Nuccio]

OK, good; also because I was looking at the file real_measures and there $S$ always seems to be a Fintype.

[Adam Topaz]

Johan Commelin said:

I guess we first do it for finite S, and hopefully magic will extend it to profinite S.

FWIW: "Magic" = Profinite.extend_nat_trans in for_mathlib/Profinite/extend.lean

[Johan Commelin]

@Adam Topaz But will that also extend the fact that it is an epi?

[Adam Topaz]

So to use it we would need to show $\theta$ is natural in $S$

[Adam Topaz]

No, proving it's an epi will require more work

[Johan Commelin]

We need a version that extends SES's, I think.

[Adam Topaz]

Well, in general there would be a $\lim^1$ term?

[Johan Commelin]

Hmmz, you mean we need to do some actual maths again? :rofl:

[Yaël Dillies]

Filippo A. E. Nuccio said:

Yaël Dillies Ah good, you're generalising nat_floor to semirings?

I am now working on this.

[Filippo A. E. Nuccio]

I am trying to have a look at Prop 7.2, as I believe that it will be crucial for uploading $\theta$ to a comp_haus_blabla morphism. I have a small doubt about point (3), is $g(x)$ the evaluation of $g$ at $x$ (so, what it is called $\theta_x(g)$ in Thm 6.9?)

[Johan Commelin]

Yup, that seems to make sense.

[Johan Commelin]

Note that what we really want is a nonexisting Prop 7.2' which does everything for spaces of measures (instead of the base rings)

[Johan Commelin]

But this should hopefully be a straightforward adaptation of Prop 7.2

[Filippo A. E. Nuccio]

Do you mean Thm 6.9 (2) or something more?

[Johan Commelin]

No, that's what I mean.

[Filippo A. E. Nuccio]

Ok, thanks.

[Filippo A. E. Nuccio]

I have just pushed a possible approach to the SES of Theorem 6.9. I don't know if it is the best one, and comments are welcome!

[Filippo A. E. Nuccio]

Two major points that I see are:
1) Although I am happy to work purely with abelian groups, the definition of the first map in the SES is "multiplication by a generator of $\mathrm{ker}\theta$". I think it would be reasonable to add an

instance : has_scalar (laurent_measures r (Fintype.of punit)) (laurent_measures r S)  :=

and this is currently done on line 364. It is quite straightforward, the only nasty thing is that we need to prove that this is actually a CompHausFiltPseuNormGroup action (so, additive, sending 0 to 0 and respecting filtration+topology). The other option would be to "explicitely describe" this multiplication, by noting that the above generator is something like $T-\xi$ (or perhaps $T-\xi^{-1}$), but I believe that this would not be much cheaper, the above four conditions would still need to be checked.
2) I was unable to find an instance that the category CompHausFiltPseuNormGrp has kernels, zeroes and images. Am I right or did I look at the wrong places?

[Filippo A. E. Nuccio]

I think I am done for tonight, but will resume working on this tomorrow.

[Filippo A. E. Nuccio]

I have just pushed some more material towards the SES of Thm6.9. @Johan Commelin can you confirm that its current formulation (l. 67 of thm69.lean) is what you had in mind?

[Johan Commelin]

@Filippo A. E. Nuccio Yes, that's looking good! Even though I had in mind just an unbundled version.

[Johan Commelin]

I would do the bundling afterwards, I think.

[Johan Commelin]

Note that add_monoid_hom.mk' allows you to skip the map_zero' field. That might be a useful intermediate step when constructing a comphausly_hom

[Filippo A. E. Nuccio]

Thanks! But what do you mean by "unbundled version"?

[Filippo A. E. Nuccio]

Also, do you agree that the has_scalar instance is needed to define multiplication by a generator of $\ker\theta$? Or do you have another approach in mind?

[Johan Commelin]

unbundled = without categories.

[Johan Commelin]

So just define the maps ad comphausly_homs. And then show that they compose to 0. For im = ker we will maybe need to define what im and ker mean in this context.

[Filippo A. E. Nuccio]

Ah, really in that sense? But there is no def of a SES without categories, no?

[Johan Commelin]

Sure, so getting an actual SES will happen in the bundling step.

[Filippo A. E. Nuccio]

Johan Commelin said:

So just define the maps ad comphausly_homs. And then show that they compose to 0. For im = ker we will maybe need to define what im and ker mean in this context.

Ah ok, I see. OK, I'll go for that.

[Johan Commelin]

But that step should just call to 5 earlier results, instead of inlining the proofs.

[Filippo A. E. Nuccio]

OKOK, got it.

[Filippo A. E. Nuccio]

Thanks.

[Filippo A. E. Nuccio]

I was trying to use the add_monoid_hom.mk' def, but I am unable to: in tactic mode, I get five fields to be filled in. Did you mean that I should first prove that my map is a add_monoid_hom with add_monoid_hom.mk' and then fill the map_zero' by simply using a field of the add_monoid_hom structure? I guess not, but cannot come up with anything smarter.

[Johan Commelin]

something like

def my_map_as_add_monoid_hom : blabla :=
add_monoid_hom.mk' _ _

def my_map_as_comphausly_thing : blabla :=
{ new_field1 := _,
  .. my_map_as_add_monoid_hom }

[Filippo A. E. Nuccio]

Ah ok: so the two dots inside the bracket make lean understand that it should look for all the missing fields in my_map_as_add_monoid_hom?

[Filippo A. E. Nuccio]

I have the feeling that specializing $\theta=1/2$ slows down the computation: I have defined θ₂ r = θ (1 / 2) r, and things are really slow now. Is it possible or must the slowness come from something else?

[Filippo A. E. Nuccio]

What is strange is that the orange bars on the right disappear almost immediately, and what now takes very long to be discharged are the ones on the left.

[Johan Commelin]

@Filippo A. E. Nuccio Does the problem persist after compiling the full project?

[Filippo A. E. Nuccio]

Yes, and it seems to be very localized to this file (all the other files work perfectly)

[Johan Commelin]

Hmm, frustrating

[Filippo A. E. Nuccio]

I am now trying with another version of the lemma where I keep $\xi$ as a variable

[Johan Commelin]

Random weird idea. Would it help to use def half := 1/ 2 and then only mention half? If that works, it would in some sense be quite sad.

[Filippo A. E. Nuccio]

Let me try.

[Riccardo Brasca]

def half := 1/ 2 is in ℕ, right?

[Riccardo Brasca]

And it is probably 1

[Filippo A. E. Nuccio]

Well, I did def half := (1 / 2 : ℝ)

[Filippo A. E. Nuccio]

(fixing a couple of errors, as soon as I have an answer I will report it)

[Reid Barton]

Another option along these lines is to keep a variable but also pass a hypothesis that it's equal to 1/2

[Filippo A. E. Nuccio]

Like variables (ξ : ℝ) [fact (ξ = 1/2 : ℝ)]?

[Johan Commelin]

Or just (h : ξ = 1/2)

[Filippo A. E. Nuccio]

OK, let me try.

[Filippo A. E. Nuccio]

Well, as far as I can tell the problem does not come from the $\xi= 1/2$: even leaving it as a variable and not specifying its value, my left bars still take very long to disappear. I will try to understand if the problem comes from somewhere else. Thanks for the suggestions, at any rate: it is somewhat a relief that the problem does not (seem to come from) specialising to a specific value.

[Johan Commelin]

I can reproduce the slowness. Take the following snippet:

lemma θ_is_linear (ξ : ℝ) : is_linear_map ℤ (θ ξ r) := sorry

noncomputable def θ₂.to_linear : (laurent_measures r (Fintype.of punit)) →ₗ[ℤ] ℝ :=
{ to_fun := θ (1 / 2) r,
  map_add' := (θ_is_linear r (1 / 2)).1,
  map_smul' := (θ_is_linear r (1 / 2) ).2 }

lemma ker_θ₂_principal : submodule.is_principal ((θ₂.to_linear r).ker) :=
begin
  -- constructor,
  let pos : ℕ → ℤ := λ n, (if n = 0 then -1 else if n = 1 then 2 else 0),
  let f₀ : ℤ → ℤ := λ d : ℤ, int.rec_on d (pos) (λ n, 0),
  use (λ s, f₀),
  sorry,
  ext,
  split,
  swap,
  sorry,
  sorry,
--   intro h_x,
--   obtain ⟨a, h_ax⟩ := mem_span_singleton.mp h_x,
--   apply mem_ker.mpr,
--   rw ← h_ax,
--   -- squeeze_simp,
--   simp,
--   apply or.intro_right,
--   rw θ₂.to_linear,
--   -- rw θ.to_linear,
--   simp,
--   rw θ,
--   simp,
--   simp_rw [laurent_measures.to_Rfct],
--   let S : finset ℤ := {0, 1},
--   have hf : function.support f₀ ⊆ S, sorry,
--   have hf₀ : ∀ s ∉ S, ((f₀ s) : ℝ) * ((2 ^ s) : ℝ)⁻¹ = (0 : ℝ), sorry,
--   rw [tsum_eq_sum hf₀],
--   -- rw ← [has_sum_subtype_iff_of_support_subset hf],
--   sorry, sorry,
end

[Johan Commelin]

That noncomputable def θ₂.to_linear takes ~ 9s and the lemma ker_θ₂_principal ~7s.

[Filippo A. E. Nuccio]

Any idea on why this happens?

[Johan Commelin]

I have no clue. The profiler says that it's spending ages on elaboration. I have no idea how to debug this further.

[Johan Commelin]

@Mario Carneiro If you have some time to look into this, that would be great.

[Filippo A. E. Nuccio]

Of course I can (=will!) improve the lemma, and its proof. But the definition looked quite innocent to me, and also somewhat necessary. Another option would be to immediately define θ as a linear_map, but would that be faster, on your opinion?

[Filippo A. E. Nuccio]

Do you think it might be related to the fact that the lemma θ_is_linear is sorryed?

[Johan Commelin]

That shouldn't matter

[Johan Commelin]

At this point, I really don't know where to look for the source of this problem

[Kevin Buzzard]

Is it related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Slow.20elaboration.20-.20algebra/near/257774565 which we also never got to the bottom of?

[Johan Commelin]

Hmm, could very well be.

[Filippo A. E. Nuccio]

I am teaching now, but I will try to modify the original definition of θ to immediately define it as a linear_map this afternoon, to see if that changes something.

[Kevin Buzzard]

(my logic is only that they're both "random algebra being slow")

[Filippo A. E. Nuccio]

A small update: as @Kevin Buzzard was rightly suggesting, there has basically been no improvement when changing the definition of θ as a linear_map instead of simply a map. I have the feeling that what is really slow is the submodule.is_principal ((θₗ r).ker) whereas the rest is somewhat OK. I will try to remove the lemma and just keep the relevant computation, since at any rate we know an explicit generator.

[Rob Lewis]

I might not have more time this afternoon to debug, gotta move on to a couple other things for now, but a couple preliminary notes:

• You have some slow searches for module ℤ (laurent_measures r (Fintype.of punit)) toward the beginning. Adding this as a high priority instance helps a bit but not everywhere.
• With set_option trace.type_context.is_def_eq true there are weird failures in various places (including the proof of θ₂.to_linear) of the form

[type_context.is_def_eq] summable (λ (n : ℤ), ↑|0 • ⇑F s n| * ↑r ^ n) = summable (λ (n : ℤ), |↑(0 • ⇑F s n)| * ↑r ^ n) =?= summable (λ (n : ℤ), ↑|0 • ⇑F s n| * ↑r ^ n) = summable (λ (n : ℤ), ↑|0 • ⇑F s n| * ↑r ^ n) ... failed  (approximate mode)

I can't figure out where this is coming from but it seems like it could be slow.

• In ker_θ₂_principal, adding fconstructor, fconstructor before use cuts the compilation time in half. use uses fconstructor under the hood, but only after it fails to unify the input with the original goal. At least one of these failures must be very slow for some reason.

[Filippo A. E. Nuccio]

I will be away from my PC and my VSCode for 10 days or so, until 2022; the current status of theorem 6.9 is that I have finally managed to have all details written down on paper, and most of the lemmas are stated in the file, some sorryed out. The code is a bit of a mess, but I hope to be able to finish the full proof of Theorem 6.9 quite soon as soon as I will be back, and to polish the code afterwards.

[Filippo A. E. Nuccio]

What will need to be done next is to state the exactness of the SES of Thm 6.9 in categorical terms; if nobody sees any obstruction, I would like to claim that part of the file as well, so as to get acquainted with the new categorical materials with which I have not worked much so far.