[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) • ∑ i in s, g i ≤ card s • ∑ i in s, f i • g i
[PROOFSTEP]
classical
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
rw [← card_range s.card, sum_smul_sum_eq_sum_perm hσ]
exact
  sum_le_card_nsmul _ _ _ fun n _ =>
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx => hs fun h => hx <| IsFixedPt.perm_pow h _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) • ∑ i in s, g i ≤ card s • ∑ i in s, f i • g i
[PROOFSTEP]
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ✝ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : IsCycleOn σ ↑s
hs : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ (∑ i in s, f i) • ∑ i in s, g i ≤ card s • ∑ i in s, f i • g i
[PROOFSTEP]
rw [← card_range s.card, sum_smul_sum_eq_sum_perm hσ]
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ✝ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : IsCycleOn σ ↑s
hs : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ k in range (card s), ∑ i in s, f i • g (↑(σ ^ k) i) ≤ card (range (card s)) • ∑ i in s, f i • g i
[PROOFSTEP]
exact
  sum_le_card_nsmul _ _ _ fun n _ =>
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx => hs fun h => hx <| IsFixedPt.perm_pow h _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
⊢ card s • ∑ i in s, f i • g i ≤ (∑ i in s, f i) • ∑ i in s, g i
[PROOFSTEP]
refine hfg.dual_right.sum_smul_sum_le_card_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ Fintype.card ι • ∑ i : ι, f i • g i ≤ (∑ i : ι, f i) • ∑ i : ι, g i
[PROOFSTEP]
refine (hfg.dual_right.monovaryOn _).sum_smul_sum_le_card_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ ↑(card s) * ∑ i in s, f i * g i
[PROOFSTEP]
rw [← nsmul_eq_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ card s • ∑ i in s, f i * g i
[PROOFSTEP]
exact hfg.sum_smul_sum_le_card_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ ↑(card s) * ∑ i in s, f i * g i ≤ (∑ i in s, f i) * ∑ i in s, g i
[PROOFSTEP]
rw [← nsmul_eq_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ card s • ∑ i in s, f i * g i ≤ (∑ i in s, f i) * ∑ i in s, g i
[PROOFSTEP]
exact hfg.card_smul_sum_le_sum_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
⊢ (∑ i in s, f i) ^ 2 ≤ ↑(card s) * ∑ i in s, f i ^ 2
[PROOFSTEP]
simp_rw [sq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
⊢ (∑ i in s, f i) * ∑ i in s, f i ≤ ↑(card s) * ∑ x in s, f x * f x
[PROOFSTEP]
exact (monovaryOn_self _ _).sum_mul_sum_le_card_mul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
f : ι → α
⊢ ((∑ i in ∅, f i) / ↑(card ∅)) ^ 2 ≤ (∑ i in ∅, f i ^ 2) / ↑(card ∅)
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
[PROOFSTEP]
rw [← card_pos, ← @Nat.cast_pos α] at hs 
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
[PROOFSTEP]
rw [div_pow, div_le_div_iff (sq_pos_of_ne_zero _ hs.ne') hs, sq (s.card : α), mul_left_comm, ← mul_assoc]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ (∑ i in s, f i) ^ 2 * ↑(card s) ≤ (↑(card s) * ∑ i in s, f i ^ 2) * ↑(card s)
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right sq_sum_le_card_mul_sum_sq hs.le
