no goals
ι : 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
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 _
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
ι : 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
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
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
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
rw [← card_range s.card, sum_smul_sum_eq_sum_perm hσ]
no goals
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
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 _