`Compfiles/Usa2020P6.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

17 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2020 Problem 6

Let n ≥ 2 be an integer. Let x₁ ≥ x₂ ≥ ⋯ ≥ xₙ and y₁ ≥ y₂ ≥ ⋯ ≥ yₙ be 2n real numbers such that

0 = x₁ + x₂ + ⋯ + xₙ = y₁ + y₂ + ⋯ + yₙ,

and

1 = x₁² + x₂² + ⋯ + xₙ² = y₁² + y₂² + ⋯ + yₙ².

Prove that

∑_{i=1}^{n} (xᵢyᵢ − xᵢyₙ₊₁₋ᵢ) ≥ 2/√(n−1).

Imports (5)

Imported by 1 file

Compfiles.lean

lemma Usa2020P6.card_fiber_eq Documented declaration: card_fiber_eq line 56 source
Source documentation
The fibers of the evaluation map σ ↦ σ i on Perm (Fin n) all have the same cardinality: left multiplication by Equiv.swap a b is a bijection between the fiber over a and the fiber over b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.card, Equiv.Perm, Finset.filter, Finset.univ
Proof uses: Finset.card_bij, Membership.mem, Finset, HMul.hMul, Equiv.swap, Eq.mpr, And, id, congrArg, propext, Finset.mem_filter, And.intro, Finset.mem_univ, Equiv.Perm.mul_apply, And.right, Eq.mp, Equiv.swap_apply_left, Eq.refl, mul_left_cancel, Exists.intro and 3 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma card_fiber_eq {n : ℕ} (i a b : Fin n) :
    #(univ.filter fun σ : Equiv.Perm (Fin n) => σ i = a) =
    #(univ.filter fun σ : Equiv.Perm (Fin n) => σ i = b) := by
…
```
lemma Usa2020P6.card_fiber Each fiber of the evaluation map σ ↦ σ i has cardinality (n-1)! line 74 source
Source documentation
Each fiber of the evaluation map σ ↦ σ i has cardinality (n-1)!.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Eq, Finset.card, Equiv.Perm, Finset.filter, Finset.univ, Nat.factorial, HSub.hSub
Proof uses: Usa2020P6.card_fiber_eq, Eq.mpr, Fintype.card, id, congrArg, Finset.card_univ, Fintype.card_perm, Fintype.card_fin, Eq.refl, Finset.sum, Eq.symm, Finset.card_eq_sum_card_fiberwise, Membership.mem, Set, Finset, Finset.mem_univ, HMul.hMul, HAdd.hAdd, Eq.rec, Eq.trans and 9 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma card_fiber {n : ℕ} (hn : 1 ≤ n) (i a : Fin n) :
    #(univ.filter fun σ : Equiv.Perm (Fin n) => σ i = a) = (n - 1)! := by
