Inequalities in ordered fields

This file records a bound on a sum of two reciprocals in a linearly ordered field. It turns a lower bound on a reciprocal sum 1 / b + 1 / c with b ≤ c into an upper bound on the smaller denominator b; the classifications of sorted triangle-group signatures use it to bound their second parameter.

It also records an a priori bound from a difference of two quadratic penalties b² / (2τ) - a² / (2τ₀) with τ < τ₀: if a ≤ R + b, a bound on this difference bounds a. This is the arithmetic behind the equicoercivity of penalized energies in Moreau–Yosida regularization.

It records that for 0 < d, 0 < a and e < a, the time d * e / a lies strictly before d; this is where a timed piece of duration d running across [0, a] reaches e.

It also records how to remove a term ε * C from a bound valid for every ε ∈ (0, δ₀], and how to transfer bounds from maximizers of f + εw when the barrier w is bounded above.

Finally, it records the rescaling identity q |q x - m| = q² |x - m / q| for q > 0, which converts between the two usual forms of an approximation x ≈ m / q.

It also records a perturbation bound for quotients, |x / a - y / b| ≤ 2 (e + y δ) / b when (1 - δ) b ≤ a ≤ b, δ ≤ 1 / 2 and |x - y| ≤ e, the comparison 2 t / (t² + ρ²) ≤ (2 t / r) (2 r / (r² + ρ²)) for 0 < t, 0 < r ≤ ρ, which compares the profiles 2 t / (t² + ρ²) of two scales t and r outside the radius r, and the clearing bound a * b ≤ 1 from a ≤ (1 + b)⁻¹ for 0 ≤ b, and an error-budget bound: if 0 ≤ ε, 0 < K and K dominates a + b then ε / (2 K) * a + b * (ε / (2 K)) ≤ ε / 2. It also records the absorption bound C (K₀ + N) ≤ 2 C (1 + γ) (K + N) from K₀ + N = K + γ N + 2 β e H, H ≤ C (K₀ + N) and 2 C β e H ≤ H / 2, together with the bookkeeping bound C (M + N P + N) ≤ C (1 + P) (M + N) for nonnegative C, M and P.

Finally, it records a polynomial barrier bound: if r ≤ M, 0 < ε, 1 ≤ c and n is larger than M / ε, then the barrier ε * (c * (1 + n ^ 2)) exceeds r.

It also records that |p| * (C₀ * (Lam / lam)) ≤ A follows from |p| ≤ A / (C₀ + 1) * (lam / Lam), the choice of exponent range in an estimate where p is multiplied by a constant C₀ times a ratio Lam / lam of ellipticity bounds.

It further records the power inequality L * r ^ (n - 1) ≤ 2 ^ (n + 1) * ((m + 1) * (r / 2) ^ n) from L / (2 r) < m + 1, which bounds the volume of a convex set containing a ball and a point.

It also records how to bound a sum U + Y from U ≤ 2 Z + 2 M² Y and c / 2 * Y ≤ a Z + b W: solve the second estimate for Y and substitute it into the first.

It also records that the normalized position (c - a) / (b - a) of a point c ∈ [a, b] lies in [0, 1], also when the interval is degenerate, and that for a finite family of nonnegative elements the sum 1 + ∑ i ∈ s, (x i)⁻¹ is positive and bounds each reciprocal (x j)⁻¹.

Main results

