A sixth-power bound by a maximum #
For elements x, y of a linearly ordered commutative monoid (for instance the natural numbers),
the product (x * y) ^ 6 is at most (max (x ^ 3) (y ^ 2)) ^ 5
(TauCeti.mul_pow_six_le_max_pow_five). Consequently a bound g * R ≤ K * (x * y * N) gives
(g * R) ^ 6 ≤ K ^ 6 * (max (x ^ 3) (y ^ 2)) ^ 5 * N ^ 6 (TauCeti.pow_six_le_of_le_mul), the
sixth-power bookkeeping of the estimates of a Weierstrass invariant pair (c₄, c₆) against
max (|c₄| ^ 3, c₆ ^ 2).
theorem
TauCeti.mul_pow_six_le_max_pow_five
{α : Type u_1}
[CommMonoid α]
[LinearOrder α]
[IsOrderedMonoid α]
(x y : α)
:
In a linearly ordered commutative monoid, (x * y) ^ 6 ≤ (max (x ^ 3) (y ^ 2)) ^ 5.
theorem
TauCeti.pow_six_le_of_le_mul
{α : Type u_1}
[CommMonoid α]
[LinearOrder α]
[IsOrderedMonoid α]
{x y N g R K : α}
(h : g * R ≤ K * (x * y * N))
:
A bound g * R ≤ K * (x * y * N) bounds (g * R) ^ 6 by K ^ 6 * M ^ 5 * N ^ 6, where
M = max (x ^ 3) (y ^ 2).