…
```
lemma Usa2020P6.sum_perm_apply Summing f (σ i) over all permutations gives (n-1)! times the sum of f line 95 source
Source documentation
Summing f (σ i) over all permutations gives (n-1)! times the sum of f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Eq, Finset.sum, Equiv.Perm, Finset.univ, HMul.hMul, Nat.factorial, HSub.hSub
Proof uses: Trans.trans, Finset.filter, Eq.symm, Finset.sum_fiberwise_of_maps_to', Membership.mem, Finset, Finset.mem_univ, Finset.sum_congr, rfl, Eq.mpr, HSMul.hSMul, Finset.card, id, congrArg, Finset.sum_const, nsmul_eq_mul, Usa2020P6.card_fiber, Eq.refl, Finset.mul_sum
52 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma sum_perm_apply {n : ℕ} (hn : 1 ≤ n) (i : Fin n) (f : Fin n → ℝ) :
    ∑ σ : Equiv.Perm (Fin n), f (σ i) = ((n - 1)! : ℝ) * ∑ a, f a := by
…
```
Mentions: f
lemma Usa2020P6.card_fiber₂_eq The fibers of σ ↦ (σ i, σ j) over pairs (a₁, b) and (a₂, b) have the same cardinality, via left multiplication by Equiv.swap a₁ a₂ line 110 source
Source documentation
The fibers of σ ↦ (σ i, σ j) over pairs (a₁, b) and (a₂, b) have the same cardinality, via left multiplication by Equiv.swap a₁ a₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Ne, Eq, Finset.card, Equiv.Perm, Finset.filter, And, Finset.univ
Proof uses: Finset.card_bij, Membership.mem, Finset, HMul.hMul, Equiv.swap, Eq.mpr, id, congrArg, propext, Finset.mem_filter, And.intro, Finset.mem_univ, Equiv.Perm.mul_apply, And.left, And.right, Eq.mp, Equiv.swap_apply_left, Eq.refl, Equiv.swap_apply_of_ne_of_ne, Ne.symm and 5 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma card_fiber₂_eq {n : ℕ} (i j : Fin n) (b a₁ a₂ : Fin n) (h₁ : a₁ ≠ b) (h₂ : a₂ ≠ b) :
    #(univ.filter fun σ : Equiv.Perm (Fin n) => σ i = a₁ ∧ σ j = b) =
    #(univ.filter fun σ : Equiv.Perm (Fin n) => σ i = a₂ ∧ σ j = b) := by
…
```
lemma Usa2020P6.card_fiber₂ Each fiber of σ ↦ (σ i, σ j) over a pair (a, b) with a ≠ b has cardinality (n-2)! line 135 source
Source documentation
Each fiber of σ ↦ (σ i, σ j) over a pair (a, b) with a ≠ b has cardinality (n-2)!.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Ne, Eq, Finset.card, Equiv.Perm, Finset.filter, And, Finset.univ, Nat.factorial, HSub.hSub
Proof uses: Finset, Eq.mpr, id, congrArg, Finset.filter_filter, Finset.filter_congr, Membership.mem, and_comm, Finset.sum, Finset.card_eq_sum_card_fiberwise, Set, Finset.mem_univ, Finset.sum_congr, rfl, Eq.refl, EmptyCollection.emptyCollection, propext, Finset.card_eq_zero, Finset.filter_false_of_mem, Equiv.injective and 24 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma card_fiber₂ {n : ℕ} (hn : 2 ≤ n) (i j : Fin n) (hij : i ≠ j) (a b : Fin n)
    (hab : a ≠ b) :
    #(univ.filter fun σ : Equiv.Perm (Fin n) => σ i = a ∧ σ j = b) = (n - 2)! := by
…
```
lemma Usa2020P6.sum_perm_apply₂ Summing g (σ i) (σ j) over all permutations, for i ≠ j line 178 source
Source documentation
Summing g (σ i) (σ j) over all permutations, for i ≠ j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Ne, Real, Eq, Finset.sum, Equiv.Perm, Finset.univ, HMul.hMul, Nat.factorial, HSub.hSub, Finset.erase
Proof uses: Finset, Finset.filter, Prod, Prod.mk, And, Finset.filter_congr, Membership.mem, Prod.ext_iff, Finset.card, Eq.mpr, id, congrArg, EmptyCollection.emptyCollection, propext, Finset.card_eq_zero, Finset.filter_false_of_mem, Equiv.injective, Eq.trans, Equiv, And.left and 26 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma sum_perm_apply₂ {n : ℕ} (hn : 2 ≤ n) (i j : Fin n) (hij : i ≠ j) (g : Fin n → Fin n → ℝ) :
    ∑ σ : Equiv.Perm (Fin n), g (σ i) (σ j) =
      ((n - 2)! : ℝ) * ∑ a : Fin n, ∑ b ∈ univ.erase a, g a b := by
