Help wanted: proof in `Nat.nthRoot`

Stream: mathlib4

[Yury G. Kudryashov]

In #28768 I define Nat.nthRoot and prove its correctness. Currently, the proof depends on AM-GM for real numbers. It would be nice to rewrite the proof without dependency on real numbers so that we can move the definition to Batteries. Any ideas? One possible approach is to prove the AM-GM inequality in the form of n ^ n * ∏ i, a i ≤ (∑ i, a i) ^ n for rational numbers (in case of Mathlib - for ordered semirings). Any other ideas?

[Yaël Dillies]

I think this ordered semiring AM-GM idea is best

[Violeta Hernández]

I attempted to prove this form of AM-GM about a year ago but I never really finished the proof. It'd be great to have!

[Aaron Liu]

is it true in ordered semirings too? I can try proving it

[Aaron Liu]

I guess it would have to be a commsemiring for finset mul

[Aaron Liu]

ok I believe it now

[Aaron Liu]

for a linear order I believe it

[Yaël Dillies]

This should be a consequence of the rearrangement inequality, which we have in both binary and finitary forms

[Yury G. Kudryashov]

Don't we need it for k tuples for this?

[Yury G. Kudryashov]

Another option is to prove https://en.wikipedia.org/wiki/Muirhead's_inequality for an ordered (semi?)ring. Probably, the SemiRing version will need something like ExistsAddOfLE.

[Yury G. Kudryashov]

@Yaël Dillies Do you know a proof of AM-GM with the rearrangement inequality that doesn't rely on existence of the n-th root or division?

[Darij Grinberg]

What version of AM-GM?

[Darij Grinberg]

This https://arxiv.org/abs/1206.5783 gives very nice completely general proofs of various basic inequalities including Muirhead and thus AM-GM (for any ordered field and probably even for most ordered rings). Some reliance on dominance order combinatorics is used

[Darij Grinberg]

Incidentally, ordered semirings or ordered rings aren't the right place to do this in. You want all squares to be nonnegative at least, but for some purposes also division by 1,2,3,...

[Yury G. Kudryashov]

I need $n^n\prod_{i=1}^n a_i \le \left(\sum_{i=1}^n a_i\right)^n$ for nonnegative $a_i$.

[Yury G. Kudryashov]

E.g., in linearly ordered rings.

[Darij Grinberg]

That should be doable, by the Muirhead inequality (Lemma 2) as proved in the above arxiv paper.
Essentially, for any polynomial f in n variables x_1, x_2, ..., x_n, define R(f) = \sum f(x_{\sigma(1)}, x_{\sigma(2)}, ..., x_{\sigma(n)}). Let [alpha] = R(x^\alpha) for any n-tuple \alpha. The Muirhead inequality says that [\alpha] \geq [\beta] whenever a partition \alpha dominates (= majorizes) a partition \beta. The proof shows this directly for Robin Hood moves, which are known to generate the dominance order (this is probably the most annoying part to formalize). Now to prove AM-GM, expand (\sum x_i)^n by the multinomial formula and notices that each \alpha dominates [1,1,...,1], which is n! x_1 x_2 ... x_n.

[Darij Grinberg]

What is needed is "squares are \geq 0" and "positive integers have inverses and these inverses are positive"

[Yury G. Kudryashov]

I suspect that this inequality should be true without any division.

[Darij Grinberg]

I wonder how easy such an argument is to formalize, given that I plan to be doing combinatorics in Lean myself

[Yury G. Kudryashov]

But I don't have a proof right now.

[Darij Grinberg]

Not sure about this. Things like a^2 + b^2 + c^2 \geq bc + ca + ab seem to require division by 2 for example

[Darij Grinberg]

Actually I would bet that AM-GM for n = 3 requires division by at least 2

[Darij Grinberg]

because RHS - LHS = a^3 + b^3 + c^3 + lower terms, but you will need to sum at least 3 expressions with each containing at least two cubes

[Yury G. Kudryashov]

Probably you're right. I'll think about it later today.

[Darij Grinberg]

Division by 2 is enough for n = 3, and who knows, maybe for general n. That would be an interesting result!

[Yury G. Kudryashov]

Note: IMHO, we can merge #28768 without waiting for a better proof. The norm_num extension won't need the proof, only the definition.

[Darij Grinberg]

Ah, division by 2 is necessary for n = 3. Indeed, if you write a^3 + b^3 + c^3 - 27abc as a sum of "visibly nonnegative" expressions, then these expressions must be of the form fg^2 where f and g are two linear forms (= homogeneous degree-1 polynomials) in a,b,c (why homogeneous? because the leading and the trailing terms cannot cancel due to the positivity). but any such expressions have abc appear with an even coefficient. meanwhile 27 is odd

[Darij Grinberg]

Of course, if you start with a totally ordered ring, then you have more tools at your disposal than "visibly nonnegative", and you don't have to divide

[Yaël Dillies]

Darij Grinberg said:

Actually I would bet that AM-GM for n = 3 requires division by at least 2

Order cancellativity is a cheap way to get division by natural numbers. Therefore you don't need to actually be in a field

[Yaël Dillies]

Oh I see you just said that! :slight_smile:

[Darij Grinberg]

