feat(Archive/Imo): formalize IMO 1982q3

[AlexBrodbelt]

Formalized problem 3 of 1982 IMO.

For part a, helper lemmas like Sedrakayan's lemma, a specialization of the Cauchy-Schwarz inequality, and useful other inequalities involving summations to solve the main problem.

For part b, rearranging terms inside summations and involving summations in inequalities were proved.

---

[github-actions]

PR summary c062503898

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Ico_sdiff_zero_eq_Ico
+ Imo1982Q3_part_a
+ Imo1982Q3_part_b
+ Sedrakyan's_lemma
+ eq₀
+ ineq₁
+ ineq₂
+ ineq₃
+ sum_Fin_eq_sum_Ico

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.

[jsm28]

General comments applicable both to this lemma and elsewhere in this PR:

• Normally rather than having a lemma statement start with ∀ after the colon and then the proof starting with intro, we use named hypotheses before the colon, so (N : ℕ) in this case, and so don't need to start the proof with intro. Much the same applies if the statement is of the form h → p: move the hypotheses h before the colon rather than having an implication on the right hand side of the colon.
• Standard indentation of the proof body is two columns, not four.

Specific remark about this lemma: it's essentially a combination of the existing lemmas sdiff_singleton_eq_erase, Ico_erase_left and Ico_succ_left. That should allow a much shorter proof. It might then be reasonable to inline that at the point where this lemma is needed.

[YaelDillies]

Suggested change

	have LHS_nonneg : 0 ≤ ∑ n : Fin n, √(y n) * (x n / √(y n)) := by
	apply Finset.sum_nonneg
	intro i _hi
	apply mul_nonneg (le_of_lt (sqrt_yi_pos i))
	apply div_nonneg (xi_nonneg _) (le_of_lt (sqrt_yi_pos _))
	have LHS_nonneg : 0 ≤ ∑ n : Fin n, √(y n) * (x n / √(y n)) := by positivity

[YaelDillies]

This is a general fact about sequences of reals. Can you generalise? The lemma you want to use is Finset.sum_mul_sq_le_sq_mul_sq instead of real_inner_le_norm

[vihdzp]

I'd also like to reiterate my petition for this lemma to be added within Mathlib proper. It will definitely be useful for other IMO problems!

[vihdzp]

#19311

[YaelDillies]

These @ are usually useless

Suggested change

	rw [@Nat.cast_eq_one] at h
	rw [Nat.cast_eq_one] at h

[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.

[dwrensha]

FYI I added this solution to Compfiles: dwrensha/compfiles@e7f00a5

[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.