Zulip Chat Archive
Stream: general
Topic: Naming convention
Sebastien Gouezel (Jun 02 2020 at 20:23):
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 (Jun 02 2020 at 20:24):
You forgot the of_pos_of_pos_of_one_le
at the end...
Johan Commelin (Jun 02 2020 at 20:25):
More serious: how about chopping of everything after the le
?
Reid Barton (Jun 02 2020 at 20:26):
how about lp_sum_le_sum_lp
Reid Barton (Jun 02 2020 at 20:26):
or something along these lines
Chris Hughes (Jun 02 2020 at 20:27):
And make the norm into a definition?
Sebastien Gouezel (Jun 02 2020 at 20:27):
I like lp_sum_le_sum_lp
: people who would need this should now what lp
is.
Reid Barton (Jun 02 2020 at 20:28):
lp_norm
in place of lp
is also possible, it seems short enough still.
Sebastien Gouezel (Jun 02 2020 at 20:28):
The definition of the norm is coming afterwards, to put a distance on a finite product of metric spaces.
Sebastien Gouezel (Jun 02 2020 at 20:29):
finset.lp_norm_add_le_add_lp_norm
?
Reid Barton (Jun 02 2020 at 20:29):
or lᵖ_sum_le_sum_lᵖ
Sebastien Gouezel (Jun 02 2020 at 20:30):
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 (Jun 02 2020 at 20:30):
aw :(
Sebastien Gouezel (Jun 02 2020 at 20:30):
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 (Jun 02 2020 at 20:31):
finset.sum_mul_le_lp_norm_mul_lq_norm
?
Sebastien Gouezel (Jun 02 2020 at 20:32):
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 (Jun 02 2020 at 20:42):
How about finset.sum_minkowski
Mario Carneiro (Jun 02 2020 at 20:44):
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 (Jun 02 2020 at 20:44):
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 (Jun 02 2020 at 20:45):
That's why it's finset.sum_minkowski
and not minkowski_ineq
Mario Carneiro (Jun 02 2020 at 20:45):
The idea here is to put some basic namespacing in, but otherwise use the usual name
Sebastien Gouezel (Jun 02 2020 at 20:45):
You can lookup Minkowski sum on wikipedia to check that there is a serious ambiguity here :)
Mario Carneiro (Jun 02 2020 at 20:46):
What are the distinguishing features of this minkowski theorem vs the other ones?
Mario Carneiro (Jun 02 2020 at 20:46):
whatever they are, put them in the name
Reid Barton (Jun 02 2020 at 20:47):
It's the one about the norm
Mario Carneiro (Jun 02 2020 at 20:48):
Well, L^p doesn't come up in the statement, but rpow does, so perhaps finset.sum_rpow_minkowski
?
Mario Carneiro (Jun 02 2020 at 20:50):
Also, I don't think that Minkowski sum will clash here since that is a sum over set
not finset
Sebastien Gouezel (Jun 02 2020 at 20:50):
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 (Jun 02 2020 at 20:52):
(You could take a Minkowski sum of a finset
of sets though.)
Mario Carneiro (Jun 02 2020 at 20:54):
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 (Jun 02 2020 at 20:55):
(not that I'm actually proposing that name)
Mario Carneiro (Jun 02 2020 at 20:55):
I would probably call it zip_with_add
Mario Carneiro (Jun 02 2020 at 20:55):
oh wait it's not a zip nvm
Last updated: Dec 20 2023 at 11:08 UTC