feat(Archive/Imo): formalize IMO 1982q3

[AlexBrodbelt]

Formalize problem 3 of 1982 IMO.

Co-authored by: Violeta Hernández Palacios [email protected]

---

[github-actions]

PR summary 3e11988adf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ geom_sum_lt
+ imo1982_q3a
+ imo1982_q3b
+ ineq
+ le_avg

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[hrmacbeth]

@AlexBrodbelt, I have the impression that you have quite a few tricks yet to learn about writing analysis arguments in Lean. As an example, I have pushed an efficient proof of your first lemma.

The "Archive" is for high quality proofs that, while being mathematical "leaf theories", show off the automation and libraries developed in Mathlib. At the moment this proof is quite far from being this kind of showcase. If you want to work on getting this proof to that level, it will take a lot of back-and-forth, and this may proceed rather slowly, depending on reviewers' availability to point out inefficiencies.

If you just want to make this proof available in a public repository for the community to use, you might consider instead contributing it to https://github.com/dwrensha/compfiles. Are you aware of that project?

[vihdzp]

I'm interested in helping clean this proof up! I just haven't found the time for it yet. Maybe sometime during the week?

One thing which I'd like to see beforehand (and I think I already mentioned this above) is Sedrakyan's lemma in a separate PR. There will almost definitely be more IMO problems that depend on this.

[vihdzp]

@AlexBrodbelt I did a complete rewrite of the proof on my own branch. It ends up being only about 100 lines long, and I think that it better showcases Mathlib's automation. If you think what I did is sensible, you can merge the changes in that branch with this branch. Note that my proof depends on PR #19311.

If you're not available to come back to this PR, I can take it over.

[vihdzp]

Since there's been no activity from OP since September, I've decided to take over this PR. The new proof is an almost complete rewrite from the original one, and makes use of the version of Sedrakyan I had previously PR'd onto Mathlib.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[kbuzzard]

This docstring does not seem to correspond to the lemma it's documenting.

[vihdzp]

The actual lemma is just this plus ∑ k ∈ range n, x k added to both sides.

[kbuzzard]

That's not true either because of various errors involving bounds (range n is 0<=i<n, right?).

[vihdzp]

You're right, I've updated the docstring.