Zulip Chat Archive

Stream: maths

Topic: Naming contest


Yury G. Kudryashov (Oct 19 2020 at 13:08):

How would you call

def some_name : affine_subspace k (α →₀ k) :=
{ carrier := {f | f.sum (λ a, id) = 1}, .. }

and

def some_name : set (α →₀ k) := {f | f.sum (λ a, id) = 1   x, 0  f x}

@Joseph Myers I want to rewrite affine combinations based on the first definition. This way we'll have an API much closer to what's used in docs#linear_independent.

Eric Wieser (Oct 19 2020 at 13:13):

Can you show the typeclasses on α and k?

Adam Topaz (Oct 19 2020 at 13:16):

simplex for the second one?

Eric Wieser (Oct 19 2020 at 13:17):

The second one looks more suited to a Prop or perhaps a subtype rather than a set to me

  • is_some_name (f : α →₀ k) : Prop := f.sum (λ a, id) = 1 ∧ ∀ x, 0 ≤ f x
  • is_some_name : Type := { f : α →₀ k // f.sum (λ a, id) = 1 ∧ ∀ x, 0 ≤ f x}

(or both)

Adam Topaz (Oct 19 2020 at 13:17):

(I'm on mobile, so I can't see some Unicode, but I assume those are finsupps?)

Yury G. Kudryashov (Oct 19 2020 at 13:19):

Yes, arrows are finsupps

Adam Topaz (Oct 19 2020 at 13:19):

The first one is the affine space generated by the second one, which is the "standard" simplex, right?

Yury G. Kudryashov (Oct 19 2020 at 13:19):

@Eric Wieser The second one is the convex hull of all single x 1, so I want it as a set.

Yury G. Kudryashov (Oct 19 2020 at 13:20):

No typeclasses on α, semiring or ring on k.

Adam Topaz (Oct 19 2020 at 13:20):

Well, you need an order on k for the second one

Yury G. Kudryashov (Oct 19 2020 at 13:21):

Yes, an ordered semiring for the second one.

Yury G. Kudryashov (Oct 19 2020 at 13:21):

Those are universal objects for affine spaces with marked points and convex sets with marked points (as finsupp is for vector spaces with marked points).

Adam Topaz (Oct 19 2020 at 13:22):

free_affine and free_convex for names?

Joseph Myers (Oct 19 2020 at 19:11):

Whatever the implementation approach, weighted_vsub (combinations with sum of weights 0) should be implemented consistently with affine_combination (combinations with sum of weights 1) and it should be easy to work with both of those together.

Joseph Myers (Oct 19 2020 at 19:12):

In principle, finsupp makes sense for the weights. In practice, I think you'll need to do a lot of work on the finsupp API to make it as convenient to work with finsupp as it is to work with the big_operators API for sums over finsets.

Joseph Myers (Oct 19 2020 at 19:14):

Existing code using affine combinations uses of lots of big_operators lemmas, some of which were added to make those proofs more convenient. It constructs concrete weights using e.g. function.const, function.update, set.indicator and lambdas using ite and dite to describe weights piecewise. There are various lemmas for sums and products involving those operations; corresponding API will be needed for use of those operations or equivalent operations for finsupp.

Joseph Myers (Oct 19 2020 at 19:16):

There are also cases where concrete weights in geometry are defined using pattern matching on points_with_circumcenter_index.

Joseph Myers (Oct 19 2020 at 19:20):

Some of the manipulations in geometry.euclidean.monge_point dispose of quite complicated expressions with a quick simp, so should serve as a reasonable stress test for parts of the API for doing such things with finsupp.

Yury G. Kudryashov (Oct 19 2020 at 19:21):

I understand that if I want to refactor, then migrating existing code is my job ;)

Adam Topaz (Mar 17 2021 at 13:57):

Let C\mathcal{C} be a category, XX an object of C\mathcal{C}, and SS a set of objects in C\mathcal{C}.

Consider the full subcategory of the over category CX\mathcal{C}_X given by arrows YXY \to X where YSY \in S.

What should this category be called?

Adam Topaz (Mar 17 2021 at 17:51):

Well, I still don't know if this has a name, but I called it over_trunc in the specific case I'm thinking about:
https://github.com/leanprover-community/mathlib/blob/f3215b8e8b0929c62d9803632629d5af732c37fa/src/algebraic_topology/simplex_category.lean#L345

