Naming contest

Stream: maths

[Yury G. Kudryashov]

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]

Can you show the typeclasses on α and k?

[Adam Topaz]

simplex for the second one?

[Eric Wieser]

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]

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

[Yury G. Kudryashov]

Yes, arrows are finsupps

[Adam Topaz]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

No typeclasses on α, semiring or ring on k.

[Adam Topaz]

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

[Yury G. Kudryashov]

Yes, an ordered semiring for the second one.

[Yury G. Kudryashov]

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]

free_affine and free_convex for names?

[Joseph Myers]

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]

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]

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]

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

[Joseph Myers]

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]

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

[Adam Topaz]

Let $\mathcal{C}$ be a category, $X$ an object of $\mathcal{C}$, and $S$ a set of objects in $\mathcal{C}$.

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

What should this category be called?

[Adam Topaz]

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]

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$ on $S$ -- say $D$ -- and then it's the comma category $(D, X)$.

[Patrick Massot]

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]

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]

exists_strict_mono_forall_of_frequently?

[Patrick Massot]

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]

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]

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

[Adam Topaz]

(Of course! Fixed)

[Adam Topaz]

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

[Bhavik Mehta]

Maybe you can use this to generalise wide equalizers too?

[Adam Topaz]

Yeah, that should be possible

[Adam Topaz]

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]

Umm, sorry not quite.

[Adam Topaz]

I want $\alpha = \beta$ to both be punit, and $\gamma$ arbitrary

[Adam Topaz]

That should give wide euqlizers

[Adam Topaz]

with usual equalizers being $\gamma = fin 2$

[David Wärn]

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]

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]

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]

Is this the right adjoint of filter.comap?

[Yury G. Kudryashov]

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]

filter.cocomap?

[Iván Sadofschi Costa]

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]

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

[Anne Baanen]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

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

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

$$\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 $\phi(t) = t$, one obtains

$$\int_X f \, \mathrm{d} \mu = \int_0^\infty \mu \{ f \ge t \} \, \mathrm{d} t .$$

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

$$\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ä]

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

It turned out that @Jason KY. independently proved and PR'ed the $p$: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ä]

/poll What should layercake be called?

layercake
lintegral_primitive_comp_eq_lintegral_measure_le_mul

[Kalle Kytölä]

/poll What should layercake_one be called?

layercake_one
lintegral_eq_lintegral_measure_le

[Kalle Kytölä]

/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ä]

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

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

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

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

[Sebastien Gouezel]

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

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

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]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Yury G. Kudryashov]

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]

@Sebastien Gouezel :up:

[Yury G. Kudryashov]

For now, I call it iterIter.

[Yury G. Kudryashov]

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