…
```
lemma Usa2020P6.sum_S_eq_zero ∑ σ, S σ = 0 where S σ = ∑ i, x i * y (σ i) line 220 source
Source documentation
∑ σ, S σ = 0 where S σ = ∑ i, x i * y (σ i).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Eq, Finset.sum, Finset.univ, Equiv.Perm, HMul.hMul
Proof uses: Eq.mpr, id, congrArg, Finset.sum_comm, Finset.sum_eq_zero, Membership.mem, Finset, Eq.symm, Finset.mul_sum, Nat.factorial, HSub.hSub, Usa2020P6.sum_perm_apply, MulZeroClass.mul_zero, Eq.refl
48 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma sum_S_eq_zero {n : ℕ} (hn : 1 ≤ n) (x y : Fin n → ℝ) (hys : ∑ i, y i = 0) :
    ∑ σ : Equiv.Perm (Fin n), ∑ i, x i * y (σ i) = 0 := by
…
```
lemma Usa2020P6.sum_S_sq The second moment `∑ σ, (S σ)² = (n-1)! line 229 source
Source documentation
The second moment ∑ σ, (S σ)² = (n-1)! + (n-2)!.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Eq, Finset.sum, Finset.univ, HPow.hPow, Equiv.Perm, HMul.hMul, HAdd.hAdd, Nat.factorial, HSub.hSub
Proof uses: Finset.erase, Neg.neg, Finset.sum_erase_add, Finset.mem_univ, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.sub_congr and 73 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma sum_S_sq {n : ℕ} (hn : 2 ≤ n) (x y : Fin n → ℝ)
    (hxs : ∑ i, x i = 0) (hys : ∑ i, y i = 0)
    (hx2 : ∑ i, x i ^ 2 = 1) (hy2 : ∑ i, y i ^ 2 = 1) :
    ∑ σ : Equiv.Perm (Fin n), (∑ i, x i * y (σ i)) ^ 2 = ((n - 1)! : ℝ) + ((n - 2)! : ℝ) := by
…
```
lemma Usa2020P6.variance_bound The variance bound: if S σ lies in [m, M] for all σ, then 2/√(n-1) ≤ M - m line 300 source
Source documentation
The variance bound: if S σ lies in [m, M] for all σ, then 2/√(n-1) ≤ M - m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Eq, Finset.sum, Finset.univ, HPow.hPow, Equiv.Perm, HMul.hMul, HDiv.hDiv, Real.sqrt, HSub.hSub
Proof uses: Usa2020P6.sum_S_eq_zero, HAdd.hAdd, Nat.factorial, Usa2020P6.sum_S_sq, mul_nonneg, Iff.mpr, sub_nonneg, Neg.neg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 114 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
lemma variance_bound {n : ℕ} (hn : 2 ≤ n) (x y : Fin n → ℝ)
    (hxs : ∑ i, x i = 0) (hys : ∑ i, y i = 0)
    (hx2 : ∑ i, x i ^ 2 = 1) (hy2 : ∑ i, y i ^ 2 = 1)
    (m M : ℝ) (hm : ∀ σ : Equiv.Perm (Fin n), m ≤ ∑ i, x i * y (σ i))
    (hM : ∀ σ : Equiv.Perm (Fin n), ∑ i, x i * y (σ i) ≤ M) :
    2 / Real.sqrt ((n : ℝ) - 1) ≤ M - m := by
