# 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 `finset`

s.

#### 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