theorem abs_basic_properties (x y : ℝ) : (0 ≤ |x| ∧ (|x| = 0 ↔ x = 0)) ∧ |(-x)| = |x| ∧ |x * y| = |x| * |y| ∧ |x| ^ 2 = x ^ 2 ∧ (|x| ≤ y ↔ -y ≤ x ∧ x ≤ y) ∧ -|x| ≤ x ∧ x ≤ |x|

Proposition 1.3.1: (i) |x| ≥ 0, and |x| = 0 if and only if x = 0. (ii) | -x| = |x| for all real x. (iii) |x * y| = |x| * |y| for all real x, y. (iv) |x| ^ 2 = x ^ 2 for all real x. (v) |x| ≤ y if and only if -y ≤ x ∧ x ≤ y. (vi) -(|x|) ≤ x ∧ x ≤ |x| for all real x.

theorem real_abs_add_le (x y : ℝ) : |x + y| ≤ |x| + |y|

Proposition 1.3.2 (Triangle Inequality): For all real numbers x and y, we have |x + y| ≤ |x| + |y|.

theorem real_abs_abs_sub_abs_le (x y : ℝ) : ||x| - |y|| ≤ |x - y|

Corollary 1.3.3: (i) (reverse triangle inequality) For real x, y, | |x| - |y| | ≤ |x - y|. (ii) For real x, y, |x - y| ≤ |x| + |y|.

theorem real_abs_sub_le (x y : ℝ) : |x - y| ≤ |x| + |y|

theorem real_abs_sum_le_sum_abs {n : ℕ} (f : Fin n → ℝ) : |∑ i : Fin n, f i| ≤ ∑ i : Fin n, |f i|

Corollary 1.3.4: For real numbers x_1, x_2, ..., x_n, the absolute value of their sum is at most the sum of their absolute values.

theorem abs_x_le_five_of_mem_interval {x : ℝ} (hx : x ∈ Set.Icc (-1) 5) : |x| ≤ 5

theorem abs_quad_le_linear_in_abs (x : ℝ) : |x ^ 2 - 9 * x + 1| ≤ |x| ^ 2 + 9 * |x| + 1

theorem poly_bound_at_abs_le_five {a : ℝ} (ha0 : 0 ≤ |a|) (ha : |a| ≤ 5) : |a| ^ 2 + 9 * |a| + 1 ≤ 71

theorem abs_quadratic_bound_on_interval (x : ℝ) (hx : x ∈ Set.Icc (-1) 5) : |x ^ 2 - 9 * x + 1| ≤ 71

Example 1.3.5: On the interval [-1, 5], the quadratic x ^ 2 - 9 * x + 1 is bounded in absolute value by 71; that is, a permissible M satisfying |x ^ 2 - 9 * x + 1| ≤ M for all x in this interval is M = 71.

def isBoundedOnReal (D : Set ℝ) (f : ↑D → ℝ) : Prop

Definition 1.3.6: A function f : D → ℝ is bounded if there exists a real M such that |f x| ≤ M for all x ∈ D.

Equations

• isBoundedOnReal D f = ∃ (M : ℝ), ∀ (x : ↑D), |f x| ≤ M

theorem sup_inf_monotone_on_nonempty {D : Set ℝ} (hD : D.Nonempty) {f g : ↑D → ℝ} (hf : isBoundedOnReal D f) (hg : isBoundedOnReal D g) (hfg : ∀ (x : ↑D), f x ≤ g x) : sSup (Set.range f) ≤ sSup (Set.range g) ∧ sInf (Set.range f) ≤ sInf (Set.range g)

Proposition 1.3.7: If f, g : D → ℝ are bounded functions on a nonempty set D with f x ≤ g x for every x ∈ D, then the supremum of the range of f is at most the supremum of the range of g, and the infimum of the range of f is at most the infimum of the range of g.