…
```
lemma Usa2020P6.fin_strictMono_ge A strictly monotone function Fin m → ℕ dominates the identity line 381 source
Source documentation
A strictly monotone function Fin m → ℕ dominates the identity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, StrictMono, LE.le
Proof uses: LT.lt, Fin.mk, Nat.recAux, OfNat.ofNat, Nat.zero_le, HAdd.hAdd, Nat.lt_of_succ_lt, Eq.mpr, id, Eq, congrArg, propext, Fin.mk_lt_mk, Nat.lt_succ_self, Fin.isLt
17 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma fin_strictMono_ge {m : ℕ} {g : Fin m → ℕ} (hg : StrictMono g) (j : Fin m) :
    j.val ≤ g j := by
…
```
lemma Usa2020P6.topsum The sum of an antitone function over any finset is at most the sum over an initial segment of the same cardinality line 397 source
Source documentation
The sum of an antitone function over any finset is at most the sum over an initial segment of the same cardinality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Antitone, Finset, Eq, Finset.card, LE.le, Finset.sum, Finset.univ, Fin.mk, lt_of_lt_of_le, Fin.isLt
Proof uses: Membership.mem, OrderIso, Subtype, Finset.orderIsoOfFin, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_coe_sort, Equiv, RelIso.toEquiv, Equiv.sum_comp, Finset.sum_le_sum, propext, Fin.le_def, OrderEmbedding, Finset.orderEmbOfFin, Finset.coe_orderIsoOfFin_apply, Usa2020P6.fin_strictMono_ge, Function.comp and 3 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma topsum {n : ℕ} (y : Fin n → ℝ) (hy : Antitone y) (s : Finset (Fin n)) {m : ℕ}
    (hm : s.card = m) (hmn : m ≤ n) :
    ∑ i ∈ s, y i ≤ ∑ j : Fin m, y ⟨j.val, lt_of_lt_of_le j.isLt hmn⟩ := by
…
```
lemma Usa2020P6.topsum' The sum of a monotone function over any finset is at most the sum over a terminal segment of the same cardinality line 412 source
Source documentation
The sum of a monotone function over any finset is at most the sum over a terminal segment of the same cardinality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Monotone, Finset, Eq, Finset.card, LE.le, Finset.sum, Finset.univ, Fin.rev, Fin.mk, lt_of_lt_of_le, Fin.isLt
Proof uses: Antitone, Function.comp, Monotone.comp_antitone, Iff.mpr, Fin.rev_le_rev, Finset.image, Eq.mpr, id, congrArg, Finset.card_image_of_injective, Fin.rev_injective, Usa2020P6.topsum, Eq.mp, congr, Finset.sum_congr, Eq.refl, Membership.mem, Fin.rev_rev, Finset.sum_image, Function.Injective.injOn
24 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma topsum' {n : ℕ} (g : Fin n → ℝ) (hg : Monotone g) (s : Finset (Fin n)) {m : ℕ}
    (hm : s.card = m) (hmn : m ≤ n) :
    ∑ i ∈ s, g i ≤ ∑ j : Fin m, g (Fin.rev ⟨j.val, lt_of_lt_of_le j.isLt hmn⟩) := by
…
```
lemma Usa2020P6.bottomsum The sum of an antitone function over any finset is at least the sum over a terminal segment of the same cardinality line 427 source
Source documentation
The sum of an antitone function over any finset is at least the sum over a terminal segment of the same cardinality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Antitone, Finset, Eq, Finset.card, LE.le, Finset.sum, Finset.univ, Fin.rev, Fin.mk, lt_of_lt_of_le, Fin.isLt
Proof uses: Neg.neg, Usa2020P6.topsum', neg_le_neg, le_of_neg_le_neg, Eq.mp, congrArg, Finset.sum_neg_distrib
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma bottomsum {n : ℕ} (y : Fin n → ℝ) (hy : Antitone y) (s : Finset (Fin n)) {m : ℕ}
    (hm : s.card = m) (hmn : m ≤ n) :
    ∑ j : Fin m, y (Fin.rev ⟨j.val, lt_of_lt_of_le j.isLt hmn⟩) ≤ ∑ i ∈ s, y i := by
