## 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 $\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 (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$ on $S$ -- say $D$ -- and then it's the comma category $(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

Last updated: May 18 2021 at 06:15 UTC