In a totally ordered ring with 2 and n invertible, the "replacement of quantities" proof (eg https://nhsjs.com/wp-content/uploads/2023/09/Induction-Proofs-and-Application-of-the-AM-GM-Inequality.pdf ) is probably the easiest to formalize

[Darij Grinberg]

Formally, you're inducting on k in proving "AM-GM holds for any n numbers such that all but k of them equal their arithmetic mean"

[Aaron Liu]

Darij Grinberg said:

Incidentally, ordered semirings or ordered rings aren't the right place to do this in. You want all squares to be nonnegative at least, but for some purposes also division by 1,2,3,...

what goes wrong without division

[Darij Grinberg]

You get 2(RHS - LHS) = sum of squares but not RHS - LHS = sum of squares

[Aaron Liu]

so in a totally ordered ring

[Aaron Liu]

you don't need division?

[Aaron Liu]

since if RHS - LHS is not nonnegative, then it is negative, so then 2(RHS - LHS) is also negative

[Darij Grinberg]

in a totally ordered, sure
in a partially ordered, though, you do

[Kevin Buzzard]

I've never known what to make of Lean's ordering on the complexes (which needs to be switched on, it's not on by default) which has a<=b iff b-a is a nonnegative real. I argued at the time that this was a pathological thing that should never be in mathlib but the C^* algebra people assured me that it was useful to them so the compromise was that you had to switch it on rather than it being there by default. Does this make the complexes into a partially ordered ring? I'm just trying to get a feeling for these things, I've only ever seen totally ordered rings before.

[Aaron Liu]

Darij Grinberg said:

in a totally ordered, sure
in a partially ordered, though, you do

I don't think you know squares are nonnegative in a partially ordered ring

[Aaron Liu]

Kevin Buzzard said:

I've never known what to make of Lean's ordering on the complexes (which needs to be switched on, it's not on by default) which has a<=b iff b-a is a nonnegative real. I argued at the time that this was a pathological thing that should never be in mathlib but the C^* algebra people assured me that it was useful to them so the compromise was that you had to switch it on rather than it being there by default. Does this make the complexes into a partially ordered ring? I'm just trying to get a feeling for these things, I've only ever seen totally ordered rings before.

import Mathlib

open scoped ComplexOrder

-- @RCLike.toIsStrictOrderedRing ℂ Complex.instRCLike
#synth IsStrictOrderedRing Complex

[Aaron Liu]

my intuition is that partially ordered rings are like totally ordered rings but without the order being total

[Kevin Buzzard]

My instinct of "totally order thing" is "in a line", and maybe I have some kind of instinct about a partially ordered set (some subset of a power set) but I'm not sure I understand partially ordered rings until I've seen some examples, which was why I asked about the complexes.

[Kevin Buzzard]

How many partially ordered ring structures are there on the integers? The rationals?

[Andrew Yang]

The fractional ideals of your favourite number field forms a partially ordered semifield.
And AM-GM is true on it.

[Aaron Liu]

Kevin Buzzard said:

How many partially ordered ring structures are there on the integers? The rationals?

do you want the ones that give you IsOrderedRing or IsStrictOrderedRing

[Aaron Liu]

I think on the integers there's only one

[Aaron Liu]

actually I think in an integral domain IsOrderedRing and IsStrictOrderedRing might be equivalent

[Aaron Liu]

I think over the rationals there's also only one order making it an ordered ring and this is probably related to the fact that Module.finrank Int Rat = 1

[Aaron Liu]

no that's not right

[Aaron Liu]

there's other orders too on the rationals maybe?

[Aaron Liu]

yeah

[Aaron Liu]

there's the order where a<=b iff b-a is a nonnegative integer

[Aaron Liu]

I think you get one of these for every subring of the rationals

[Darij Grinberg]

Sorry, a lot of context here got lost as I wasn't very explicit about it.

AM-GM is definitely false for partially ordered comm rings in general.

I think (see mod-2 argument above) that it is also false for partially ordered comm rings in which squares are \geq 0, at least when n is odd.

But it holds for partially ordered comm rings in which squares are \geq 0 AND 1, 2, ..., n are cancellable from inequalities (that is, ka \geq kb entails a \geq b for k \in [n]). Invertibility is too much to assume, though probably achievable by localization (haven't checked).

In particular, AM-GM holds for totally ordered comm rings.

[Violeta Hernández]

So, what's the Lean statement we want to prove?

[Yury G. Kudryashov]

For Nat.nthRoot, I need docs#Nat.nthRoot.lt_pow_go_succ_aux which follows from, e.g.,

theorem aux (l : List Nat) : l.length ^ l.length * l.prod ≤ l.sum ^ l.length

[Yury G. Kudryashov]

(or a version with Fin n -> R tuples).

[Yury G. Kudryashov]

We need a proof without heavy dependencies.

[Junyan Xu]

1, 2, ..., n are cancellable from inequalities (that is, ka \geq kb entails a \geq b for k \in [n])

docs#MulLeftReflectLE

[Yury G. Kudryashov]

If we want a very precise statement, then we can have the same inequality multiplied by some natural number on both sides.

[Yury G. Kudryashov]

Junyan Xu said:

1, 2, ..., n are cancellable from inequalities (that is, ka \geq kb entails a \geq b for k \in [n])

docs#MulLeftReflectLE

This is a wrong typeclass. It doesn't assume k > 0.

[Snir Broshi]

Yury G. Kudryashov said:

For Nat.nthRoot, I need docs#Nat.nthRoot.lt_pow_go_succ_aux which follows from, e.g.,

theorem aux (l : List Nat) : l.length ^ l.length * l.prod ≤ l.sum ^ l.length

Well apart from the following lemma that is easy to prove over ℤ but not ℕ (although it is true over ℕ since the subtraction is not saturated so the ℤ proof should imply it for ℕ):

import Mathlib
lemma foo {a b c : ℕ} (ha : a ≤ c) (hb : c ≤ b) : a * b ≤ (a + b - c) * c := by
  -- proof over ℤ:
  --   `a ≤ c` → `0 ≤ c - a`
  --   `c ≤ b` → `0 ≤ b - c`
  --   → `0 ≤ (c - a) * (b - c) = cb - cc - ab + ac = (a + b - c) * c - a * b`
  --   → `a * b ≤ (a + b - c) * c`
  sorry

then I've done it:

theorem aux

import Mathlib
theorem aux (l : List ℕ) : l.length ^ l.length * l.prod ≤ l.sum ^ l.length := by
  induction h : l.length generalizing l with
  | zero =>
    cases l
    · simp
    · contradiction
  | succ n ih =>
    cases n with
    | zero =>
      obtain ⟨_, rfl⟩ := l.length_eq_one_iff.mp h
      simp
    | succ n => _
    -- get the minimum of `l` and remove it to create `l₁`
    let min := l.minimum_of_length_pos <| by cutsat
    let l₁ := l.erase min
    have := l.length_erase_add_one <| l.minimum_of_length_pos_mem <| by cutsat
    -- get the maximum of `l₁` and remove it to create `l₂`
    let max := l₁.maximum_of_length_pos <| by cutsat
    let l₂ := l₁.erase max
    have := l₁.length_erase_add_one <| l₁.maximum_of_length_pos_mem <| by cutsat
    -- multiply `l₂` by `n + 2` to create `l₃`
    let l₃ := l₂.map ((n + 2) * ·)
    have := l₂.length_map ((n + 2) * ·)
    -- prepend `x` to `l₃` to create `l₄`
    let x := (n + 2) * (min + max) - l.sum
    let l₄ := x :: l₃
    have := l₃.length_cons (a := x)
    -- induction hypothesis on `l₄`
    have ih := ih l₄ (by cutsat)

    -- upper bound for `min`
    have := l.sum_le_sum (f := fun _ ↦ min) (g := id) (fun i hi ↦ l.minimum_of_length_pos_le_of_mem hi <| by cutsat)
    simp at this
    have min_le : (n + 2) * min ≤ l.sum := by cutsat

    -- lower bound for `max`
    have := l₁.sum_le_sum (f := id) (g := fun _ ↦ max) (fun i hi ↦ l₁.le_maximum_of_length_pos_of_mem hi <| by cutsat)
    simp at this
    have : min ≤ max := l.minimum_of_length_pos_le_of_mem (l.mem_of_mem_erase <| l₁.maximum_of_length_pos_mem <| by cutsat) <| by cutsat
    have max_ge : l.sum ≤ (n + 2) * max := by
      rw [← (show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat)]
      rw [show n + 2 = 1 + l₁.length by cutsat]
      cutsat

    calc
      (n+2) ^ (n+2) * l.prod = (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) := by
        grind [List.prod_erase]
      (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) ≤ (n+2) ^ n * l₂.prod * (x * l.sum) := by
        apply Nat.mul_le_mul_left
        unfold x
        nth_rw 1 [mul_add]
        exact foo min_le max_ge
      (n+2) ^ n * l₂.prod * (x * l.sum) ≤ l.sum ^ (n+2) := by
        have : l₄.sum = (n + 1) * l.sum := calc
          _ = x + l₃.sum := rfl
          _ = x + (n + 2) * l₂.sum := by rw [l₂.sum_map_mul_left]; simp
          _ = x + (n + 2) * (l₁.sum - max) := by simp [← show max + l₂.sum = l₁.sum by exact l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - min - max) := by simp [← show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - (min + max)) := by cutsat
          _ = x + ((n + 2) * l.sum - (n + 2) * (min + max)) := by rw [Nat.mul_sub]
          _ = (n + 1) * l.sum := by
            unfold x
            have : min + l₁.sum = l.sum := l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat
            have : max + l₂.sum = l₁.sum := l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat
            have : min + max ≤ l.sum := by cutsat
            have : (n + 2) * (min + max) ≤ (n + 2) * l.sum := Nat.mul_le_mul_left _ this
            cutsat
        rw [this] at ih
        have := l₂.prod_map_mul (f := fun _ ↦ n + 2) (g := id)
        simp at this
        rw [l₃.prod_cons, this, show l₂.length = n by cutsat, mul_pow] at ih
        have := Nat.mul_le_mul_right l.sum <| Nat.le_of_mul_le_mul_left ih Nat.pow_self_pos
        cutsat

It's a rough translation of a proof from Wikipedia meant for reals/rationals.
It ain't pretty but it works. Anyone up for a game of golf?

[Aaron Liu]

proved a slightly different theorem before realizing I don't know how to conclude your aux from this without nth roots

following mathse

import Mathlib.Algebra.Order.BigOperators.Group.List

-- still not sure if this is left or right
theorem List.zipWith_replicate_right {α : Type u} {β : Type v} {γ : Type w}
    (f : α → β → γ) {l : List α} {n : Nat} (a : β) (hl : l.length = n) :
    l.zipWith f (List.replicate n a) = l.map fun x => f x a := by
  induction n generalizing l with
  | zero =>
    rw [List.length_eq_zero_iff] at hl
    subst hl
    simp
  | succ n ih =>
    cases l with
    | nil => cases hl
    | cons x xs => exact congrArg (List.cons (f x a)) (ih (Nat.succ.inj hl))

theorem aux (l : List Nat) (n : Nat) (hn : l.prod = n ^ l.length) : l.length * n ≤ l.sum := by
  obtain ⟨k, hk⟩ : ∃ k, l.length = k := ⟨l.length, rfl⟩
  induction k generalizing l n with
  | zero =>
    rw [List.length_eq_zero_iff] at hk
    subst hk
    simp
  | succ k ih =>
    cases h₁ : l.max? with
    | none =>
      rw [List.max?_eq_none_iff] at h₁
      subst h₁
      simp
    | some M =>
      rw [List.max?_eq_some_iff] at h₁
      cases h₂ : l.min? with
      | none =>
        rw [List.min?_eq_none_iff] at h₂
        subst h₂
        simp
      | some m =>
        rw [List.min?_eq_some_iff] at h₂
        have s₁ : m ≤ n := by
          apply Nat.le_of_not_lt
          rw [Nat.lt_iff_add_one_le]
          intro h
          have uh : (n + 1) ^ l.length ≤ l.prod :=
            List.pow_card_le_prod l (n + 1) fun x hx =>
              Nat.le_trans h (h₂.right x hx)
          rw [hn, hk, Nat.pow_le_pow_iff_left (Nat.add_one_ne_zero k)] at uh
          exact Nat.not_add_one_le_self n uh
        have s₂ : n ≤ M := by
          apply Nat.le_of_not_lt
          rw [Nat.lt_iff_add_one_le]
          intro h
          have uh : l.prod ≤ (n - 1) ^ l.length :=
            List.prod_le_pow_card l (n - 1) fun x hx =>
              Nat.le_trans (h₁.right x hx) (Nat.sub_le_sub_right h 1)
          rw [hn, hk, Nat.pow_le_pow_iff_left (Nat.add_one_ne_zero k)] at uh
          cases n
          · exact Nat.not_add_one_le_zero M h
          · exact Nat.not_add_one_le_self _ uh
        have s₁₂ : n * n + M * m ≤ (M + m) * n := by
          simp only [← Int.ofNat_le, Int.natCast_add, Int.natCast_mul] at s₁ s₂ ⊢
          rw [← Int.sub_nonneg] at s₁ s₂ ⊢
          have s₁₂ := Int.mul_nonneg s₁ s₂
          simpa [Int.sub_eq_add_neg, Int.add_mul, Int.mul_add, Int.add_assoc,
            Int.add_left_comm, Int.mul_comm, Int.neg_mul, Int.mul_neg, Int.add_comm] using s₁₂
        by_cases hMm : M = m
        · rw [List.sum_eq_card_nsmul l n fun x hx =>
            Nat.le_antisymm ((hMm ▸ h₁.2 x hx).trans s₁) ((hMm ▸ s₂).trans (h₂.2 x hx))]
          rfl
        let il := M * m :: ((l.erase m).erase M).zipWith (· * ·) (List.replicate (k - 1) n)
        have ik : M ∈ l.erase m := (List.mem_erase_of_ne hMm).2 h₁.1
        have cil : ((l.erase m).erase M).length = k - 1 := by
          simp [h₂.1, ik, hk]
        have uk : 1 ≤ k := by
          rw [Nat.one_le_iff_ne_zero]
          rintro rfl
          rw [List.length_eq_one_iff] at hk
          obtain ⟨a, rfl⟩ := hk
          rw [List.mem_singleton] at h₁ h₂
          exact hMm (h₁.1.trans h₂.1.symm)
        have lil : il.length = k := by
          simp [il, cil, uk]
        have hil : il.prod = (n * n) ^ il.length := by
          rw [lil]
          unfold il
          rw [List.prod_cons,
            ← List.prod_mul_prod_eq_prod_zipWith_of_length_eq _ _ (by simpa using cil),
            Nat.mul_right_comm M m, ← Nat.mul_assoc, List.prod_erase ik, Nat.mul_right_comm,
            ← Nat.mul_comm m, List.prod_erase h₂.1, List.prod_replicate, hn, hk, ← Nat.pow_add,
            ← Nat.add_sub_assoc uk, Nat.add_right_comm k, ← Nat.pow_two, ← Nat.pow_mul, Nat.two_mul,
            Nat.add_sub_cancel]
        have oil : il.sum + (M + m) * n = l.sum * n + M * m := by
          unfold il
          rw [List.zipWith_replicate_right (· * ·) n cil,
            ← ZeroHom.coe_mk (· * n) (Nat.zero_mul n),
            ← AddMonoidHom.coe_mk _ (Nat.add_mul · · n),
            List.sum_cons, ← map_list_sum, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
            Nat.add_assoc, ← Nat.add_mul, Nat.add_left_comm, ← Nat.add_assoc,
            List.sum_erase ik, ← Nat.add_comm m, List.sum_erase h₂.1, Nat.add_comm]
        specialize ih il (n * n) hil lil
        have rg := Nat.add_le_add ih s₁₂
        obtain rfl | hpos := Nat.eq_zero_or_pos n
        · simp
        · rwa [oil, ← Nat.add_assoc, lil, ← Nat.add_one_mul,
            ← hk, ← Nat.mul_assoc, Nat.add_le_add_iff_right,
            Nat.mul_le_mul_right_iff hpos] at rg

[Kevin Buzzard]

Snir's missing lemma is

import Mathlib.Algebra.Order.Group.Nat
import Mathlib.Algebra.Ring.Nat

lemma foo {a b c : ℕ} (ha : a ≤ c) (hb : c ≤ b) : a * b ≤ (a + b - c) * c := by
  rw [Nat.add_sub_assoc hb]
  obtain ⟨e, rfl⟩ := Nat.exists_eq_add_of_le hb
  simp [mul_add, mul_comm]
  gcongr

Annoyingly, #min_imports doesn't work on Snir's proof because the cutsat tactic gets better the more you import.

[Aaron Liu]

without any imports

theorem foo {a b c : Nat} (ha : a ≤ c) (hb : c ≤ b) : a * b ≤ (a + b - c) * c := by
  obtain ⟨u₁, rfl⟩ := ha.dest
  obtain ⟨u₂, rfl⟩ := hb.dest
  clear ha hb
  simp only [Nat.mul_add, Nat.sub_mul, Nat.add_mul]
  grind

[Kevin Buzzard]

I think the real question is: what imports does Snir's proof actually use? I am struggling to get two of the cutsat calls succeeding without importing all of Mathlib but clearly we don't need that .

import Mathlib.Algebra.BigOperators.Ring.List
import Mathlib.Algebra.Order.BigOperators.Group.List
import Mathlib.Algebra.Order.Group.Nat
import Mathlib.Algebra.Ring.Nat
import Mathlib.Data.List.MinMax
import Mathlib -- how to get rid of this without making two cutsat's fail? What more needs to be imported?

theorem foo {a b c : Nat} (ha : a ≤ c) (hb : c ≤ b) : a * b ≤ (a + b - c) * c := by
  obtain ⟨u₁, rfl⟩ := ha.dest
  obtain ⟨u₂, rfl⟩ := hb.dest
  clear ha hb
  simp only [Nat.mul_add, Nat.sub_mul, Nat.add_mul]
  grind

theorem aux (l : List ℕ) : l.length ^ l.length * l.prod ≤ l.sum ^ l.length := by
  induction h : l.length generalizing l with
  | zero =>
    cases l
    · simp
    · contradiction
  | succ n ih =>
    cases n with
    | zero =>
      obtain ⟨_, rfl⟩ := l.length_eq_one_iff.mp h
      simp
    | succ n => _
    -- get the minimum of `l` and remove it to create `l₁`
    let min := l.minimum_of_length_pos <| by cutsat
    let l₁ := l.erase min
    have := l.length_erase_add_one <| l.minimum_of_length_pos_mem <| by cutsat
    -- get the maximum of `l₁` and remove it to create `l₂`
    let max := l₁.maximum_of_length_pos <| by cutsat
    let l₂ := l₁.erase max
    have := l₁.length_erase_add_one <| l₁.maximum_of_length_pos_mem <| by cutsat
    -- multiply `l₂` by `n + 2` to create `l₃`
    let l₃ := l₂.map ((n + 2) * ·)
    have := l₂.length_map ((n + 2) * ·)
    -- prepend `x` to `l₃` to create `l₄`
    let x := (n + 2) * (min + max) - l.sum
    let l₄ := x :: l₃
    have := l₃.length_cons (a := x)
    -- induction hypothesis on `l₄`
    have ih := ih l₄ (by cutsat)

    -- upper bound for `min`
    have := l.sum_le_sum (f := fun _ ↦ min) (g := id) (fun i hi ↦ l.minimum_of_length_pos_le_of_mem hi <| by cutsat)
    simp at this
    have min_le : (n + 2) * min ≤ l.sum := by show_term cutsat

    -- lower bound for `max`
    have := l₁.sum_le_sum (f := id) (g := fun _ ↦ max) (fun i hi ↦ l₁.le_maximum_of_length_pos_of_mem hi <| by cutsat)
    simp at this
    have : min ≤ max := l.minimum_of_length_pos_le_of_mem (l.mem_of_mem_erase <| l₁.maximum_of_length_pos_mem <| by cutsat) <| by cutsat
    have max_ge : l.sum ≤ (n + 2) * max := by
      rw [← (show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat)]
      rw [show n + 2 = 1 + l₁.length by cutsat]
      show_term cutsat

    calc
      (n+2) ^ (n+2) * l.prod = (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) := by
        grind [List.prod_erase]
      (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) ≤ (n+2) ^ n * l₂.prod * (x * l.sum) := by
        apply Nat.mul_le_mul_left
        unfold x
        nth_rw 1 [mul_add]
        exact foo min_le max_ge
      (n+2) ^ n * l₂.prod * (x * l.sum) ≤ l.sum ^ (n+2) := by
        have : l₄.sum = (n + 1) * l.sum := calc
          _ = x + l₃.sum := rfl
          _ = x + (n + 2) * l₂.sum := by rw [l₂.sum_map_mul_left]; simp
          _ = x + (n + 2) * (l₁.sum - max) := by simp [← show max + l₂.sum = l₁.sum by exact l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - min - max) := by simp [← show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - (min + max)) := by cutsat
          _ = x + ((n + 2) * l.sum - (n + 2) * (min + max)) := by rw [Nat.mul_sub]
          _ = (n + 1) * l.sum := by
            unfold x
            have : min + l₁.sum = l.sum := l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat
            have : max + l₂.sum = l₁.sum := l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat
            have : min + max ≤ l.sum := by cutsat
            have : (n + 2) * (min + max) ≤ (n + 2) * l.sum := Nat.mul_le_mul_left _ this
            cutsat
        rw [this] at ih
        have := l₂.prod_map_mul (f := fun _ ↦ n + 2) (g := id)
        simp at this
        rw [l₃.prod_cons, this, show l₂.length = n by cutsat, mul_pow] at ih
        have := Nat.mul_le_mul_right l.sum <| Nat.le_of_mul_le_mul_left ih Nat.pow_self_pos
        cutsat

[Aaron Liu]

maybe just prove it manually

[Aaron Liu]

don't rely on the cutsat

[Kevin Buzzard]

Well good luck with that!

[Kevin Buzzard]

The proofs found are aux._proof_1_14 and aux._proof_1_8 so I would imagine that if someone knew what they were doing it might be easy, but I couldn't get it working.

[Aaron Liu]

btw what did #min_imports say

[Kevin Buzzard]

All the other imports in the code I posted above. It was one of those situations where if you tried the output it failed.

[Kevin Buzzard]

oh actually that was before I replaced my foo proof with yours so maybe we can get rid of the nat imports

[Snir Broshi]

The problem was that docs#List.sum_replicate is a simp lemma and it introduced nsmul between two nats, and for some reason simp and cutsat don't know that Nat.cast n = n. The easy fix is to squeeze the simps and use docs#List.sum_replicate_nat instead.

5 imports left

import Mathlib.Algebra.BigOperators.Ring.List
import Mathlib.Algebra.Order.BigOperators.Group.List
import Mathlib.Algebra.Order.Group.Nat
import Mathlib.Algebra.Ring.Nat
import Mathlib.Data.List.MinMax

theorem foo {a b c : Nat} (ha : a ≤ c) (hb : c ≤ b) : a * b ≤ (a + b - c) * c := by
  obtain ⟨u₁, rfl⟩ := ha.dest
  obtain ⟨u₂, rfl⟩ := hb.dest
  grind [Nat.sub_mul]

theorem aux (l : List ℕ) : l.length ^ l.length * l.prod ≤ l.sum ^ l.length := by
  induction h : l.length generalizing l with
  | zero =>
    cases l
    · simp
    · contradiction
  | succ n ih =>
    cases n with
    | zero =>
      obtain ⟨_, rfl⟩ := l.length_eq_one_iff.mp h
      simp
    | succ n => _
    -- get the minimum of `l` and remove it to create `l₁`
    let min := l.minimum_of_length_pos <| by cutsat
    let l₁ := l.erase min
    have := l.length_erase_add_one <| l.minimum_of_length_pos_mem <| by cutsat
    -- get the maximum of `l₁` and remove it to create `l₂`
    let max := l₁.maximum_of_length_pos <| by cutsat
    let l₂ := l₁.erase max
    have := l₁.length_erase_add_one <| l₁.maximum_of_length_pos_mem <| by cutsat
    -- multiply `l₂` by `n + 2` to create `l₃`
    let l₃ := l₂.map ((n + 2) * ·)
    have := l₂.length_map ((n + 2) * ·)
    -- prepend `x` to `l₃` to create `l₄`
    let x := (n + 2) * (min + max) - l.sum
    let l₄ := x :: l₃
    have := l₃.length_cons (a := x)
    -- induction hypothesis on `l₄`
    have ih := ih l₄ (by cutsat)

    -- upper bound for `min`
    have := l.sum_le_sum (f := fun _ ↦ min) (g := id) (fun i hi ↦ l.minimum_of_length_pos_le_of_mem hi <| by cutsat)
    simp only [List.map_const', List.sum_replicate_nat, List.map_id_fun, id_eq] at this
    have min_le : (n + 2) * min ≤ l.sum := by cutsat

    -- lower bound for `max`
    have := l₁.sum_le_sum (f := id) (g := fun _ ↦ max) (fun i hi ↦ l₁.le_maximum_of_length_pos_of_mem hi <| by cutsat)
    simp only [List.map_id_fun, id_eq, List.map_const', List.sum_replicate_nat] at this
    have : min ≤ max := l.minimum_of_length_pos_le_of_mem (l.mem_of_mem_erase <| l₁.maximum_of_length_pos_mem <| by cutsat) <| by cutsat
    have max_ge : l.sum ≤ (n + 2) * max := by
      rw [← (show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat)]
      rw [show n + 2 = 1 + l₁.length by cutsat]
      cutsat

    calc
      (n+2) ^ (n+2) * l.prod = (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) := by
        grind [List.prod_erase]
      (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) ≤ (n+2) ^ n * l₂.prod * (x * l.sum) := by
        apply Nat.mul_le_mul_left
        unfold x
        nth_rw 1 [mul_add]
        exact foo min_le max_ge
      (n+2) ^ n * l₂.prod * (x * l.sum) ≤ l.sum ^ (n+2) := by
        have : l₄.sum = (n + 1) * l.sum := calc
          _ = x + l₃.sum := rfl
          _ = x + (n + 2) * l₂.sum := by rw [l₂.sum_map_mul_left]; simp
          _ = x + (n + 2) * (l₁.sum - max) := by simp [← show max + l₂.sum = l₁.sum by exact l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - min - max) := by simp [← show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - (min + max)) := by cutsat
          _ = x + ((n + 2) * l.sum - (n + 2) * (min + max)) := by rw [Nat.mul_sub]
          _ = (n + 1) * l.sum := by
            unfold x
            have : min + l₁.sum = l.sum := l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat
            have : max + l₂.sum = l₁.sum := l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat
            have : min + max ≤ l.sum := by cutsat
            have : (n + 2) * (min + max) ≤ (n + 2) * l.sum := Nat.mul_le_mul_left _ this
            cutsat
        rw [this] at ih
        have := l₂.prod_map_mul (f := fun _ ↦ n + 2) (g := id)
        simp at this
        rw [l₃.prod_cons, this, show l₂.length = n by cutsat, mul_pow] at ih
        have := Nat.mul_le_mul_right l.sum <| Nat.le_of_mul_le_mul_left ih Nat.pow_self_pos
        cutsat

Other than the much needed golfing of this proof, what's the goal for imports? My guess is that we can do without the first 2, but is that something we want or is importing all of Algebra fine?

[Snir Broshi]

The 1st import, Algebra.BigOperators.Ring.List, is for showing (lst.map (k * ·)).sum = k * lst.sum using docs#List.sum_map_mul_left.

The 2nd import, Algebra.Order.BigOperators.Group.List, is for showing ∀ x ∈ lst, M ≤ x implies lst.length * M ≤ lst.sum using docs#List.sum_le_sum
But it also imports the definition of List.prod, so if we replace that lemma we can only replace the import with Algebra.BigOperators.Group.List.Basic (Algebra.BigOperators instead of Algebra.Order).

The 4th import, Mathlib.Algebra.Ring.Nat, can apparently be removed trivially by replacing docs#mul_add with docs#Nat.mul_add.

Here's the proof with just 2 imports + 3 list lemmas:

2 imports + 3 list lemmas

import Mathlib.Algebra.BigOperators.Group.List.Basic
import Mathlib.Data.List.MinMax

theorem map_mul_sum (k : ℕ) : ∀ lst : List ℕ, (lst.map (k * ·)).sum = k * lst.sum
  | .nil => rfl
  | .cons head tail => by
    have ih := map_mul_sum k tail
    grind
theorem sum_lower_bound {M : ℕ} : ∀ {lst : List ℕ}, (h : ∀ x ∈ lst, M ≤ x) → lst.length * M ≤ lst.sum
  | .nil, h => by simp
  | .cons head tail, h => by
    have := h head List.mem_cons_self
    have ih := sum_lower_bound fun _ hx ↦ h _ <| List.mem_cons_of_mem _ hx
    simp only [List.length_cons]
    grind
theorem sum_upper_bound {M : ℕ} : ∀ {lst : List ℕ}, (h : ∀ x ∈ lst, x ≤ M) → lst.sum ≤ lst.length * M
  | .nil, h => by simp
  | .cons head tail, h => by
    have := h head List.mem_cons_self
    have ih := sum_upper_bound fun _ hx ↦ h _ <| List.mem_cons_of_mem _ hx
    simp only [List.length_cons]
    grind

theorem foo {a b c : Nat} (ha : a ≤ c) (hb : c ≤ b) : a * b ≤ (a + b - c) * c := by
  obtain ⟨u₁, rfl⟩ := ha.dest
  obtain ⟨u₂, rfl⟩ := hb.dest
  grind [Nat.sub_mul]

theorem aux (l : List ℕ) : l.length ^ l.length * l.prod ≤ l.sum ^ l.length := by
  induction h : l.length generalizing l with
  | zero =>
    cases l
    · simp
    · contradiction
  | succ n ih =>
    cases n with
    | zero =>
      obtain ⟨_, rfl⟩ := l.length_eq_one_iff.mp h
      simp
    | succ n => _
    -- get the minimum of `l` and remove it to create `l₁`
    let min := l.minimum_of_length_pos <| by cutsat
    let l₁ := l.erase min
    have := l.length_erase_add_one <| l.minimum_of_length_pos_mem <| by cutsat
    -- get the maximum of `l₁` and remove it to create `l₂`
    let max := l₁.maximum_of_length_pos <| by cutsat
    let l₂ := l₁.erase max
    have := l₁.length_erase_add_one <| l₁.maximum_of_length_pos_mem <| by cutsat
    -- multiply `l₂` by `n + 2` to create `l₃`
    let l₃ := l₂.map ((n + 2) * ·)
    have := l₂.length_map ((n + 2) * ·)
    -- prepend `x` to `l₃` to create `l₄`
    let x := (n + 2) * (min + max) - l.sum
    let l₄ := x :: l₃
    have := l₃.length_cons (a := x)
    -- induction hypothesis on `l₄`
    have ih := ih l₄ (by cutsat)

    -- upper bound for `min`
    have min_le : l.length * min ≤ l.sum := sum_lower_bound fun i hi ↦ l.minimum_of_length_pos_le_of_mem hi <| by cutsat
    rw [show l.length = n + 2 by assumption] at min_le

    -- lower bound for `max`
    have max_ge : l.sum ≤ (n + 2) * max := by
      have : l₁.sum ≤ l₁.length * max := sum_upper_bound fun i hi ↦ l₁.le_maximum_of_length_pos_of_mem hi <| by cutsat
      have : min ≤ max := l.minimum_of_length_pos_le_of_mem (l.mem_of_mem_erase <| l₁.maximum_of_length_pos_mem <| by cutsat) <| by cutsat
      rw [← (show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat)]
      rw [show n + 2 = 1 + l₁.length by cutsat]
      cutsat

    calc
      (n+2) ^ (n+2) * l.prod = (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) := by
        grind [List.prod_erase]
      (n+2) ^ n * l₂.prod * (((n+2)*min) * ((n+2)*max)) ≤ (n+2) ^ n * l₂.prod * (x * l.sum) := by
        apply Nat.mul_le_mul_left
        unfold x
        nth_rw 1 [Nat.mul_add]
        exact foo min_le max_ge
      (n+2) ^ n * l₂.prod * (x * l.sum) ≤ l.sum ^ (n+2) := by
        have : l₄.sum = (n + 1) * l.sum := calc
          _ = x + l₃.sum := rfl
          _ = x + (n + 2) * l₂.sum := by rw [map_mul_sum]
          _ = x + (n + 2) * (l₁.sum - max) := by simp [← show max + l₂.sum = l₁.sum by exact l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - min - max) := by simp [← show min + l₁.sum = l.sum by exact l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat]
          _ = x + (n + 2) * (l.sum - (min + max)) := by cutsat
          _ = x + ((n + 2) * l.sum - (n + 2) * (min + max)) := by rw [Nat.mul_sub]
          _ = (n + 1) * l.sum := by
            unfold x
            have : min + l₁.sum = l.sum := l.sum_erase <| l.minimum_of_length_pos_mem <| by cutsat
            have : max + l₂.sum = l₁.sum := l₁.sum_erase <| l₁.maximum_of_length_pos_mem <| by cutsat
            have : min + max ≤ l.sum := by cutsat
            have : (n + 2) * (min + max) ≤ (n + 2) * l.sum := Nat.mul_le_mul_left _ this
            cutsat
        rw [this] at ih
        have := l₂.prod_map_mul (f := fun _ ↦ n + 2) (g := id)
        simp at this
        rw [l₃.prod_cons, this, show l₂.length = n by cutsat, mul_pow] at ih
        have := Nat.mul_le_mul_right l.sum <| Nat.le_of_mul_le_mul_left ih Nat.pow_self_pos
        cutsat

although it's a bit weird to prove lemmas about lists in a file about nth roots.

I think removing the last 2 imports is pretty much impossible - one is for List.prod so the theorem statement requires it, and the other is for minimum/maximum of lists which the proof itself requires.

[Eric Wieser]

@Yury G. Kudryashov, do we actually care that much about minimizing the imports here?

[Eric Wieser]

My thoughts would be that we obviously want to drop the real numbers from the proof (as we have arleady done), but after that it would almost be better to try and prove this for abstract order / algebra typeclasses, rather than specfically for Nat

[Yury G. Kudryashov]

I agree that we want a proof for some abstract order/algebra typeclasses for Mathlib. However, if/when we move Nat.nthRoot to Batteries, we'll have to port this proof to Nat/Int/Rat.

[Snir Broshi]

Yury G. Kudryashov said:

if/when we move Nat.nthRoot to Batteries

Do you have an alternate statement without List.prod? Otherwise List.prod also has to move back to core/Batteries

[Eric Wieser]

I think moving this to batteries is probably a long way off

[Eric Wieser]

For what it's worth, I had a go at the binary recursion approach:

import Mathlib

/-- An induction principle considering powers of two; to produce `P`,
we need only a mechanism to produce it for powers of `2`,
and for values less than the closest power. -/
def Nat.powTwoRec {P : ℕ → Sort*}
    (pow_two : ∀ k, P (2 ^ k))
    (le_pow_two : ∀ k, P (2 ^ k) → ∀ i < 2 ^ k, P i) : ∀ n, P n := fun n =>
  match hn : n with
  | 0 => le_pow_two 0 (pow_two 0) 0 Nat.zero_lt_one
  | _ + 1 =>
    let k := n.log2
    if h : 2 ^ k = n then
      cast (congrArg P (h.trans hn)) (pow_two k)
    else
      le_pow_two _ (pow_two (k + 1)) _ <| hn.symm.trans_lt Nat.lt_log2_self

-- https://en.wikipedia.org/wiki/AM%E2%80%93GM_inequality#Proof_by_Cauchy_using_forward%E2%80%93backward_induction
theorem cauchy (l : List ℕ) :
    l.length ^ l.length * l.prod ≤ l.sum ^ l.length := by
  induction h : l.length using Nat.powTwoRec generalizing l with
  | pow_two k =>
    induction k using Nat.caseStrongRecOn generalizing l with
    | zero =>
      rw [pow_zero, List.length_eq_one_iff] at h
      obtain ⟨a, rfl⟩ := h
      simp
    | ind k' ik =>
      cases k' with
      | zero =>
        simp [List.length_eq_two] at h
        obtain ⟨a, b, rfl⟩ := h
        suffices 4 * a * b ≤ a^2 + 2 * a * b + b^2 by
          simpa [add_sq, mul_assoc] using this
        have := two_mul_le_add_pow_two a b
        cutsat
      | succ k' =>
        rw [pow_succ] at h
        let +generalize k'' := k' + 1
        let l_left := l.take (2 ^ k'')
        let l_right := l.drop (2 ^ k'')
        have ik_left := ik k'' le_rfl l_left <| by grind
        have ik_right := ik k'' le_rfl l_right <| by grind
        have : l = l_left ++ l_right := List.take_append_drop _ _ |>.symm
        rw [this, List.prod_append, List.sum_append, pow_succ']
        trans 4 ^ 2 ^ k'' * (l_left.sum * l_right.sum) ^ 2 ^ k''
        . have ik_lr := mul_le_mul_left' (mul_le_mul' ik_left ik_right)  (2 ^ (2 * 2 ^ k'')); clear ik_left ik_right
          rw [mul_mul_mul_comm, ← pow_add, ← two_mul, ← pow_succ', ← pow_mul, ← mul_pow] at ik_lr
          convert ik_lr using 1
          · rw [← mul_assoc _ _ (_ * _)]
            congr 1
            simp [← pow_add, mul_pow, ← pow_mul, pow_succ']
          · simp [pow_succ', pow_mul]
        . specialize ik 1 (by cutsat) [l_left.sum, l_right.sum] rfl
          replace ik := Nat.pow_le_pow_left ik (2 ^ k'')
          simpa [← pow_mul, mul_pow 4] using ik
  | le_pow_two k ih i hi =>
    by_cases hls : l.sum = 0
    · rw [hls]
      cases l; · simp_all
      rw [List.sum_eq_zero_iff] at hls
      simp [hls _ List.mem_cons_self, List.prod_cons]
    let l' := l.map (i * ·)
    have hl's : l'.sum = i * l.sum := by
      dsimp [l']
      rw [List.sum_map_mul_left, List.map_id']
    have hl'p : l'.prod = i ^ i * l.prod := by
      dsimp [l']
      rw [List.prod_map_mul, List.map_id', List.map_const', List.prod_replicate, h]
    let l'' := l' ++ List.replicate (2^k - i) l.sum
    specialize ih l'' (by grind)
    simp [l'', hl's, hl'p, ← add_mul, mul_pow, add_tsub_cancel_of_le hi.le] at ih
    rw [← mul_le_mul_iff_of_pos_left (a := (2 ^ k) ^ 2 ^ k * l.sum ^ (2 ^ k - i))
      (by positivity),
      mul_assoc _ _ (l.sum ^ _), ← pow_add, tsub_add_cancel_of_le hi.le]
    convert ih using 1
    grind

[Eric Wieser]

One potentially nice thing about this approach is that it doesn't use any subtraction on the elements, only the counts

[Junyan Xu]

Yury G. Kudryashov said:

Junyan Xu said:

1, 2, ..., n are cancellable from inequalities (that is, ka \geq kb entails a \geq b for k \in [n])

docs#MulLeftReflectLE

This is a wrong typeclass. It doesn't assume k > 0.

Sorry, this should work instead

import Mathlib.Order.Fin.Basic
import Mathlib.Algebra.Order.Module.Defs
variable (n : ℕ) (α : Type*) [AddMonoid α] [Preorder α]
instance [SMul ℕ α] : SMul (Fin n) α where
  smul := (·.val • ·)
#check PosSMulReflectLE (Fin (n + 1)) α

[Snir Broshi]

Eric Wieser said:

For what it's worth, I had a go at the binary recursion approach:

Cool induction!
You don't need to show it for all powers less than 2^k, just for k itself, since k ≤ 2^k:

simplified induction principle

import Mathlib

/-- An induction principle considering powers of two; to produce `P`,
we need only a mechanism to produce it for powers of `2`,
and for values less than the closest power. -/
def Nat.powTwoRec {P : ℕ → Sort*}
    (pow_two : ∀ k, P (2 ^ k))
    (le_pow_two : ∀ k, P (2 ^ k) → P k) : ∀ n, P n :=
  fun _ ↦ le_pow_two _ <| pow_two _

-- https://en.wikipedia.org/wiki/AM%E2%80%93GM_inequality#Proof_by_Cauchy_using_forward%E2%80%93backward_induction
theorem cauchy (l : List ℕ) :
    l.length ^ l.length * l.prod ≤ l.sum ^ l.length := by
  induction h : l.length using Nat.powTwoRec generalizing l with
  | pow_two k =>
    induction k using Nat.caseStrongRecOn generalizing l with
    | zero =>
      rw [pow_zero, List.length_eq_one_iff] at h
      obtain ⟨a, rfl⟩ := h
      simp
    | ind k' ik =>
      cases k' with
      | zero =>
        simp [List.length_eq_two] at h
        obtain ⟨a, b, rfl⟩ := h
        suffices 4 * a * b ≤ a^2 + 2 * a * b + b^2 by
          simpa [add_sq, mul_assoc] using this
        suffices 2 * a * b ≤ a^2 + b^2 by
          cutsat
        exact two_mul_le_add_pow_two _ _
      | succ k' =>
        rw [pow_succ] at h
        let +generalize k'' := k' + 1
        let l_left := l.take (2 ^ k'')
        let l_right := l.drop (2 ^ k'')
        have ik_left := ik k'' le_rfl l_left <| by grind
        have ik_right := ik k'' le_rfl l_right <| by grind
        have ik_lr := mul_le_mul_left' (mul_le_mul' ik_left ik_right)  (2 ^ (2 * 2 ^ k'')); clear ik_left ik_right
        rw [mul_mul_mul_comm, ← pow_add, ← two_mul, ← pow_succ', ← pow_mul,
          ← mul_pow] at ik_lr
        have : l = l_left ++ l_right := List.take_append_drop _ _ |>.symm
        rw [this, List.prod_append, List.sum_append, pow_succ']
        have ik2 := ik 1 (by cutsat) [l_left.sum, l_right.sum] rfl
        simp at ik2
        replace ik2 := Nat.pow_le_pow_left ik2 (2 ^ k'')
        rw [← pow_mul, mul_pow 4] at ik2
        refine le_trans ?_ ik2
        clear ik2
        convert ik_lr using 1
        · rw [← mul_assoc _ _ (_ * _)]
          congr 1
          simp [← pow_add, mul_pow, ← pow_mul, pow_succ']
        · simp [pow_succ', pow_mul]
  | le_pow_two k ih =>
    by_cases hls : l.sum = 0
    · rw [hls]
      cases l; · simp_all
      rw [List.sum_eq_zero_iff] at hls
      simp [hls _ List.mem_cons_self, List.prod_cons]
    let l' := l.map (k * ·)
    have hl's : l'.sum = k * l.sum := by
      dsimp [l']
      rw [List.sum_map_mul_left, List.map_id']
    have hl'p : l'.prod = k ^ k * l.prod := by
      dsimp [l']
      rw [List.prod_map_mul, List.map_id', List.map_const', List.prod_replicate, h]
    let l'' := l' ++ List.replicate (2^k - k) l.sum
    have hle : k ≤ 2 ^ k := le_trans (Nat.le_succ _) <| pow_right_strictMono₀ Nat.one_lt_two |>.add_le_nat k 0
    specialize ih l'' (by grind)
    simp [l'', hl's, hl'p, ← add_mul, mul_pow, add_tsub_cancel_of_le hle] at ih
    rw [← mul_le_mul_iff_of_pos_left (a := (2 ^ k) ^ 2 ^ k * l.sum ^ (2 ^ k - k))
      (by positivity),
      mul_assoc _ _ (l.sum ^ _), ← pow_add, tsub_add_cancel_of_le hle]
    convert ih using 1
    grind

[Snir Broshi]

These also seem like nice induction variants:

def Nat.backwardRec {P : ℕ → Sort*} (hback : ∀ n, P (n + 1) → P n) :
    ∀ n m, m ≤ n → P n → P m :=
  fun _ _ hmn hn ↦ Nat.decreasingInduction (fun _ _ hkp1 ↦ hback _ hkp1) hn hmn

def Nat.forwardBackwardRec {P : ℕ → Sort*} {f : ℕ → ℕ} (hf : ∀ n, n ≤ f n)
    (hpf : ∀ n, P (f n)) (hback : ∀ n, P (n + 1) → P n) : ∀ n, P n :=
  fun _ ↦ Nat.backwardRec hback _ _ (hf _) (hpf _)

[Eric Wieser]

Snir Broshi said:

You don't need to show it for all powers less than 2^k, just for k itself, since k ≤ 2^k:

To me this feels like it makes the induction uglier, especially when you consider it as a recursion principle instead. I think the nicer verion has extra hypotheses that i is between two adjacent known powers. Either way, I'm not sure I'd expect this principle to be used elsewhere, so it's probably best to make it private.

[Violeta Hernández]

Ah yes, "Cauchy induction", the induction principle used for this proof and nowhere else

[Francisco Unda]

I was directed to this thread after I posted https://github.com/leanprover-community/mathlib4/pull/31492 in "new members", and I wanted to share :)