• TauCeti.le_of_forall_mem_Ioc_mul_le: if a ≤ m + ε * C for every ε ∈ (0, δ₀], then a ≤ m.
• BddAbove.le_of_forall_pos_exists_add_mul_le: transfer a bound at maximizers of f + εw to f when w is bounded above.
• TauCeti.one_div_add_one_div_le_two_div: for 0 < b ≤ c, the sum 1 / b + 1 / c is at most 2 / b.
• TauCeti.le_of_sq_div_sub_sq_div_le: an upper bound on a from a ≤ R + b and an upper bound on b² / (2τ) - a² / (2τ₀), for 0 < τ < τ₀.
• TauCeti.mul_div_lt_self: d * e / a < d for 0 < d, 0 < a and e < a.
• TauCeti.mul_abs_mul_sub_eq_sq_mul_abs_sub_div: q |q x - m| = q² |x - m / q| for q > 0.
• TauCeti.abs_div_sub_div_le: |x / a - y / b| ≤ 2 (e + y δ) / b for a relative perturbation (1 - δ) b ≤ a ≤ b of the denominator with δ ≤ 1 / 2 and |x - y| ≤ e.
• TauCeti.two_mul_div_add_sq_le_mul: 2 t / (t² + ρ²) ≤ (2 t / r) (2 r / (r² + ρ²)) for 0 < t and 0 < r ≤ ρ.
• TauCeti.mul_le_one_of_le_inv_one_add: a * b ≤ 1 for 0 ≤ b and a ≤ (1 + b)⁻¹.
• TauCeti.pow_five_lt_of_mul_div_le: ε ^ 5 < g from 0 < ε, ε * n ^ 2 < M, 0 < D ≤ n ^ 2 and ε ^ 2 * ε ^ 2 * (M / D) ≤ g.
• TauCeti.mul_le_of_le_div_mul: x * (C₀ * (Lam / lam)) ≤ A from x ≤ A / (C₀ + 1) * (lam / Lam), for 0 ≤ A, 0 ≤ C₀, 0 ≤ lam and 0 ≤ Lam.
• TauCeti.sub_mul_mul_one_add_sq_neg_of_lt: the strict inequality r - ε * (c * (1 + n ^ 2)) < 0 for r ≤ M, 0 < ε, 1 ≤ c and M / ε < n.
• TauCeti.sub_div_sub_mem_Icc: (c - a) / (b - a) ∈ [0, 1] for c ∈ [a, b].
• TauCeti.one_add_sum_inv_pos, TauCeti.inv_le_one_add_sum_inv: for nonnegative x i, 0 < 1 + ∑ i ∈ s, (x i)⁻¹ and (x j)⁻¹ ≤ 1 + ∑ i ∈ s, (x i)⁻¹ for j ∈ s.
• TauCeti.div_mul_add_mul_div_le_half: ε / (2 K) * a + b * (ε / (2 K)) ≤ ε / 2 when 0 ≤ ε, 0 < K and a + b ≤ K.
• TauCeti.mul_pow_le_two_pow_mul_succ_mul_pow: L * r ^ (n - 1) ≤ 2 ^ (n + 1) * ((m + 1) * (r / 2) ^ n) for 0 < r, 1 ≤ n and L / (2 r) < m + 1.
• TauCeti.add_le_mul_add_mul_of_le_of_le: U + Y ≤ (2 + (2 M² + 1) (2 / c) (a + b)) (Z + W) from U ≤ 2 Z + 2 M² Y and c / 2 * Y ≤ a Z + b W.
• TauCeti.le_two_mul_of_le_add_mul: J ≤ 2 * Y from J ≤ Y + X * J, X ≤ 1 / 2 and 0 ≤ J.

theorem TauCeti.le_of_forall_mem_Ioc_mul_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a m C δ₀ : α} (hδ₀ : 0 < δ₀) (h : ∀ ε ∈ Set.Ioc 0 δ₀, a ≤ m + ε * C) : a ≤ m

If a ≤ m + ε * C for every ε ∈ (0, δ₀], then a ≤ m. No sign assumption on C is needed.

theorem TauCeti.le_of_forall_pos_mul_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a m C : α} (h : ∀ (ε : α), 0 < ε → a ≤ m + ε * C) : a ≤ m

If a ≤ m + ε * C for every positive ε, then a ≤ m. No sign assumption on C is needed.