…
```
lemma Usa2020P6.abel_nonneg Summation by parts: if z has zero sum and nonnegative partial sums, and x is decreasing on range n, then ∑ x i * z i ≥ 0 line 436 source
Source documentation
Summation by parts: if z has zero sum and nonnegative partial sums, and x is decreasing on range n, then ∑ x i * z i ≥ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Finset.sum, Finset.range, OfNat.ofNat, LT.lt, HAdd.hAdd, LE.le, HSub.hSub, HMul.hMul
Proof uses: Finset.Ico, Eq.mpr, id, congrArg, Finset.sum_Ico_eq_sub, Finset.sum_range_sub, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.Common.neg_add and 55 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
lemma abel_nonneg {n : ℕ} (x z : ℕ → ℝ)
    (hz : ∑ i ∈ Finset.range n, z i = 0)
    (hx : ∀ k : ℕ, k + 1 < n → 0 ≤ x k - x (k + 1))
    (hZ : ∀ k : ℕ, k < n → 0 ≤ ∑ i ∈ Finset.range (k + 1), z i) :
    0 ≤ ∑ i ∈ Finset.range n, x i * z i := by
…
```
lemma Usa2020P6.rearr_upper Rearrangement inequality (upper bound): for two decreasing sequences, the "identity" pairing maximizes ∑ x i * y (σ i) over all permutations σ line 508 source
Source documentation
Rearrangement inequality (upper bound): for two decreasing sequences, the "identity" pairing maximizes ∑ x i * y (σ i) over all permutations σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Antitone, Equiv.Perm, LE.le, Finset.sum, Finset.univ, HMul.hMul
Proof uses: Eq, Finset.range, dite, LT.lt, HSub.hSub, Fin.mk, Not, OfNat.ofNat, Eq.symm, Finset.sum_fin_eq_sum_range, Eq.mpr, id, congrArg, Finset.sum_sub_distrib, Equiv, Equiv.sum_comp, sub_self, Eq.refl, HAdd.hAdd, dite_eq_left and 37 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma rearr_upper {n : ℕ} (x y : Fin n → ℝ) (hx : Antitone x) (hy : Antitone y)
    (σ : Equiv.Perm (Fin n)) :
    ∑ i, x i * y (σ i) ≤ ∑ i, x i * y i := by
…
```
lemma Usa2020P6.rearr_lower Rearrangement inequality (lower bound): for two decreasing sequences, the "reversed" pairing minimizes ∑ x i * y (σ i) over all permutations σ line 560 source
Source documentation
Rearrangement inequality (lower bound): for two decreasing sequences, the "reversed" pairing minimizes ∑ x i * y (σ i) over all permutations σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Antitone, Equiv.Perm, LE.le, Finset.sum, Finset.univ, HMul.hMul, Fin.rev
Proof uses: Eq, Finset.range, dite, LT.lt, HSub.hSub, Fin.mk, Not, OfNat.ofNat, Eq.symm, Finset.sum_fin_eq_sum_range, Eq.mpr, id, congrArg, Finset.sum_sub_distrib, Equiv, Equiv.sum_comp, Fin.revPerm, sub_self, Eq.refl, HAdd.hAdd and 38 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma rearr_lower {n : ℕ} (x y : Fin n → ℝ) (hx : Antitone x) (hy : Antitone y)
    (σ : Equiv.Perm (Fin n)) :
    ∑ i, x i * y (Fin.rev i) ≤ ∑ i, x i * y (σ i) := by
…
```
problem Usa2020P6.usa2020_p6 USA Mathematical Olympiad 2020, Problem 6 line 615 source
Source documentation
USA Mathematical Olympiad 2020, Problem 6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Antitone, Eq, Finset.sum, Finset.univ, HPow.hPow, GE.ge, HSub.hSub, HMul.hMul, Fin.rev, HDiv.hDiv, Real.sqrt
Proof uses: Equiv.Perm, And, Membership.mem, Finset, Exists, Finset.exists_max_image, Finset.univ_nonempty, Finset.exists_min_image, Usa2020P6.variance_bound, Finset.mem_univ, Usa2020P6.rearr_upper, Usa2020P6.rearr_lower, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, congrArg and 66 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
problem usa2020_p6 {n : ℕ} (hn : 2 ≤ n) (x y : Fin n → ℝ)
    (hx : Antitone x) (hy : Antitone y)
    (hxs : ∑ i, x i = 0) (hys : ∑ i, y i = 0)
    (hx2 : ∑ i, x i ^ 2 = 1) (hy2 : ∑ i, y i ^ 2 = 1) :
    ∑ i, (x i * y i - x i * y (Fin.rev i)) ≥ 2 / Real.sqrt ((n : ℝ) - 1) := by
…
```