refactor(library/algebra/ordered_ring,ordered_field): move theorems from ordered_field to ordered_ring
This commit is contained in:
parent
7d72c9b6b5
commit
51e0d31304
2 changed files with 46 additions and 43 deletions
|
@ -299,17 +299,6 @@ section linear_ordered_field
|
|||
theorem div_two_sub_self (a : A) : a / 2 - a = - (a / 2) :=
|
||||
by rewrite [-{a}add_halves at {2}, sub_add_eq_sub_sub, sub_self, zero_sub]
|
||||
|
||||
theorem nonneg_le_nonneg_of_squares_le (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a ≤ b * b) : a ≤ b :=
|
||||
begin
|
||||
apply le_of_not_gt,
|
||||
intro Hab,
|
||||
let Hposa := lt_of_le_of_lt Hb Hab,
|
||||
let H' := calc
|
||||
b * b ≤ a * b : mul_le_mul_of_nonneg_right (le_of_lt Hab) Hb
|
||||
... < a * a : mul_lt_mul_of_pos_left Hab Hposa,
|
||||
apply (not_le_of_gt H') H
|
||||
end
|
||||
|
||||
theorem add_self_div_two (a : A) : (a + a) / 2 = a :=
|
||||
symm (iff.mpr (!eq_div_iff_mul_eq (ne_of_gt (add_pos zero_lt_one zero_lt_one)))
|
||||
(by rewrite [left_distrib, *mul_one]))
|
||||
|
@ -499,38 +488,6 @@ section discrete_linear_ordered_field
|
|||
assert Heq : a = 0, from eq_of_le_of_ge (le_of_not_gt H) (le_of_not_gt H'),
|
||||
by rewrite [Heq, div_zero, *abs_zero, div_zero])
|
||||
|
||||
theorem sub_le_of_abs_sub_le_left (H : abs (a - b) ≤ c) : b - c ≤ a :=
|
||||
if Hz : 0 ≤ a - b then
|
||||
(calc
|
||||
a ≥ b : (iff.mp !sub_nonneg_iff_le) Hz
|
||||
... ≥ b - c : sub_le_of_nonneg _ _ (le.trans !abs_nonneg H))
|
||||
else
|
||||
(have Habs : b - a ≤ c, by rewrite [abs_of_neg (lt_of_not_ge Hz) at H, neg_sub at H]; apply H,
|
||||
have Habs' : b ≤ c + a, from (iff.mpr !le_add_iff_sub_right_le) Habs,
|
||||
(iff.mp !le_add_iff_sub_left_le) Habs')
|
||||
|
||||
theorem sub_le_of_abs_sub_le_right (H : abs (a - b) ≤ c) : a - c ≤ b :=
|
||||
sub_le_of_abs_sub_le_left (!abs_sub ▸ H)
|
||||
|
||||
theorem abs_sub_square (a b : A) : abs (a - b) * abs (a - b) = a * a + b * b - 2 * a * b :=
|
||||
by rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
|
||||
sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul,
|
||||
*add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
|
||||
|
||||
theorem abs_abs_sub_abs_le_abs_sub (a b : A) : abs (abs a - abs b) ≤ abs (a - b) :=
|
||||
begin
|
||||
apply nonneg_le_nonneg_of_squares_le,
|
||||
repeat apply abs_nonneg,
|
||||
rewrite [*abs_sub_square, *abs_abs, *abs_mul_abs_self],
|
||||
apply sub_le_sub_left,
|
||||
rewrite *mul.assoc,
|
||||
apply mul_le_mul_of_nonneg_left,
|
||||
rewrite -abs_mul,
|
||||
apply le_abs_self,
|
||||
apply le_of_lt,
|
||||
apply two_pos
|
||||
end
|
||||
|
||||
theorem sign_eq_div_abs (a : A) : sign a = a / (abs a) :=
|
||||
decidable.by_cases
|
||||
(suppose a = 0, by subst a; rewrite [zero_div, sign_zero])
|
||||
|
|
|
@ -437,6 +437,17 @@ section
|
|||
... ≤ b * c : mul_le_mul_of_nonneg_left Hc Hb,
|
||||
le_of_mul_le_mul_right H' (lt_of_lt_of_le zero_lt_one Hc)
|
||||
|
||||
theorem nonneg_le_nonneg_of_squares_le {a b : A} (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a ≤ b * b) :
|
||||
a ≤ b :=
|
||||
begin
|
||||
apply le_of_not_gt,
|
||||
intro Hab,
|
||||
let Hposa := lt_of_le_of_lt Hb Hab,
|
||||
let H' := calc
|
||||
b * b ≤ a * b : mul_le_mul_of_nonneg_right (le_of_lt Hab) Hb
|
||||
... < a * a : mul_lt_mul_of_pos_left Hab Hposa,
|
||||
apply (not_le_of_gt H') H
|
||||
end
|
||||
end
|
||||
|
||||
/- TODO: Isabelle's library has all kinds of cancelation rules for the simplifier.
|
||||
|
@ -647,6 +658,41 @@ section
|
|||
|
||||
theorem abs_mul_self (a : A) : abs (a * a) = a * a :=
|
||||
by rewrite [abs_mul, abs_mul_abs_self]
|
||||
|
||||
theorem sub_le_of_abs_sub_le_left (H : abs (a - b) ≤ c) : b - c ≤ a :=
|
||||
if Hz : 0 ≤ a - b then
|
||||
(calc
|
||||
a ≥ b : (iff.mp !sub_nonneg_iff_le) Hz
|
||||
... ≥ b - c : sub_le_of_nonneg _ _ (le.trans !abs_nonneg H))
|
||||
else
|
||||
(have Habs : b - a ≤ c, by rewrite [abs_of_neg (lt_of_not_ge Hz) at H, neg_sub at H]; apply H,
|
||||
have Habs' : b ≤ c + a, from (iff.mpr !le_add_iff_sub_right_le) Habs,
|
||||
(iff.mp !le_add_iff_sub_left_le) Habs')
|
||||
|
||||
theorem sub_le_of_abs_sub_le_right (H : abs (a - b) ≤ c) : a - c ≤ b :=
|
||||
sub_le_of_abs_sub_le_left (!abs_sub ▸ H)
|
||||
|
||||
theorem abs_sub_square (a b : A) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
|
||||
by rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
|
||||
sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul,
|
||||
*add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
|
||||
|
||||
theorem abs_abs_sub_abs_le_abs_sub (a b : A) : abs (abs a - abs b) ≤ abs (a - b) :=
|
||||
begin
|
||||
apply nonneg_le_nonneg_of_squares_le,
|
||||
repeat apply abs_nonneg,
|
||||
rewrite [*abs_sub_square, *abs_abs, *abs_mul_abs_self],
|
||||
apply sub_le_sub_left,
|
||||
rewrite *mul.assoc,
|
||||
apply mul_le_mul_of_nonneg_left,
|
||||
rewrite -abs_mul,
|
||||
apply le_abs_self,
|
||||
apply le_of_lt,
|
||||
apply add_pos,
|
||||
apply zero_lt_one,
|
||||
apply zero_lt_one
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
|
||||
|
|
Loading…
Reference in a new issue