theorem TauCeti.one_div_add_one_div_le_two_div {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {b c : α} (hb : 0 < b) (hbc : b ≤ c) : 1 / b + 1 / c ≤ 2 / b

For 0 < b ≤ c, the sum 1 / b + 1 / c is at most 2 / b.

theorem TauCeti.le_of_sq_div_sub_sq_div_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {τ τ₀ a b R D : α} (hτ : 0 < τ) (hττ₀ : τ < τ₀) (hR : 0 ≤ R) (hab : a ≤ R + b) (h : b ^ 2 / (2 * τ) - a ^ 2 / (2 * τ₀) ≤ D) : a ≤ R + 1 + (2 * τ₀ * R + 2 * τ * τ₀ * |D|) / (τ₀ - τ)

If a ≤ R + b and b² / (2τ) - a² / (2τ₀) ≤ D with 0 < τ < τ₀ and R ≥ 0, then a is bounded by a constant depending only on R, D, τ and τ₀.

theorem TauCeti.mul_div_lt_self {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {d e a : α} (hd : 0 < d) (ha : 0 < a) (hea : e < a) : d * e / a < d

For 0 < d, 0 < a and e < a, scaling d by the fraction e / a < 1 gives d * e / a < d.

theorem TauCeti.mul_abs_mul_sub_eq_sq_mul_abs_sub_div {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {q : α} (hq : 0 < q) (x m : α) : q * |q * x - m| = q ^ 2 * |x - m / q|

The rescaling identity q |q x - m| = q ^ 2 |x - m / q| for q > 0.

theorem TauCeti.abs_div_sub_div_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {x y a b e δ : α} (hb : 0 < b) (hy : 0 ≤ y) (hδ : δ ≤ 1 / 2) (hab : (1 - δ) * b ≤ a) (hab' : a ≤ b) (hxy : |x - y| ≤ e) : |x / a - y / b| ≤ 2 * (e + y * δ) / b

A perturbation estimate for quotients: if (1 - δ) b ≤ a ≤ b with δ ≤ 1 / 2 and |x - y| ≤ e, then |x / a - y / b| ≤ 2 (e + y δ) / b.

theorem TauCeti.two_mul_div_add_sq_le_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {t r ρ : α} (ht : 0 < t) (hr : 0 < r) (hρ : r ≤ ρ) : 2 * t / (t ^ 2 + ρ ^ 2) ≤ 2 * t / r * (2 * r / (r ^ 2 + ρ ^ 2))

For 0 < t and 0 < r ≤ ρ, the profile 2 t / (t² + ρ²) of scale t is at most 2 t / r times the profile 2 r / (r² + ρ²) of scale r.

theorem TauCeti.mul_le_one_of_le_inv_one_add {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 ≤ b) (ha : a ≤ (1 + b)⁻¹) : a * b ≤ 1

If 0 ≤ b and a ≤ (1 + b)⁻¹, then a * b ≤ 1.

theorem TauCeti.sub_mul_mul_one_add_sq_neg_of_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c ε M r n : α} (hc : 1 ≤ c) (hε : 0 < ε) (hr : r ≤ M) (hn : M / ε < n) : r - ε * (c * (1 + n ^ 2)) < 0

The barrier ε * (c * (1 + n ^ 2)) dominates an upper bound r ≤ M once the radius n exceeds M / ε, for c ≥ 1 and ε > 0.

theorem TauCeti.sub_div_sub_mem_Icc {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c ∈ Set.Icc a b) : (c - a) / (b - a) ∈ Set.Icc 0 1

The normalized position (c - a) / (b - a) of a point c ∈ [a, b] lies in [0, 1]. For a degenerate interval a = b it is 0.

theorem TauCeti.one_add_sum_inv_pos {α : Type u_1} {ι : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {s : Finset ι} {x : ι → α} (h : ∀ i ∈ s, 0 ≤ x i) : 0 < 1 + ∑ i ∈ s, (x i)⁻¹

For a finite family of nonnegative elements, 1 + ∑ i ∈ s, (x i)⁻¹ is positive.

theorem TauCeti.inv_le_one_add_sum_inv {α : Type u_1} {ι : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {s : Finset ι} {x : ι → α} (h : ∀ i ∈ s, 0 ≤ x i) {j : ι} (hj : j ∈ s) : (x j)⁻¹ ≤ 1 + ∑ i ∈ s, (x i)⁻¹

For a finite family of nonnegative elements, each reciprocal (x j)⁻¹ with j ∈ s is at most 1 + ∑ i ∈ s, (x i)⁻¹.

theorem TauCeti.pow_five_lt_of_mul_div_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {ε M D n g : α} (hε : 0 < ε) (hD : 0 < D) (hDn : D ≤ n ^ 2) (hbad : ε * n ^ 2 < M) (hgain : ε ^ 2 * ε ^ 2 * (M / D) ≤ g) : ε ^ 5 < g

If 0 < ε, ε * n ^ 2 < M, 0 < D ≤ n ^ 2 and ε ^ 2 * ε ^ 2 * (M / D) ≤ g, then ε ^ 5 < g: the gain ε² ε² M / D exceeds ε⁵.

theorem TauCeti.div_mul_add_mul_div_le_half {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b K ε : α} (hε : 0 ≤ ε) (hK0 : 0 < K) (hK : a + b ≤ K) : ε / (2 * K) * a + b * (ε / (2 * K)) ≤ ε / 2

The error budget: for 0 ≤ ε and 0 < K dominating a + b, the two error terms ε / (2 K) * a and b * (ε / (2 K)) sum to at most ε / 2.

theorem TauCeti.mul_le_of_le_div_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {A C₀ lam Lam x : α} (hA : 0 ≤ A) (hC₀ : 0 ≤ C₀) (hlam : 0 ≤ lam) (hLam : 0 ≤ Lam) (hx : x ≤ A / (C₀ + 1) * (lam / Lam)) : x * (C₀ * (Lam / lam)) ≤ A

If x ≤ A / (C₀ + 1) * (lam / Lam) for A ≥ 0, C₀ ≥ 0, lam ≥ 0 and Lam ≥ 0, then x * (C₀ * (Lam / lam)) ≤ A.

theorem TauCeti.mul_pow_le_two_pow_mul_succ_mul_pow {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {L r : α} {m n : ℕ} (hr : 0 < r) (hn : 1 ≤ n) (hm : L / (2 * r) < ↑m + 1) : L * r ^ (n - 1) ≤ 2 ^ (n + 1) * ((↑m + 1) * (r / 2) ^ n)

The inequality behind the volume bound for a convex set containing a ball and a point: if L / (2 r) < m + 1 then L * r ^ (n - 1) ≤ 2 ^ (n + 1) * ((m + 1) * (r / 2) ^ n).

theorem TauCeti.add_le_mul_add_mul_of_le_of_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {U Y Z W M a b c : α} (hc : 0 < c) (ha : 0 ≤ a) (hb : 0 ≤ b) (hZ : 0 ≤ Z) (hW : 0 ≤ W) (hX : U ≤ 2 * Z + 2 * M ^ 2 * Y) (hY : c / 2 * Y ≤ a * Z + b * W) : U + Y ≤ (2 + (2 * M ^ 2 + 1) * (2 / c) * (a + b)) * Z + (2 + (2 * M ^ 2 + 1) * (2 / c) * (a + b)) * W

If U ≤ 2 Z + 2 M² Y and c / 2 * Y ≤ a Z + b W, where a, b ≥ 0, c > 0 and Z, W ≥ 0, then U + Y ≤ (2 + (2 M² + 1) (2 / c) (a + b)) (Z + W).

theorem TauCeti.le_two_mul_of_le_add_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {J X Y : α} (hJ : 0 ≤ J) (hX : X ≤ 1 / 2) (h : J ≤ Y + X * J) : J ≤ 2 * Y

Absorbing the term X * J with X ≤ 1 / 2 into the left side: J ≤ Y + X * J gives J ≤ 2 * Y for 0 ≤ J.

theorem TauCeti.mul_add_mul_add_le_mul_one_add_mul_add {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {C M N P : R} (hC : 0 ≤ C) (hM : 0 ≤ M) (hP : 0 ≤ P) : C * (M + N * P + N) ≤ C * (1 + P) * (M + N)

The bookkeeping bound C (M + N P + N) ≤ C (1 + P) (M + N) for nonnegative C, M and P.

theorem TauCeti.mul_add_le_two_mul_one_add_mul_add {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {C K N γ β e H K₀ : R} (hC : 0 ≤ C) (hK : 0 ≤ K) (hN : 0 ≤ N) (hγ : 0 ≤ γ) (hK₀ : K₀ + N = K + γ * N + 2 * β * e * H) (hHle : H ≤ C * (K₀ + N)) (habs : 2 * C * β * e * H ≤ 1 / 2 * H) : C * (K₀ + N) ≤ 2 * C * (1 + γ) * (K + N)

The absorption step of an a priori estimate: if K₀ + N = K + γ N + 2 β e H, with H ≤ C (K₀ + N) and 2 C β e H ≤ H / 2, then C (K₀ + N) ≤ 2 C (1 + γ) (K + N), for nonnegative C, K, N and γ.

theorem BddAbove.le_of_forall_pos_exists_add_mul_le {X : Type u_1} {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {K : Set X} {w : X → α} (hw : BddAbove (w '' K)) {f : X → α} {m : α} {x : X} (H : ∀ (ε : α), 0 < ε → ∃ z ∈ K, f x + ε * w x ≤ f z + ε * w z ∧ f z ≤ m) : f x ≤ m

If w is bounded above on K and every positive ε admits a point z ∈ K with f z ≤ m and f x + ε * w x ≤ f z + ε * w z, then f x ≤ m. No sign condition on the barrier or its upper bound is needed.