Zulip Chat Archive

Stream: maths

Topic: Naming contest


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 19 2020 at 13:13):

Can you show the typeclasses on α and k?

view this post on Zulip Adam Topaz (Oct 19 2020 at 13:16):

simplex for the second one?

view this post on Zulip 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)

view this post on Zulip 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?)

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 13:19):

Yes, arrows are finsupps

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 13:20):

No typeclasses on α, semiring or ring on k.

view this post on Zulip Adam Topaz (Oct 19 2020 at 13:20):

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

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 13:21):

Yes, an ordered semiring for the second one.

view this post on Zulip 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).

view this post on Zulip Adam Topaz (Oct 19 2020 at 13:22):

free_affine and free_convex for names?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 19:21):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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) .

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Yury G. Kudryashov (Mar 21 2021 at 16:28):

exists_strict_mono_forall_of_frequently?

view this post on Zulip 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