Loogle!

Result

Found 25 declarations whose name contains "sum_le_sum".

• List.Forall₂.sum_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M} (h : List.Forall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂) : l₁.sum ≤ l₂.sum
• List.sum_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) : (List.map f l).sum ≤ (List.map g l).sum
• List.Sublist.sum_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M} (h : l₁.Sublist l₂) (h₁ : ∀ a ∈ l₂, 0 ≤ a) : l₁.sum ≤ l₂.sum
• List.SublistForall₂.sum_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M} (h : List.SublistForall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂) (h₁ : ∀ a ∈ l₂, 0 ≤ a) : l₁.sum ≤ l₂.sum
• Cardinal.sum_le_sum 📋 Mathlib.SetTheory.Cardinal.Order
  {ι : Type u_1} (f g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i ≤ g i) : Cardinal.sum f ≤ Cardinal.sum g
• Multiset.sum_le_sum_of_rel_le 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} [AddCommMonoid α] [PartialOrder α] {s t : Multiset α} [AddLeftMono α] (h : Multiset.Rel (fun x1 x2 => x1 ≤ x2) s t) : s.sum ≤ t.sum
• Multiset.sum_le_sum_map 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} [AddCommMonoid α] [PartialOrder α] {s : Multiset α} [AddLeftMono α] (f : α → α) (h : ∀ x ∈ s, x ≤ f x) : s.sum ≤ (Multiset.map f s).sum
• Multiset.abs_sum_le_sum_abs 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} : |s.sum| ≤ (Multiset.map abs s).sum
• Finset.sum_le_sum_of_subset 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s t : Finset ι} (h : s ⊆ t) : ∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
• Finset.sum_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f g : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ i ∈ s, f i ≤ g i) : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
• Finset.abs_sum_le_sum_abs 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {G : Type u_9} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (f : ι → G) (s : Finset ι) : |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i|
• Finset.sum_le_sum_of_ne_zero 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s t : Finset ι} (h : ∀ x ∈ s, f x ≠ 0 → x ∈ t) : ∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
• Finset.sum_le_sum_of_subset_of_nonneg 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s t : Finset ι} [AddLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 0 ≤ f i) : ∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
• Finset.sum_le_sum_of_subset_of_nonpos 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s t : Finset ι} [AddLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → f i ≤ 0) : ∑ i ∈ t, f i ≤ ∑ i ∈ s, f i
• Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [AddLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, ∑ x ∈ s with g x = y, f x ≤ 0) : ∑ x ∈ s, f x ≤ ∑ y ∈ t, ∑ x ∈ s with g x = y, f x
• Finsupp.sum_le_sum 📋 Mathlib.Data.Finsupp.Order
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ h₂ : ι → α → β} (h : ∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) : f.sum h₁ ≤ f.sum h₂
• Finsupp.sum_le_sum_index 📋 Mathlib.Data.Finsupp.Order
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β} (hf : f₁ ≤ f₂) (hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)) (hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) : f₁.sum h ≤ f₂.sum h
• Antivary.card_mul_sum_le_sum_mul_sum 📋 Mathlib.Algebra.Order.Chebyshev
  {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ↑(Fintype.card ι) * ∑ i, f i * g i ≤ (∑ i, f i) * ∑ i, g i
• AntivaryOn.card_mul_sum_le_sum_mul_sum 📋 Mathlib.Algebra.Order.Chebyshev
  {ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {s : Finset ι} {f g : ι → α} (hfg : AntivaryOn f g ↑s) : ↑s.card * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
• Antivary.card_smul_sum_le_sum_smul_sum 📋 Mathlib.Algebra.Order.Chebyshev
  {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {f : ι → α} {g : ι → β} [Fintype ι] (hfg : Antivary f g) : Fintype.card ι • ∑ i, f i • g i ≤ (∑ i, f i) • ∑ i, g i
• AntivaryOn.card_smul_sum_le_sum_smul_sum 📋 Mathlib.Algebra.Order.Chebyshev
  {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {s : Finset ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g ↑s) : s.card • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, g i
• Finset.sum_le_sum_range 📋 Mathlib.Algebra.Order.Group.Int.Sum
  {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) : ∑ x ∈ s, x ≤ ∑ n ∈ Finset.range s.card, (c - ↑n)
• Finset.sum_le_sum_Ioc 📋 Mathlib.Algebra.Order.Group.Int.Sum
  {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) : ∑ x ∈ s, x ≤ ∑ x ∈ Finset.Ioc (c - ↑s.card) c, x
• NumberField.house_sum_le_sum_house 📋 Mathlib.NumberTheory.NumberField.House
  {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (α : ι → K) : NumberField.house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, NumberField.house (α i)
• BoundingSieve.siftedSum_le_sum_of_upperMoebius 📋 Mathlib.NumberTheory.SelbergSieve
  {s : BoundingSieve} (muPlus : ℕ → ℝ) (h : BoundingSieve.IsUpperMoebius muPlus) : BoundingSieve.siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * BoundingSieve.multSum d

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 76f94b4