Skip to content

Commit ddae32a

Browse files
jcommelinChrisHughes24
jcommelin
and
ChrisHughes24
committed
feat: port Data.Fintype.BigOperators (#1742)
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
1 parent d96e4c3 commit ddae32a

File tree

2 files changed

+307
-0
lines changed

2 files changed

+307
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -268,6 +268,7 @@ import Mathlib.Data.Finset.Sigma
268268
import Mathlib.Data.Finset.Sort
269269
import Mathlib.Data.Finset.Sum
270270
import Mathlib.Data.Fintype.Basic
271+
import Mathlib.Data.Fintype.BigOperators
271272
import Mathlib.Data.Fintype.Card
272273
import Mathlib.Data.Fintype.Lattice
273274
import Mathlib.Data.Fintype.List

‎Mathlib/Data/Fintype/BigOperators.lean‎

Lines changed: 306 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,306 @@
1+
/-
2+
Copyright (c) 2017 Mario Carneiro. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mario Carneiro
5+
6+
! This file was ported from Lean 3 source module data.fintype.big_operators
7+
! leanprover-community/mathlib commit 2445c98ae4b87eabebdde552593519b9b6dc350c
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Data.Fintype.Option
12+
import Mathlib.Data.Fintype.Powerset
13+
import Mathlib.Data.Fintype.Sigma
14+
import Mathlib.Data.Fintype.Sum
15+
import Mathlib.Data.Fintype.Vector
16+
import Mathlib.Algebra.BigOperators.Ring
17+
import Mathlib.Algebra.BigOperators.Option
18+
19+
/-!
20+
Results about "big operations" over a `Fintype`, and consequent
21+
results about cardinalities of certain types.
22+
23+
## Implementation note
24+
This content had previously been in `Data.Fintype.Basic`, but was moved here to avoid
25+
requiring `Algebra.BigOperators` (and hence many other imports) as a
26+
dependency of `Fintype`.
27+
28+
However many of the results here really belong in `Algebra.BigOperators.Basic`
29+
and should be moved at some point.
30+
-/
31+
32+
33+
universe u v
34+
35+
variable {α : Type _} {β : Type _} {γ : Type _}
36+
37+
-- open BigOperators -- Porting note: notation is currently global
38+
39+
namespace Fintype
40+
41+
@[to_additive]
42+
theorem prod_bool [CommMonoid α] (f : Bool → α) : (∏ b, f b) = f true * f false := by simp
43+
#align fintype.prod_bool Fintype.prod_bool
44+
#align fintype.sum_bool Fintype.sum_bool
45+
46+
theorem card_eq_sum_ones {α} [Fintype α] : Fintype.card α = ∑ _a : α, 1 :=
47+
Finset.card_eq_sum_ones _
48+
#align fintype.card_eq_sum_ones Fintype.card_eq_sum_ones
49+
50+
section
51+
52+
open Finset
53+
54+
variable {ι : Type _} [DecidableEq ι] [Fintype ι]
55+
56+
@[to_additive]
57+
theorem prod_extend_by_one [CommMonoid α] (s : Finset ι) (f : ι → α) :
58+
(∏ i, if i ∈ s then f i else 1) = ∏ i in s, f i := by
59+
rw [← prod_filter, filter_mem_eq_inter, univ_inter]
60+
#align fintype.prod_extend_by_one Fintype.prod_extend_by_one
61+
#align fintype.sum_extend_by_zero Fintype.sum_extend_by_zero
62+
63+
end
64+
65+
section
66+
67+
variable {M : Type _} [Fintype α] [CommMonoid M]
68+
69+
@[to_additive]
70+
theorem prod_eq_one (f : α → M) (h : ∀ a, f a = 1) : (∏ a, f a) = 1 :=
71+
Finset.prod_eq_one fun a _ha => h a
72+
#align fintype.prod_eq_one Fintype.prod_eq_one
73+
#align fintype.sum_eq_zero Fintype.sum_eq_zero
74+
75+
@[to_additive]
76+
theorem prod_congr (f g : α → M) (h : ∀ a, f a = g a) : (∏ a, f a) = ∏ a, g a :=
77+
Finset.prod_congr rfl fun a _ha => h a
78+
#align fintype.prod_congr Fintype.prod_congr
79+
#align fintype.sum_congr Fintype.sum_congr
80+
81+
@[to_additive]
82+
theorem prod_eq_single {f : α → M} (a : α) (h : ∀ (x) (_ : x ≠ a), f x = 1) : (∏ x, f x) = f a :=
83+
Finset.prod_eq_single a (fun x _ hx => h x hx) fun ha => (ha (Finset.mem_univ a)).elim
84+
#align fintype.prod_eq_single Fintype.prod_eq_single
85+
#align fintype.sum_eq_single Fintype.sum_eq_single
86+
87+
@[to_additive]
88+
theorem prod_eq_mul {f : α → M} (a b : α) (h₁ : a ≠ b) (h₂ : ∀ x, x ≠ a ∧ x ≠ b → f x = 1) :
89+
(∏ x, f x) = f a * f b := by
90+
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx <;>
91+
exact fun hc => (hc (Finset.mem_univ _)).elim
92+
#align fintype.prod_eq_mul Fintype.prod_eq_mul
93+
#align fintype.sum_eq_add Fintype.sum_eq_add
94+
95+
/-- If a product of a `Finset` of a subsingleton type has a given
96+
value, so do the terms in that product. -/
97+
@[to_additive "If a sum of a `Finset` of a subsingleton type has a given
98+
value, so do the terms in that sum."]
99+
theorem eq_of_subsingleton_of_prod_eq {ι : Type _} [Subsingleton ι] {s : Finset ι} {f : ι → M}
100+
{b : M} (h : (∏ i in s, f i) = b) : ∀ i ∈ s, f i = b :=
101+
Finset.eq_of_card_le_one_of_prod_eq (Finset.card_le_one_of_subsingleton s) h
102+
#align fintype.eq_of_subsingleton_of_prod_eq Fintype.eq_of_subsingleton_of_prod_eq
103+
#align fintype.eq_of_subsingleton_of_sum_eq Fintype.eq_of_subsingleton_of_sum_eq
104+
105+
end
106+
107+
end Fintype
108+
109+
open Finset
110+
111+
section
112+
113+
variable {M : Type _} [Fintype α] [CommMonoid M]
114+
115+
@[to_additive (attr := simp)]
116+
theorem Fintype.prod_option (f : Option α → M) : (∏ i, f i) = f none * ∏ i, f (some i) :=
117+
Finset.prod_insertNone f univ
118+
#align fintype.prod_option Fintype.prod_option
119+
#align fintype.sum_option Fintype.sum_option
120+
121+
end
122+
123+
open Finset
124+
125+
@[simp]
126+
nonrec theorem Fintype.card_sigma {α : Type _} (β : α → Type _) [Fintype α] [∀ a, Fintype (β a)] :
127+
Fintype.card (Sigma β) = ∑ a, Fintype.card (β a) :=
128+
card_sigma _ _
129+
#align fintype.card_sigma Fintype.card_sigma
130+
131+
@[simp]
132+
theorem Finset.card_pi [DecidableEq α] {δ : α → Type _} (s : Finset α) (t : ∀ a, Finset (δ a)) :
133+
(s.pi t).card = ∏ a in s, card (t a) :=
134+
Multiset.card_pi _ _
135+
#align finset.card_pi Finset.card_pi
136+
137+
@[simp]
138+
theorem Fintype.card_piFinset [DecidableEq α] [Fintype α] {δ : α → Type _} (t : ∀ a, Finset (δ a)) :
139+
(Fintype.piFinset t).card = ∏ a, card (t a) := by simp [Fintype.piFinset, card_map]
140+
#align fintype.card_pi_finset Fintype.card_piFinset
141+
142+
@[simp]
143+
theorem Fintype.card_pi {β : α → Type _} [DecidableEq α] [Fintype α] [f : ∀ a, Fintype (β a)] :
144+
Fintype.card (∀ a, β a) = ∏ a, Fintype.card (β a) := by
145+
-- Porting note: term mode proof `Fintype.card_piFinset _` no longer works
146+
unfold Fintype.card
147+
erw [Fintype.card_piFinset]
148+
apply Finset.prod_congr rfl
149+
simp [Fintype.card]
150+
#align fintype.card_pi Fintype.card_pi
151+
152+
-- FIXME ouch, this should be in the main file.
153+
@[simp]
154+
theorem Fintype.card_fun [DecidableEq α] [Fintype α] [Fintype β] :
155+
Fintype.card (α → β) = Fintype.card β ^ Fintype.card α := by
156+
rw [Fintype.card_pi, Finset.prod_const]; rfl
157+
#align fintype.card_fun Fintype.card_fun
158+
159+
@[simp]
160+
theorem card_vector [Fintype α] (n : ℕ) : Fintype.card (Vector α n) = Fintype.card α ^ n := by
161+
rw [Fintype.ofEquiv_card]; simp
162+
#align card_vector card_vector
163+
164+
@[to_additive (attr := simp)]
165+
theorem Finset.prod_attach_univ [Fintype α] [CommMonoid β] (f : { a : α // a ∈ @univ α _ } → β) :
166+
(∏ x in univ.attach, f x) = ∏ x, f ⟨x, mem_univ _⟩ :=
167+
Fintype.prod_equiv (Equiv.subtypeUnivEquiv fun x => mem_univ _) _ _ fun x => by simp
168+
#align finset.prod_attach_univ Finset.prod_attach_univ
169+
#align finset.sum_attach_univ Finset.sum_attach_univ
170+
171+
/-- Taking a product over `univ.pi t` is the same as taking the product over `Fintype.piFinset t`.
172+
`univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`, but differ
173+
in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
174+
`Fintype.piFinset t` is a `Finset (Π a, t a)`. -/
175+
@[to_additive "Taking a sum over `univ.pi t` is the same as taking the sum over
176+
`Fintype.piFinset t`. `univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`,
177+
but differ in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
178+
`Fintype.piFinset t` is a `Finset (Π a, t a)`."]
179+
theorem Finset.prod_univ_pi [DecidableEq α] [Fintype α] [CommMonoid β] {δ : α → Type _}
180+
{t : ∀ a : α, Finset (δ a)} (f : (∀ a : α, a ∈ (univ : Finset α) → δ a) → β) :
181+
(∏ x in univ.pi t, f x) = ∏ x in Fintype.piFinset t, f fun a _ => x a := by
182+
refine prod_bij (fun x _ a => x a (mem_univ _)) ?_ (by simp)
183+
(by simp (config := { contextual := true }) [Function.funext_iff]) fun x hx =>
184+
⟨fun a _ => x a, by simp_all⟩
185+
-- Porting note: old proof was `by simp`
186+
intro a ha
187+
simp only [Fintype.piFinset, mem_map, mem_pi, Function.Embedding.coeFn_mk]
188+
exact ⟨a, by simpa using ha, by simp⟩
189+
#align finset.prod_univ_pi Finset.prod_univ_pi
190+
#align finset.sum_univ_pi Finset.sum_univ_pi
191+
192+
/-- The product over `univ` of a sum can be written as a sum over the product of sets,
193+
`Fintype.piFinset`. `Finset.prod_sum` is an alternative statement when the product is not
194+
over `univ` -/
195+
theorem Finset.prod_univ_sum [DecidableEq α] [Fintype α] [CommSemiring β] {δ : α → Type u_1}
196+
[∀ a : α, DecidableEq (δ a)] {t : ∀ a : α, Finset (δ a)} {f : ∀ a : α, δ a → β} :
197+
(∏ a, ∑ b in t a, f a b) = ∑ p in Fintype.piFinset t, ∏ x, f x (p x) := by
198+
simp only [Finset.prod_attach_univ, prod_sum, Finset.sum_univ_pi]
199+
#align finset.prod_univ_sum Finset.prod_univ_sum
200+
201+
/-- Summing `a^s.card * b^(n-s.card)` over all finite subsets `s` of a fintype of cardinality `n`
202+
gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that
203+
`x^n` is multilinear, but multilinear maps are only available now over rings, so we give instead
204+
a proof reducing to the usual binomial theorem to have a result over semirings. -/
205+
theorem Fintype.sum_pow_mul_eq_add_pow (α : Type _) [Fintype α] {R : Type _} [CommSemiring R]
206+
(a b : R) :
207+
(∑ s : Finset α, a ^ s.card * b ^ (Fintype.card α - s.card)) = (a + b) ^ Fintype.card α :=
208+
Finset.sum_pow_mul_eq_add_pow _ _ _
209+
#align fintype.sum_pow_mul_eq_add_pow Fintype.sum_pow_mul_eq_add_pow
210+
211+
@[to_additive]
212+
theorem Function.Bijective.prod_comp [Fintype α] [Fintype β] [CommMonoid γ] {f : α → β}
213+
(hf : Function.Bijective f) (g : β → γ) : (∏ i, g (f i)) = ∏ i, g i :=
214+
Fintype.prod_bijective f hf _ _ fun _x => rfl
215+
#align function.bijective.prod_comp Function.Bijective.prod_comp
216+
#align function.bijective.sum_comp Function.Bijective.sum_comp
217+
218+
@[to_additive]
219+
theorem Equiv.prod_comp [Fintype α] [Fintype β] [CommMonoid γ] (e : α ≃ β) (f : β → γ) :
220+
(∏ i, f (e i)) = ∏ i, f i :=
221+
e.bijective.prod_comp f
222+
#align equiv.prod_comp Equiv.prod_comp
223+
#align equiv.sum_comp Equiv.sum_comp
224+
225+
@[to_additive]
226+
theorem Equiv.prod_comp' [Fintype α] [Fintype β] [CommMonoid γ] (e : α ≃ β) (f : α → γ) (g : β → γ)
227+
(h : ∀ i, f i = g (e i)) : (∏ i, f i) = ∏ i, g i :=
228+
(show f = g ∘ e from funext h).symm ▸ e.prod_comp _
229+
#align equiv.prod_comp' Equiv.prod_comp'
230+
#align equiv.sum_comp' Equiv.sum_comp'
231+
232+
/-- It is equivalent to compute the product of a function over `Fin n` or `Finset.range n`. -/
233+
@[to_additive "It is equivalent to sum a function over `fin n` or `finset.range n`."]
234+
theorem Fin.prod_univ_eq_prod_range [CommMonoid α] (f : ℕ → α) (n : ℕ) :
235+
(∏ i : Fin n, f i) = ∏ i in range n, f i :=
236+
calc
237+
(∏ i : Fin n, f i) = ∏ i : { x // x ∈ range n }, f i :=
238+
(Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))).prod_comp' _ _ (by simp)
239+
_ = ∏ i in range n, f i := by rw [← attach_eq_univ, prod_attach]
240+
241+
#align fin.prod_univ_eq_prod_range Fin.prod_univ_eq_prod_range
242+
#align fin.sum_univ_eq_sum_range Fin.sum_univ_eq_sum_range
243+
244+
@[to_additive]
245+
theorem Finset.prod_fin_eq_prod_range [CommMonoid β] {n : ℕ} (c : Fin n → β) :
246+
(∏ i, c i) = ∏ i in Finset.range n, if h : i < n then c ⟨i, h⟩ else 1 := by
247+
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
248+
rintro ⟨i, hi⟩ _
249+
simp only [hi, dif_pos]
250+
#align finset.prod_fin_eq_prod_range Finset.prod_fin_eq_prod_range
251+
#align finset.sum_fin_eq_sum_range Finset.sum_fin_eq_sum_range
252+
253+
@[to_additive]
254+
theorem Finset.prod_toFinset_eq_subtype {M : Type _} [CommMonoid M] [Fintype α] (p : α → Prop)
255+
[DecidablePred p] (f : α → M) : (∏ a in { x | p x }.toFinset, f a) = ∏ a : Subtype p, f a := by
256+
rw [← Finset.prod_subtype]
257+
simp_rw [Set.mem_toFinset]; intro; rfl
258+
#align finset.prod_to_finset_eq_subtype Finset.prod_toFinset_eq_subtype
259+
#align finset.sum_to_finset_eq_subtype Finset.sum_toFinset_eq_subtype
260+
261+
@[to_additive]
262+
theorem Finset.prod_fiberwise [DecidableEq β] [Fintype β] [CommMonoid γ] (s : Finset α) (f : α → β)
263+
(g : α → γ) : (∏ b : β, ∏ a in s.filter fun a => f a = b, g a) = ∏ a in s, g a :=
264+
Finset.prod_fiberwise_of_maps_to (fun _x _ => mem_univ _) _
265+
#align finset.prod_fiberwise Finset.prod_fiberwise
266+
#align finset.sum_fiberwise Finset.sum_fiberwise
267+
268+
@[to_additive]
269+
theorem Fintype.prod_fiberwise [Fintype α] [DecidableEq β] [Fintype β] [CommMonoid γ] (f : α → β)
270+
(g : α → γ) : (∏ b : β, ∏ a : { a // f a = b }, g (a : α)) = ∏ a, g a := by
271+
rw [← (Equiv.sigmaFiberEquiv f).prod_comp, ← univ_sigma_univ, prod_sigma]
272+
rfl
273+
#align fintype.prod_fiberwise Fintype.prod_fiberwise
274+
#align fintype.sum_fiberwise Fintype.sum_fiberwise
275+
276+
nonrec theorem Fintype.prod_dite [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β]
277+
(f : ∀ (a : α) (_ha : p a), β) (g : ∀ (a : α) (_ha : ¬p a), β) :
278+
(∏ a, dite (p a) (f a) (g a)) = (∏ a : { a // p a }, f a a.2) * ∏ a : { a // ¬p a }, g a a.2 :=
279+
by
280+
simp only [prod_dite, attach_eq_univ]
281+
congr 1
282+
· exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // p x } => f x x.2
283+
· exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // ¬p x } => g x x.2
284+
#align fintype.prod_dite Fintype.prod_dite
285+
286+
section
287+
288+
open Finset
289+
290+
variable {α₁ : Type _} {α₂ : Type _} {M : Type _} [Fintype α₁] [Fintype α₂] [CommMonoid M]
291+
292+
@[to_additive]
293+
theorem Fintype.prod_sum_elim (f : α₁ → M) (g : α₂ → M) :
294+
(∏ x, Sum.elim f g x) = (∏ a₁, f a₁) * ∏ a₂, g a₂ :=
295+
prod_disj_sum _ _ _
296+
#align fintype.prod_sum_elim Fintype.prod_sum_elim
297+
#align fintype.sum_sum_elim Fintype.sum_sum_elim
298+
299+
@[to_additive (attr := simp)]
300+
theorem Fintype.prod_sum_type (f : Sum α₁ α₂ → M) :
301+
(∏ x, f x) = (∏ a₁, f (Sum.inl a₁)) * ∏ a₂, f (Sum.inr a₂) :=
302+
prod_disj_sum _ _ _
303+
#align fintype.prod_sum_type Fintype.prod_sum_type
304+
#align fintype.sum_sum_type Fintype.sum_sum_type
305+
306+
end

0 commit comments

Comments
 (0)