Naming convention

Stream: general

[Sebastien Gouezel]

How should I name the following theorem? I have tried to follow the naming convention, but it looks longish.

/-- Minkowski inequality: the `L^p` norm satisfies the triangular inequality, i.e.,
`||f+g||_p ≤ ||f||_p + ||g||_p`. Version for sums over finite sets, with nonnegative functions. -/
theorem finset.sum_add_rpow_rpow_inv_le_sum_rpow_rpow_inv_add_sum_rpow_rpow_inv
  {α : Type*} (s : finset α) (f g : α → ℝ) (hf : ∀ x ∈ s, 0 ≤ f x) (hg : ∀ x ∈ s, 0 ≤ g x)
  (p : ℝ) (hp : 1 ≤ p) :
  (∑ i in s, (f i + g i) ^ p)^(1/p) ≤ (∑ i in s, (f i)^p) ^ (1/p) + (∑ i in s, (g i)^p) ^ (1/p)

[Johan Commelin]

You forgot the of_pos_of_pos_of_one_le at the end...

[Johan Commelin]

More serious: how about chopping of everything after the le?

[Reid Barton]

how about lp_sum_le_sum_lp

[Reid Barton]

or something along these lines

[Chris Hughes]

And make the norm into a definition?

[Sebastien Gouezel]

I like lp_sum_le_sum_lp: people who would need this should now what lp is.

[Reid Barton]

lp_norm in place of lp is also possible, it seems short enough still.

[Sebastien Gouezel]

The definition of the norm is coming afterwards, to put a distance on a finite product of metric spaces.

[Sebastien Gouezel]

finset.lp_norm_add_le_add_lp_norm?

[Reid Barton]

or lᵖ_sum_le_sum_lᵖ

[Sebastien Gouezel]

I wouldn't mention the sum in the name, because it's already part of the definition of the norm. And no, superscripts in theorem names are not acceptable.

[Reid Barton]

aw :(

[Sebastien Gouezel]

Of course, this follows from Hölder inequality. Same naming contest for

/-- Hölder inequality: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with nonnegative functions. -/
theorem finset.sum_mul_le_sum_rpow_rpow_inv_mul_sum_rpow_rpow_inv
  {α : Type*} {s : finset α} {f g : α → ℝ} {p q : ℝ}
  (hpq : p.is_conjugate_exponent q) (hf : ∀ x ∈ s, 0 ≤ f x) (hg : ∀ x ∈ s, 0 ≤ g x) :
  (∑ i in s, f i * g i) ≤ (∑ i in s, (f i)^p) ^ (1/p) * (∑ i in s, (g i)^q) ^ (1/q) :=

[Sebastien Gouezel]

finset.sum_mul_le_lp_norm_mul_lq_norm?

[Sebastien Gouezel]

The problem with these names is that they hardcode the exponents p or q. But we do the same with char_p, and since it's completely standard I don't think it's harmful.

[Mario Carneiro]

How about finset.sum_minkowski

[Mario Carneiro]

the name-by-symbols method is only useful if that is the way theorems are being distinguished from each other in a sea of lemmas, like in group.basic. If it is a high level theorem with no similar versions and a complex statement, then people will probably use the name in maths to look it up and so you should use a name based on that. Especially here, where they have well known names

[Sebastien Gouezel]

This is against the holy naming convention that names should follow the sequence of symbols in the statement ! :) More seriously, there are enough theorems by Minkowski that this is not discriminating enough.

[Mario Carneiro]

That's why it's finset.sum_minkowski and not minkowski_ineq

[Mario Carneiro]

The idea here is to put some basic namespacing in, but otherwise use the usual name

[Sebastien Gouezel]

You can lookup Minkowski sum on wikipedia to check that there is a serious ambiguity here :)

[Mario Carneiro]

What are the distinguishing features of this minkowski theorem vs the other ones?

[Mario Carneiro]

whatever they are, put them in the name

[Reid Barton]

It's the one about the $L^p$ norm

[Mario Carneiro]

Well, L^p doesn't come up in the statement, but rpow does, so perhaps finset.sum_rpow_minkowski?

[Mario Carneiro]

Also, I don't think that Minkowski sum will clash here since that is a sum over set not finset

[Sebastien Gouezel]

I would be fine with finset.sum_rpow_holder_of_nonneg and finset.sum_rpow_minkowsi_of_nonneg (where the of_nonneg is necessary to distringuish it from the general version where one takes absolute values).

[Reid Barton]

(You could take a Minkowski sum of a finset of sets though.)

[Mario Carneiro]

That would be a new function, though, which would get its own name or name segment like finset.mink so that it can be used as a name segment in other theorems

[Mario Carneiro]

(not that I'm actually proposing that name)

[Mario Carneiro]

I would probably call it zip_with_add

[Mario Carneiro]

oh wait it's not a zip nvm