Loogle!

Result

Found 2867 declarations mentioning Finset.sum. Of these, 29 have a name containing "fiber".

• Finset.card_eq_sum_card_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_4} [DecidableEq M] {f : ι → M} {s : Finset ι} {t : Finset M} (H : Set.MapsTo f ↑s ↑t) : s.card = ∑ b ∈ t, {a ∈ s | f a = b}.card
• Finset.sum_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → M) : ∑ j, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i
• Finset.sum_fiberwise' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → M) : ∑ j, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s, f (g i)
• Finset.sum_card_fiberwise_eq_card_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_5} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) : ∑ j ∈ t, {i ∈ s | g i = j}.card = {i ∈ s | g i ∈ t}.card
• Finset.sum_fiberwise_of_maps_to 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → M) : ∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i
• Finset.sum_fiberwise_eq_sum_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → M) : ∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s with g i ∈ t, f i
• Finset.sum_fiberwise_of_maps_to' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → M) : ∑ j ∈ t, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s, f (g i)
• Finset.sum_fiberwise_eq_sum_filter' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → M) : ∑ j ∈ t, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s with g i ∈ t, f (g i)
• Fintype.sum_fiberwise' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] [DecidableEq κ] (g : ι → κ) (f : κ → M) : ∑ j, ∑ _i, f j = ∑ i, f (g i)
• Fintype.sum_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] [DecidableEq κ] (g : ι → κ) (f : ι → M) : ∑ j, ∑ i, f ↑i = ∑ i, f i
• Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, 0 ≤ ∑ x ∈ s with g x = y, f x) : ∑ y ∈ t, ∑ x ∈ s with g x = y, f x ≤ ∑ x ∈ s, f x
• 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] [IsOrderedAddMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {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
• Finset.support_of_fiberwise_sum_subset_image 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] (s : Finset α) (f : α → M) (g : α → β) : (Function.support fun b => ∑ a ∈ s with g a = b, f a) ⊆ ↑(Finset.image g s)
• Finset.dens_eq_sum_dens_fiberwise 📋 Mathlib.Algebra.BigOperators.Field
  {α : Type u_3} {β : Type u_4} [Fintype β] {s : Finset α} [DecidableEq α] {f : β → α} {t : Finset β} (h : Set.MapsTo f ↑t ↑s) : t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens
• ProbabilityTheory.sum_meas_smul_cond_fiber 📋 Mathlib.Probability.ConditionalProbability
  {Ω : Type u_1} {α : Type u_3} {m : MeasurableSpace Ω} [Fintype α] [MeasurableSpace α] [DiscreteMeasurableSpace α] {X : Ω → α} (hX : Measurable X) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ∑ x, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}] = μ
• BoxIntegral.Prepartition.sum_fiberwise 📋 Mathlib.Analysis.BoxIntegral.Partition.Basic
  {ι : Type u_1} {I : BoxIntegral.Box ι} {α : Type u_2} {M : Type u_3} [AddCommMonoid M] (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → α) (g : BoxIntegral.Box ι → M) : ∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J = ∑ J ∈ π.boxes, g J
• BoxIntegral.integralSum_fiberwise 📋 Mathlib.Analysis.BoxIntegral.Basic
  {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {I : BoxIntegral.Box ι} {α : Type u_1} (g : BoxIntegral.Box ι → α) (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I) : ∑ y ∈ Finset.image g π.boxes, BoxIntegral.integralSum f vol (π.filter fun x => g x = y) = BoxIntegral.integralSum f vol π
• Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hb : Fintype.card β • b < ∑ x, w x) : ∃ y, b < ∑ x with f x = y, w x
• Fintype.exists_sum_fiber_lt_of_sum_lt_nsmul 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hb : ∑ x, w x < Fintype.card β • b) : ∃ y, ∑ x with f x = y, w x < b
• Fintype.exists_le_sum_fiber_of_nsmul_le_sum 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [Nonempty β] (hb : Fintype.card β • b ≤ ∑ x, w x) : ∃ y, b ≤ ∑ x with f x = y, w x
• Fintype.exists_sum_fiber_le_of_sum_le_nsmul 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] [Nonempty β] (hb : ∑ x, w x ≤ Fintype.card β • b) : ∃ y, ∑ x with f x = y, w x ≤ b
• Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (hb : t.card • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x
• Finset.exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (hb : ∑ x ∈ s, w x < t.card • b) : ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b
• Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hb : t.card • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x
• Finset.exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hb : ∑ x ∈ s, w x ≤ t.card • b) : ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b
• Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (ht : ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0) (hb : t.card • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x
• Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (ht : ∀ y ∉ t, 0 ≤ ∑ x ∈ s with f x = y, w x) (hb : ∑ x ∈ s, w x < t.card • b) : ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b
• Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hf : ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0) (ht : t.Nonempty) (hb : t.card • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x
• Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul 📋 Mathlib.Combinatorics.Pigeonhole
  {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] (hf : ∀ y ∉ t, 0 ≤ ∑ x ∈ s with f x = y, w x) (ht : t.Nonempty) (hb : ∑ x ∈ s, w x ≤ t.card • b) : ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b

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 19971e9 serving mathlib revision 4cb993b