Inequality of arithmetic and geometric means on the rational numbers

Content created by Louis Wasserman.

Created on 2025-04-25.
Last modified on 2025-07-25.

{-# OPTIONS --lossy-unification #-}

module elementary-number-theory.inequality-arithmetic-geometric-means-rational-numbers where
Imports 
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.additive-group-of-rational-numbers
open import elementary-number-theory.difference-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-rational-numbers
open import elementary-number-theory.nonnegative-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.squares-rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.transport-along-identifications

Idea

The arithmetic mean-geometric mean inequality states that , where that square root is defined. We cannot take arbitrary square roots in rational numbers, but we can prove the equivalent inequality that for all rational numbers.

Proof

opaque
  unfolding mul-ℚ
  unfolding neg-ℚ

  eq-square-sum-minus-four-mul-ℚ-square-diff :
    (x y : ℚ) →
    square-ℚ (x +ℚ y) -ℚ rational-ℕ 4 *ℚ (x *ℚ y) ＝ square-ℚ (x -ℚ y)
  eq-square-sum-minus-four-mul-ℚ-square-diff x y =
    equational-reasoning
      square-ℚ (x +ℚ y) -ℚ rational-ℕ 4 *ℚ (x *ℚ y)
      ＝
        ((square-ℚ x +ℚ rational-ℕ 2 *ℚ (x *ℚ y)) +ℚ square-ℚ y) -ℚ
        rational-ℕ 4 *ℚ (x *ℚ y)
        by
          ap
            ( _-ℚ rational-ℕ 4 *ℚ (x *ℚ y))
            ( square-add-ℚ x y)
      ＝
        ((square-ℚ x +ℚ square-ℚ y) +ℚ
        rational-ℕ 2 *ℚ (x *ℚ y)) -ℚ
        rational-ℕ 4 *ℚ (x *ℚ y)
        by
          ap
            ( _-ℚ rational-ℕ 4 *ℚ (x *ℚ y))
            ( right-swap-add-ℚ
              ( square-ℚ x)
              ( rational-ℕ 2 *ℚ (x *ℚ y))
              ( square-ℚ y))
      ＝
        (square-ℚ x +ℚ square-ℚ y) +ℚ
        (rational-ℕ 2 *ℚ (x *ℚ y) -ℚ rational-ℕ 4 *ℚ (x *ℚ y))
        by
          associative-add-ℚ
            ( square-ℚ x +ℚ square-ℚ y)
            ( rational-ℕ 2 *ℚ (x *ℚ y))
            ( neg-ℚ (rational-ℕ 4 *ℚ (x *ℚ y)))
      ＝
        (square-ℚ x +ℚ square-ℚ y) +ℚ
        ((rational-ℕ 2 -ℚ rational-ℕ 4) *ℚ (x *ℚ y))
        by
          ap
            ( square-ℚ x +ℚ square-ℚ y +ℚ_)
            ( inv (right-distributive-mul-diff-ℚ _ _ _))
      ＝
        (square-ℚ x +ℚ square-ℚ y) +ℚ
        (rational-ℤ (neg-ℤ (int-ℕ 2)) *ℚ (x *ℚ y))
        by
          ap
            ( square-ℚ x +ℚ square-ℚ y +ℚ_)
            ( ap
              ( _*ℚ (x *ℚ y))
              (diff-rational-ℤ _ _))
      ＝
        (square-ℚ x +ℚ square-ℚ y) -ℚ
        (rational-ℕ 2 *ℚ (x *ℚ y))
        by
          ap
            ( square-ℚ x +ℚ square-ℚ y +ℚ_)
            ( left-negative-law-mul-ℚ _ _)
      ＝ square-ℚ x -ℚ (rational-ℕ 2 *ℚ (x *ℚ y)) +ℚ square-ℚ y
        by
          right-swap-add-ℚ
            ( square-ℚ x)
            ( square-ℚ y)
            ( neg-ℚ (rational-ℕ 2 *ℚ (x *ℚ y)))
      ＝ square-ℚ (x -ℚ y) by inv (square-diff-ℚ x y)

  leq-geometric-mean-arithmetic-mean-ℚ :
    (x y : ℚ) →
    leq-ℚ (rational-ℕ 4 *ℚ (x *ℚ y)) (square-ℚ (x +ℚ y))
  leq-geometric-mean-arithmetic-mean-ℚ x y =
    leq-is-nonnegative-diff-ℚ
      ( rational-ℕ 4 *ℚ (x *ℚ y))
      ( square-ℚ (x +ℚ y))
      ( inv-tr
        ( is-nonnegative-ℚ)
        ( eq-square-sum-minus-four-mul-ℚ-square-diff x y)
        ( is-nonnegative-square-ℚ (x -ℚ y)))

The arithmetic and geometric means of x and y are equal if and only if x = y

abstract
  eq-eq-geometric-mean-arithmetic-mean-ℚ :
    (x y : ℚ) → rational-ℕ 4 *ℚ (x *ℚ y) ＝ square-ℚ (x +ℚ y) → x ＝ y
  eq-eq-geometric-mean-arithmetic-mean-ℚ x y 4xy=⟨x+y⟩² =
    eq-is-zero-diff-ℚ
      ( x)
      ( y)
      ( is-zero-square-is-zero-ℚ
        ( x -ℚ y)
        ( equational-reasoning
          square-ℚ (x -ℚ y)
          ＝ square-ℚ (x +ℚ y) -ℚ rational-ℕ 4 *ℚ (x *ℚ y)
            by inv (eq-square-sum-minus-four-mul-ℚ-square-diff x y)
          ＝ zero-ℚ by is-zero-diff-ℚ (inv 4xy=⟨x+y⟩²)))

  eq-geometric-mean-arithmetic-mean-eq-ℚ :
    (x y : ℚ) → x ＝ y → rational-ℕ 4 *ℚ (x *ℚ y) ＝ square-ℚ (x +ℚ y)
  eq-geometric-mean-arithmetic-mean-eq-ℚ x .x refl =
    inv
      ( equational-reasoning
        square-ℚ (x +ℚ x)
        ＝ square-ℚ (rational-ℕ 2 *ℚ x) by ap square-ℚ (inv (mul-two-ℚ x))
        ＝ square-ℚ (rational-ℕ 2) *ℚ square-ℚ x
          by distributive-square-mul-ℚ _ _
        ＝ rational-ℕ 4 *ℚ square-ℚ x
          by ap (_*ℚ square-ℚ x) (mul-rational-ℕ 2 2))

  eq-geometric-mean-arithmetic-mean-iff-eq-ℚ :
    (x y : ℚ) → (rational-ℕ 4 *ℚ (x *ℚ y) ＝ square-ℚ (x +ℚ y)) ↔ (x ＝ y)
  pr1 (eq-geometric-mean-arithmetic-mean-iff-eq-ℚ x y) =
    eq-eq-geometric-mean-arithmetic-mean-ℚ x y
  pr2 (eq-geometric-mean-arithmetic-mean-iff-eq-ℚ x y) =
    eq-geometric-mean-arithmetic-mean-eq-ℚ x y

Recent changes