Greg Price (Mar 17 2021 at 21:56):

I think one popular name for that would be that it's a comma category. Specifically one would give a name to the full subcategory of C C on S S -- say D D -- and then it's the comma category (D,X) (D, X) .

Patrick Massot (Mar 20 2021 at 21:29):

New naming contest, with a series of three lemmas (improvements and golfing also welcome):

lemma yo {P :     Prop} (h :  n,  N,  k > N, P n k) :
   φ :   , strict_mono φ   n, P n (φ n) :=
begin
  choose u hu hu' using h,
  use (λ n, nat.rec_on n (u 0 0) (λ n v, u (n+1) v) :   ),
  split,
  { apply strict_mono.nat,
    intro n,
    apply hu },
  { intros n,
    cases n ; simp [hu'] },
end

lemma yo' {P :     Prop} (h :  n,  N,  k  N, P n k) :
   φ :   , strict_mono φ   n, P n (φ n) :=
begin
  apply yo,
  intros n N,
  rcases h n (N+1) with k, hk, hk'⟩,
  use k; tauto
end

lemma yo'' {P :     Prop} (h :  n,  N,  k  N, P n k) :
   φ :   , strict_mono φ   n, P n (φ n) :=
begin
  apply yo',
  intros n N,
  cases h n with N₀ hN₀,
  exact max N N₀, le_max_left _ _, hN₀ _ $ le_max_right _ _⟩,
end

Heather Macbeth (Mar 20 2021 at 23:20):

They can be golfed a little if you're willing to change the hypotheses to involve eventually and frequently. I feel like there is more that can be done in this direction, but at least this is a start:

import analysis.normed_space.basic

open filter

lemma yo {P :     Prop} (h :  n, ∃ᶠ k in at_top, P n k) :
   φ :   , strict_mono φ   n, P n (φ n) :=
begin
  simp only [frequently_at_top'] at h,
  choose u hu hu' using h,
  use (λ n, nat.rec_on n (u 0 0) (λ n v, u (n+1) v) :   ),
  split,
  { apply strict_mono.nat,
    intro n,
    apply hu },
  { intros n,
    cases n ; simp [hu'] },
end

lemma yo'' {P :     Prop} (h :  n, ∀ᶠ k in at_top, P n k) :
   φ :   , strict_mono φ   n, P n (φ n) :=
yo (λ n, (h n).frequently)

Yury G. Kudryashov (Mar 21 2021 at 16:28):

exists_strict_mono_forall_of_frequently?

Patrick Massot (Mar 22 2021 at 20:33):

Thanks Heather and Yury. I wanted to PR this to order.basic, next to strict_mono.nat so it's a bit early in the hierarchy for frequently and eventually. But I guess I could put it in order.filter.at_top_bot

Adam Topaz (Jul 21 2021 at 21:35):

I would like to introduce something approximately like the following category

import category_theory.category

open category_theory

universes u

variables {α β γ : Type u}

inductive thing (f : γ  β  α)
| left (a : α) : thing
| right (b : β) : thing

namespace thing

variables {f : γ  β  α}

inductive hom : thing f  thing f  Type u
| id (X : thing f) : hom X X
| of (b : β) (g : γ) : hom (left $ f g b) (right b)

def hom.comp : Π {X Y Z : thing f} (F : hom X Y) (G : hom Y Z), hom X Z
| _ _ _ (hom.id _) H := H
| _ _ _ (hom.of b g) (hom.id _) := hom.of b g

local attribute [tidy] tactic.case_bash

instance : category (thing f) :=
{ hom := hom,
  id := hom.id,
  comp := λ X Y Z, hom.comp }

end thing

Does this thing have a name? (Ping @Bhavik Mehta since this is related to stating the sheaf condition in the case where γ\gamma is a two-term type)

Bhavik Mehta (Jul 21 2021 at 21:37):

f might as well have type f : γ → β → α, right?

Adam Topaz (Jul 21 2021 at 21:38):

(Of course! Fixed)

Adam Topaz (Jul 21 2021 at 21:39):

This is some common generalization of the diagrams we use for wide pullbacks and for equalizers.

Bhavik Mehta (Jul 21 2021 at 21:45):

Maybe you can use this to generalise wide equalizers too?

Adam Topaz (Jul 21 2021 at 21:45):

Yeah, that should be possible

Adam Topaz (Jul 21 2021 at 21:48):

If you take α=β\alpha = \beta, γ\gamma to be punit, and f punit.star to be the identity, that should give the shape for wide equalizers

Adam Topaz (Jul 21 2021 at 21:48):

Umm, sorry not quite.

Adam Topaz (Jul 21 2021 at 21:48):

I want α=β\alpha = \beta to both be punit, and γ\gamma arbitrary

Adam Topaz (Jul 21 2021 at 21:49):

That should give wide euqlizers

Adam Topaz (Jul 21 2021 at 21:49):

with usual equalizers being γ=fin2\gamma = fin 2

David Wärn (Jul 22 2021 at 09:08):

It might be easier to define this as a path category? You probably want to think of functors out of it as just collections of arrows

David Wärn (Jul 22 2021 at 09:27):

It might be easier to define this as a path category? You probably want to think of functors out of it as just collections of arrows

Yury G. Kudryashov (May 03 2022 at 22:49):

How should I call this? It is useful, e.g., to define docs#bornology on a quotient space.

import order.filter.basic

open set filter

def name_me {α β : Type*} (l : filter α) (f : α  β) : filter β :=
{ sets := {s |  t  l, s = (f '' t)},
  univ_sets := univ, univ_mem, by simp⟩,
  sets_of_superset := by { rintro _ t s, hsl, rfl hst,
    refine s  f ⁻¹' t, mem_of_superset hsl (subset_union_left _ _), _⟩,
    rw [compl_union,  preimage_compl, image_inter_preimage, compl_inter, compl_compl,
      union_eq_self_of_subset_left hst] },
  inter_sets := by { rintro _ _ s, hsl, rfl t, htl, rfl⟩,
    exact s  t, inter_mem hsl htl, by rw [compl_inter, image_union, compl_union]⟩ } }

Reid Barton (May 03 2022 at 22:57):

Is this the right adjoint of filter.comap?

Yury G. Kudryashov (May 03 2022 at 23:51):

Indeed,

example {α β : Type*} {f : α  β} {la : filter α} {lb : filter β} :
  comap f lb  la  lb  name_me f la :=
begin
  split,
  { rintro H _ s, hs, rfl⟩,
    rcases H hs with t, ht, hts⟩,
    exact mem_of_superset ht (subset_compl_comm.1 $ image_subset_iff.2 $ compl_subset_compl.2 hts) },
  { intros H s hs,
    refine _, H s, hs, rfl⟩, _⟩,
    rw [preimage_compl, compl_subset_comm],
    exact subset_preimage_image _ _ }
end

Yury G. Kudryashov (May 04 2022 at 03:24):

filter.cocomap?

Iván Sadofschi Costa (May 30 2022 at 23:39):

What would be a good name for these?

def name_me  (F E: Type*) [field F] [field E] [algebra F E] :
  (E ≃ₐ[F] E)  (E →ₐ[F] (algebraic_closure E)) :=
λ σ, (is_scalar_tower.to_alg_hom F E (algebraic_closure E)).comp σ.to_alg_hom,
 λ σ τ h, alg_equiv.ext_iff.2 (λ a, no_zero_smul_divisors.algebra_map_injective E
   (algebraic_closure E) (alg_hom.ext_iff.1 h a))⟩

def name_me' {F E : Type*} [field F] [field E] [algebra F E] [normal F E] :
  (E →ₐ[F] (algebraic_closure E))  (E ≃ₐ[F] E) :=
by refine equiv.mk (λ (σ : E →ₐ[F] (algebraic_closure E)), (alg_hom.restrict_normal' σ E))
  (λ σ, (is_scalar_tower.to_alg_hom F E (algebraic_closure E)).comp σ.to_alg_hom)
  begin
    intro σ,
    ext,
    unfold alg_hom.restrict_normal',
    simp,
  end
  begin
    intro σ,
    ext,
    unfold alg_hom.restrict_normal',
    simp only [alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_of_bijective],
    apply no_zero_smul_divisors.algebra_map_injective E (algebraic_closure E),
    rw alg_hom.restrict_normal_commutes,
    simp,
  end

(These definitions use #14450)

Eric Wieser (May 31 2022 at 09:35):

I'd argue you should replace E ≃ₐ[F] E with E →ₐ[F] E there

Anne Baanen (May 31 2022 at 10:01):

Based on docs#alg_equiv.aut I'd say something like name_me := alg_equiv.aut_embedding_(algebraic_)closure and name_me' := alg_equiv.alg_hom_(algebraic_)closure_equiv_aut.

Eric Wieser (May 31 2022 at 10:08):

Although if we make that statement more general and use alg_hom then that name isn't going to help much...

Eric Wieser (May 31 2022 at 10:09):

It looks to me like it would factor better into "composing with an injective alg_hom is itself injective"

Eric Wieser (May 31 2022 at 10:09):

we have docs#linear_map.cancel_left, but it's not stated in terms of function.injective, and we're also missing the alg_hom version

Kalle Kytölä (Jun 19 2022 at 10:29):

The three results below (two of them special cases of the first) are very common in measure theory and probability theory, but they don't appear to have sufficiently standard recognizable names and I am failing to come up with good mathlib style naming (that is easy for a probabilist/analyst to guess and find), too. These results are in PR #14424, and I'm looking for better names than the ones used in the PR. Help appreciated!

The naming (in math, not in mathlib) has been discussed before. The names "layer cake representation" and "Cavalieri's principle" were pointed out to me then. But my feeling is that very few mathematicians recognize the result with either of those names.

Kalle Kytölä (Jun 19 2022 at 10:29):

  • layercake (the general result): Let μ\mu be a (sigma-finite) measure on XX and f ⁣:X[0,]f \colon X \to [0,\infty] a measurable function. Let ϕ:[0,)[0,)\phi : [0,\infty) \to [0,\infty) be an increasing differentiable function with ϕ(0)=0\phi(0)=0. Then:

X(ϕf)dμ=0ϕ(t)μ{ft}dt.\int_X (\phi \circ f) \, \mathrm{d} \mu = \int_0^\infty \phi'(t) \, \mu \{ f \ge t \} \, \mathrm{d} t .

  • layercake_one (the most common use case): Taking ϕ(t)=t\phi(t) = t, one obtains

Xfdμ=0μ{ft}dt.\int_X f \, \mathrm{d} \mu = \int_0^\infty \mu \{ f \ge t \} \, \mathrm{d} t .

  • layercake_p (another common case for LpL^p considerations): Taking ϕ(t)=tp\phi(t) = t^p, one obtains

Xf(x)pdμ(x)=p  0tp1μ{ft}dt.\int_X f(x)^p \, \mathrm{d} \mu (x) = p \; \int_0^\infty t^{p-1} \, \mu \{ f \ge t \} \, \mathrm{d} t .

Kalle Kytölä (Jun 19 2022 at 10:30):

To facilitate mathlib-style naming, here are the actual types:

theorem layercake (μ : measure α) [sigma_finite μ]
  (f_nn : 0  f) (f_mble : measurable f)
  (g_intble :  t > 0, interval_integrable g volume 0 t)
  (g_nn : ∀ᵐ t (volume.restrict (Ioi 0)), 0  g t) :
  ∫⁻ ω, ennreal.of_real ( t in 0 .. f ω, g t) μ
    = ∫⁻ t in Ioi 0, μ {a : α | t  f a} * ennreal.of_real (g t) :=
sorry
theorem layercake_one (μ : measure α) [sigma_finite μ] (f_nn : 0  f) (f_mble : measurable f) :
  ∫⁻ ω, ennreal.of_real (f ω) μ = ∫⁻ t in Ioi 0, (μ {a : α | t  f a}) :=
sorry
theorem layercake_p (μ : measure α) [sigma_finite μ]
  (f_nn : 0  f) (f_mble : measurable f) {p : } (p_large : 1 < p) :
  ∫⁻ ω, ennreal.of_real ((f ω)^p) μ
    = (ennreal.of_real p) * ∫⁻ t in Ioi 0, (μ {a : α | t  f a}) * ennreal.of_real (t^(p-1)) :=
sorry

Kalle Kytölä (Jun 19 2022 at 10:30):

It turned out that @Jason KY. independently proved and PR'ed the pp:th power case layercake_p in #14769 under the name integral_pow_nonneg_eq_integral_meas_le (minor differences: integral instead of lintegral, and some differences in hypotheses). This option and some inspired by it are included below.

Kalle Kytölä (Jun 19 2022 at 10:30):

/poll What should layercake be called?

layercake
lintegral_primitive_comp_eq_lintegral_measure_le_mul

Kalle Kytölä (Jun 19 2022 at 10:31):

/poll What should layercake_one be called?

layercake_one
lintegral_eq_lintegral_measure_le

Kalle Kytölä (Jun 19 2022 at 10:31):

/poll What should layercake_p be called?

layercake_p
integral_rpow_nonneg_eq_integral_meas_le
lintegral_rpow_comp_eq_lintegral_measure_le
lintegral_rpow_comp_eq_lintegral_measure_le_mul_deriv_rpow

Kalle Kytölä (Jun 19 2022 at 10:51):

(Oops, sorry! The copy-pasted option from Jason's PR had integral. Clearly the lintegral/integral choice will be an uncontroversial part of the naming, so please disregard that difference.)

Kalle Kytölä (Jun 19 2022 at 12:09):

Sorry, my polls are not ideally organized, as there are many components at play at once. The above was meant as a poll about which assumptions (nonnegativity, composition, weighing the second integral by the derivative) need to be indicated by the naming --- or alternatively whether there is a single recognizable name such as "layercake" or "Cavalieri" that could be used instead of specific assumptions. But there are other naming issues at play here...

Kalle Kytölä (Jun 19 2022 at 12:09):

One aspect that I think can be independently chosen from the rest is the following. Jason used the terminology tail probability formula for these, which I think is quite descriptive for probabilists (I might have used complementary cumulative distribution function). Since the component measure_le often might refer to μ s ≤ ... but here refers to μ {a : α | t ≤ f a}, is it better to dub it measure_tail?

Another aspect is abbreviating measure to meas. Versions with meas_les could sound more concise (as well as more contagiouos :rolling_eyes:) than measure_les.

Let me still poll about those separately. (I think opinions about these can be incorporated into the above opinions about which assumptions are the ones that the naming should refer to.)

Kalle Kytölä (Jun 19 2022 at 12:09):

/poll As a component in the names, which one(s) should we prefer?
measure_le
meas_le
measure_tail
meas_tail

Sebastien Gouezel (Jun 19 2022 at 12:33):

My problem with tail is that there is no way to guess it if you don't already know that's is used for this in the library.

Kalle Kytölä (Jun 19 2022 at 14:04):

I might imagine people searching for these results with the substring (l)integral_measure or (l)integral_measure_mul. If so, the tail vs le should only make only a small difference for finding them. On the other hand, some probabilist might actually try tail, measure_tail, or (l)integral_tail as substrings, but I of course fully agree we can't count on that. My mild preference is mainly due to the μ s ≤ ... vs μ {a : α | t ≤ f a} distinction.

Kalle Kytölä (Jun 19 2022 at 14:06):

If tail is not used in the naming, then we should perhaps at least use the term "tail probability" in docstrings --- I suppose the API documentation search will then find this for someone who search using "tail" keywords.

Junyan Xu (Jun 19 2022 at 14:40):

I think you could use "epigraph" or "supergraph" in the name: https://en.wikipedia.org/wiki/Epigraph_(mathematics)

Yaël Dillies (Jun 19 2022 at 14:40):

This is already part of the naming convention: docs#convex_on.convex_epigraph

Yaël Dillies (Jun 19 2022 at 14:41):

See also stuff around docs#quasiconvex, eg. docs#quasiconvex_on.convex_lt

Yury G. Kudryashov (Jul 07 2023 at 13:15):

A common way to find h that conjugates f to g is to consider the sequence h n = g^[-n] ∘ f^[n]. I'm going to add a (probably, small) file about this sequence. How should I call it?
P.S.: Of course, g^[-n] makes no sense, so I'm going to use either g^[n] ∘ f^[n] or (EquivLike.invFun g)^[n] ∘ f^[n].

Yury G. Kudryashov (Jul 07 2023 at 13:24):

@Sebastien Gouezel :up:

Yury G. Kudryashov (Jul 07 2023 at 15:59):

For now, I call it iterIter.

Yury G. Kudryashov (Jul 07 2023 at 15:59):

(and use g^[n] ∘ f^[n])


Last updated: Dec 20 2023 at 11:08 UTC