Copy of a Pi type?

Stream: new members

[Ashley Blacquiere]

What does "copy of a Pi type" mean in reference to #docs.pi_Lp?

[Moritz Doll]

It is a Pi type, but the instances for normed_space is different. If you look at docs#pi_Lp.equiv the proof is saying 'this is the same thing'

[Jireh Loreaux]

It means that we are creating a new type pi_Lp which is definitionally equal to Π i, E i (actually, we're creating a distinct copy for each p : ℝ≥0∞). However, the instances present for Π-types are not transported through, so we can put new instances on this structure; in this case, we want a different metric space instance.

[Ashley Blacquiere]

Out of curiosity, where would I find the "instances present for Π-types", just to better understand why we wouldn't want them in this case? I would guess they're probably much more numerous than what might be contained in a single file...?

[Moritz Doll]

you find them usually under the definition, there is "Instances for pi_Lp" in docs#pi_Lp

[Matt Diamond]

I don't think there's a "definition" for the pi type itself in mathlib, so I'm not sure there's an easy way to browse the instances...

[Matt Diamond]

other than putting pi. in the mathlib docs search box and browsing the suggestions

[Mario Carneiro]

there is a file called pi_instances though

[Matt Diamond]

!

[Matt Diamond]

well then

[Mario Carneiro]

Actually I take it back. There used to be such a file, now there is a file pi_instances.lean containing a tactic which constructs pi instances, and about 16 files called pi.lean in various parts of mathematics

[Matt Diamond]

ah, alas

[Mario Carneiro]

docs#metric_space_pi seems relevant if you are looking for the metric that pi_Lp is distinguishing itself from

[Ashley Blacquiere]

On an unrelated note, what is the reason that instances in source appear as def in the API?

[Ashley Blacquiere]

Is the following relation (from Wikipedia) encoded anywhere in these libraries? image.png

[Mario Carneiro]

I believe this is (very opaquely) encoded in the theorem docs#pi_Lp.antilipschitz_with_equiv_aux

[Mario Carneiro]

in practice, the way you see this is the fact that both the Lp space and the sup norm have the same topology (the product topology)

[Ashley Blacquiere]

Ok. That's good info. Thanks.

From an architectural standpoint, why is #docs.pi_Lp defined on products of metric spaces? Or maybe that's a nonsensical question...?

[Mario Carneiro]

as opposed to what?

[Mario Carneiro]

the whole idea is that you are combining multiple dimensions in a particular way. Each dimension has its own metric structure and the p-powered weighted average is used to combine the distances

[Reid Barton]

Perhaps as opposed to https://leanprover-community.github.io/mathlib_docs/measure_theory/function/lp_space.html?

[Ashley Blacquiere]

I guess then what I'm asking is what is the end game pi_Lp? What was it written in service to?

Apologies if this seems trite. I'm still trying to understand why certain mathlib libraries are developed the way they are...

[Ashley Blacquiere]

Reid Barton said:

Perhaps as opposed to https://leanprover-community.github.io/mathlib_docs/measure_theory/function/lp_space.html?

Ya, I think that's sort of what I'm getting at, but my head isn't quite wrapped around what I want to ask, I think. I guess I don't understand why pi_Lp exists, but I assume there is an ultimate purpose.

[Matt Diamond]

my (extremely basic) understanding is that it's useful to study multidimensional spaces as Pi types, but there is a "default" metric on the Pi type itself, and so you need to use a copy of it to avoid that metric interfering with other metrics that you want to define/use

[Mario Carneiro]

I think the simplest way to answer "what is the end game of pi_Lp? What was it written in service to?" is https://en.wikipedia.org/wiki/Lp_space

[Mario Carneiro]

we want something that corresponds to the thing that this page is about

[Ashley Blacquiere]

Mario Carneiro said:

I think the simplest way to answer "what is the end game of pi_Lp? What was it written in service to?" is https://en.wikipedia.org/wiki/Lp_space

Fair point. That's the page I linked to above, so I was looking at it, but I don't see anything about product spaces there. At least not obviously. But I'm not a mathematician (BSc in math, but a loooong time ago) so the nuances of these things may be escaping me...

[Mario Carneiro]

Actually it is more accurate to say that docs#measure_theory.Lp is https://en.wikipedia.org/wiki/Lp_space and docs#pi_Lp is https://en.wikipedia.org/wiki/Norm_(mathematics)#p-norm

[Matt Diamond]

Ashley, are you just unsure about why Pi types are useful for modeling multidimensional vector spaces?

[Reid Barton]

$\mathbb{R}^n$ is a product $\mathbb{R}^n = \mathbb{R} \times \mathbb{R} \times \cdots \times \mathbb{R}$. But it doesn't cause any particular additional difficulty to allow the "factors" to be distinct.

[Ashley Blacquiere]

Matt Diamond said:

Ashley, are you just unsure about why Pi types are useful for modeling multidimensional vector spaces?

No, but thanks for asking. When you state the question in that way it's actually pretty clear to me. However, what that reveals is that perhaps it is just a question of perspective and understanding (i.e. getting accustomed to) the particular nomenclature used in mathlib. I wasn't really thinking of 'finite product of metric spaces' as being analogous to 'multidimensional vector spaces' vis-a-vis Pi-types.

[Eric Wieser]

I don't think there's a "definition" for the pi type itself in mathlib, so I'm not sure there's an easy way to browse the instances...

Doc-gen currently has this list of pi instances internally, but discards them because it doesn't know where to show them. Do you have a suggestion for where they should be shown? We have the same problem for instances on Prop.

[Eric Wieser]

Update: I've made https://github.com/leanprover-community/doc-gen/pull/172 for lack of a better idea

[Eric Wieser]

https://leanprover-community.github.io/mathlib_docs_demo/foundational_types.html#pi-types-code%CF%80-a--%CE%B1-%CE%B2-acode-or-codepi-a--%CE%B1-%CE%B2-acode-or-code-a--%CE%B1-%CE%B2-acode-or-code%CE%B1--%CE%B2code

[Eric Wieser]

What a horrible URL

[Alex J. Best]

Could this page also include quot, quot.mk, quot.lift, quot.ind in such a way that they are linked to by statements like docs#quot.exists_rep

[Alex J. Best]

Lean can #print the type of these, so I assume they are accessible in doc-gen, just there is no home for them as they are super-duper builtin

[Alex J. Best]

@[elab_as_eliminator, elab_strategy]
builtin-quotient-type-constant quot.lift : Π {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β),
  (∀ (a b : α), r a b → f a = f b) → quot r → β

[Kyle Miller]

There's a command that introduces the quotient types that gets run in the prelude, and I guess it doesn't generate anything that docgen sees? https://github.com/leanprover-community/lean/blob/283f6ed8083ab4dd7c36300f31816c5cb793f2f7/library/init/core.lean#L109

[Alex J. Best]

I think that command basically just adds the 4 declarations I mentioned to the environment, https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/src/kernel/quotient/quotient.cpp#L73 so they should be visible in the json output of the environment

[Alex J. Best]

I assume that doc-gen just ignores them at some point as they are the only declarations in mathlib for which decl_olean returns an empty string (as they have no actual source location), so doc-gen doesn't know where to put them

[Alex J. Best]

I'm actually not sure if they show up in the json output or not, the relevant code is
https://github.com/leanprover-community/doc-gen/blob/d74f0abd7a7f7ee2b22184cd870f748eeded496d/src/export_json.lean#L323 which looks like it would fail for these decls, they are neither auto-generated not internal according to lean

[Alex J. Best]

Oh aha I think I see, https://github.com/leanprover-community/doc-gen/blob/d74f0abd7a7f7ee2b22184cd870f748eeded496d/src/export_json.lean#L319 is what causes them to be skipped, the in_current_file check is simply that decl_olean = "" which is true for these decls, so they are skipped

[Eric Wieser]

I guess we can define an in_current_file' with a hard-coded list of special cases

[Alex J. Best]

Hmm looks like I'm wrong again, docs#environment.in_current_file is correct now so I'm confused what happens to these declarations once more

[Eric Wieser]

Are they filtered out as autogenerated?

[Alex J. Best]

No I tested that for quot and it wasn't autogenerated