Grace/Cumulus/Real/MeanInequality.g17

Open in Workbench Download source

Imports

Sqrt · Metric

Declarations

Source

1-- The arithmetic mean of two nonnegative reals is at least their geometric mean2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.MeanInequality8import Sqrt9import Metric1011-- The square of the mean exceeds the product by the square of half the12-- difference, so the product is at most the square of the mean.13theorem realMulValue.le_square_of_mean (a b : Real)14  shows a * b ≤ half(a + b) * half(a + b)15proof16  have doubled := half.add_self at a + b with *17  have square := realMulValue.square_nonnegative_real at a - b with *18  have squareNonnegative := NonnegativeReal.le with square19  have expansion : (a + b) * (a + b) = a * b + a * b + a * b + a * b + (a - b) * (a - b) by ring20  have meanExpansion : (half(a + b) + half(a + b)) * (half(a + b) + half(a + b)) = half(a + b) * half(a + b) + half(a + b) * half(a + b) + half(a + b) * half(a + b) + half(a + b) * half(a + b)21    ring22  rw doubled at meanExpansion23  linarith2425-- Arithmetic mean and geometric mean: √(ab) ≤ (a + b)/2 for nonnegative a, b.26theorem sqrt.le_mean (a b : Real)27  requires nonnegativeA : 0 ≤ a28  requires nonnegativeB : 0 ≤ b29  shows √(a * b) ≤ (a + b) / 230proof31  have aNonnegative := NonnegativeReal.of_le at a with *32  have bNonnegative := NonnegativeReal.of_le at b with *33  have product := NonnegativeReal.mul at a, b with *34  have doubled := half.add_self at a + b with *35  have meanNonnegative : 0 ≤ half(a + b) by linarith36  have meanSquare := realMulValue.square_nonnegative_real at half(a + b) with *37  have bound := realMulValue.le_square_of_mean at a, b with *38  have roots := sqrt.le_of_le at a * b, half(a + b) * half(a + b) with *39  have rootOfSquare := sqrt.of_square at half(a + b) with *40  rw rootOfSquare at roots41  have asQuotient := realDiv.of_double_eq with *42  rwa ← asQuotient43