|
| 1 | +# Inequality of arithmetic and geometric means on the integers |
| 2 | + |
| 3 | +```agda |
| 4 | +{-# OPTIONS --lossy-unification #-} |
| 5 | +
|
| 6 | +module elementary-number-theory.inequality-arithmetic-geometric-means-integers where |
| 7 | +``` |
| 8 | + |
| 9 | +<details><summary>Imports</summary> |
| 10 | + |
| 11 | +```agda |
| 12 | +open import elementary-number-theory.addition-integers |
| 13 | +open import elementary-number-theory.difference-integers |
| 14 | +open import elementary-number-theory.inequality-integers |
| 15 | +open import elementary-number-theory.integers |
| 16 | +open import elementary-number-theory.multiplication-integers |
| 17 | +open import elementary-number-theory.nonnegative-integers |
| 18 | +open import elementary-number-theory.squares-integers |
| 19 | +
|
| 20 | +open import foundation.action-on-identifications-functions |
| 21 | +open import foundation.identity-types |
| 22 | +open import foundation.transport-along-identifications |
| 23 | +``` |
| 24 | + |
| 25 | +</details> |
| 26 | + |
| 27 | +## Idea |
| 28 | + |
| 29 | +The |
| 30 | +{{#concept "arithmetic mean-geometric mean inequality" Disambiguation="on integers" WD="AM-GM inequality" WDID=Q841170 Agda=leq-arithmetic-mean-geometric-mean-ℤ}} |
| 31 | +states that $\sqrt{xy} \leq \frac{x + y}{2}$. We cannot take arbitrary square |
| 32 | +roots in integers, but we can prove the equivalent inequality that |
| 33 | +$4xy \leq (x + y)^2$. |
| 34 | + |
| 35 | +## Proof |
| 36 | + |
| 37 | +```agda |
| 38 | +abstract |
| 39 | + leq-arithmetic-mean-geometric-mean-ℤ : |
| 40 | + (x y : ℤ) → |
| 41 | + leq-ℤ (int-ℕ 4 *ℤ (x *ℤ y)) (square-ℤ (x +ℤ y)) |
| 42 | + leq-arithmetic-mean-geometric-mean-ℤ x y = |
| 43 | + inv-tr |
| 44 | + ( is-nonnegative-ℤ) |
| 45 | + ( equational-reasoning |
| 46 | + square-ℤ (x +ℤ y) -ℤ (int-ℕ 4 *ℤ (x *ℤ y)) |
| 47 | + ＝ |
| 48 | + (square-ℤ x +ℤ (int-ℕ 2 *ℤ (x *ℤ y)) +ℤ square-ℤ y) -ℤ |
| 49 | + (int-ℕ 4 *ℤ (x *ℤ y)) |
| 50 | + by ap (_-ℤ int-ℕ 4 *ℤ (x *ℤ y)) (square-add-ℤ x y) |
| 51 | + ＝ |
| 52 | + (square-ℤ x +ℤ square-ℤ y +ℤ (int-ℕ 2 *ℤ (x *ℤ y))) +ℤ |
| 53 | + (neg-ℤ (int-ℕ 4) *ℤ (x *ℤ y)) |
| 54 | + by |
| 55 | + ap-add-ℤ |
| 56 | + ( right-swap-add-ℤ |
| 57 | + ( square-ℤ x) |
| 58 | + ( int-ℕ 2 *ℤ (x *ℤ y)) |
| 59 | + ( square-ℤ y)) |
| 60 | + ( inv (left-negative-law-mul-ℤ _ _)) |
| 61 | + ＝ |
| 62 | + (square-ℤ x +ℤ square-ℤ y) +ℤ |
| 63 | + (int-ℕ 2 *ℤ (x *ℤ y) +ℤ neg-ℤ (int-ℕ 4) *ℤ (x *ℤ y)) |
| 64 | + by associative-add-ℤ _ _ _ |
| 65 | + ＝ |
| 66 | + (square-ℤ x +ℤ square-ℤ y) +ℤ |
| 67 | + (neg-ℤ (int-ℕ 2) *ℤ (x *ℤ y)) |
| 68 | + by |
| 69 | + ap |
| 70 | + ( square-ℤ x +ℤ square-ℤ y +ℤ_) |
| 71 | + ( inv |
| 72 | + ( right-distributive-mul-add-ℤ |
| 73 | + ( int-ℕ 2) |
| 74 | + ( neg-ℤ (int-ℕ 4)) |
| 75 | + ( x *ℤ y))) |
| 76 | + ＝ (square-ℤ x +ℤ square-ℤ y) -ℤ (int-ℕ 2 *ℤ (x *ℤ y)) |
| 77 | + by |
| 78 | + ap |
| 79 | + ( square-ℤ x +ℤ square-ℤ y +ℤ_) |
| 80 | + ( left-negative-law-mul-ℤ _ (x *ℤ y)) |
| 81 | + ＝ square-ℤ x -ℤ int-ℕ 2 *ℤ (x *ℤ y) +ℤ square-ℤ y |
| 82 | + by right-swap-add-ℤ _ _ _ |
| 83 | + ＝ square-ℤ (x -ℤ y) by inv (square-diff-ℤ x y)) |
| 84 | + ( is-nonnegative-square-ℤ (x -ℤ y)) |
| 85 | +``` |
0 commit comments