Infinite sum over a topological monoid #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This sum is known as unconditionally convergent, as it sums to the same value under all possible permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence.
Note: There are summable sequences which are not unconditionally convergent! The other way holds
generally, see has_sum.tendsto_sum_nat.
References #
- Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)
def
has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(f : β → α)
(a : α) :
Prop
Infinite sum on a topological monoid
The at_top filter on finset β is the limit of all finite sets towards the entire type. So we sum
up bigger and bigger sets. This sum operation is invariant under reordering. In particular,
the function ℕ → ℝ sending n to (-1)^n / (n+1) does not have a
sum for this definition, but a series which is absolutely convergent will have the correct sum.
This is based on Mario Carneiro's
infinite sum df-tsms in Metamath.
For the definition or many statements, α does not need to be a topological monoid. We only add
this assumption later, for the lemmas where it is relevant.
Equations
- has_sum f a = filter.tendsto (λ (s : finset β), s.sum (λ (b : β), f b)) filter.at_top (nhds a)
@[irreducible]
noncomputable
def
tsum
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
{β : Type u_2}
(f : β → α) :
α
∑' i, f i is the sum of f it exists, or 0 otherwise
theorem
summable.has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(ha : summable f) :
theorem
has_sum.summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
(h : has_sum f a) :
summable f
theorem
has_sum_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α] :
has_sum (λ (b : β), 0) 0
Constant zero function has sum 0
theorem
has_sum_empty
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[is_empty β] :
has_sum f 0
theorem
summable_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α] :
summable (λ (b : β), 0)
theorem
summable_empty
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[is_empty β] :
summable f
theorem
tsum_eq_zero_of_not_summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(h : ¬summable f) :
theorem
summable_congr
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
(hfg : ∀ (b : β), f b = g b) :
theorem
summable.congr
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
(hf : summable f)
(hfg : ∀ (b : β), f b = g b) :
summable g
theorem
has_sum.has_sum_of_sum_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α}
(h_eq : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ u'.sum (λ (x : γ), g x) = v'.sum (λ (b : β), f b)))
(hf : has_sum g a) :
has_sum f a
theorem
has_sum_iff_has_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α}
(h₁ : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ u'.sum (λ (x : γ), g x) = v'.sum (λ (b : β), f b)))
(h₂ : ∀ (v : finset β), ∃ (u : finset γ), ∀ (u' : finset γ), u ⊆ u' → (∃ (v' : finset β), v ⊆ v' ∧ v'.sum (λ (b : β), f b) = u'.sum (λ (x : γ), g x))) :
theorem
function.injective.has_sum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → β}
(hg : function.injective g)
(hf : ∀ (x : β), x ∉ set.range g → f x = 0) :
theorem
function.injective.summable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{g : γ → β}
(hg : function.injective g)
(hf : ∀ (x : β), x ∉ set.range g → f x = 0) :
theorem
has_sum_subtype_iff_of_support_subset
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{s : set β}
(hf : function.support f ⊆ s) :
theorem
has_sum_subtype_iff_indicator
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{s : set β} :
theorem
summable_subtype_iff_indicator
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{s : set β} :
@[simp]
theorem
has_sum_subtype_support
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α} :
theorem
has_sum_fintype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[fintype β]
(f : β → α) :
has_sum f (finset.univ.sum (λ (b : β), f b))
@[protected]
theorem
finset.has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(s : finset β)
(f : β → α) :
@[protected]
theorem
finset.summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(s : finset β)
(f : β → α) :
@[protected]
theorem
set.finite.summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{s : set β}
(hs : s.finite)
(f : β → α) :
theorem
has_sum_sum_of_ne_finset_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{s : finset β}
(hf : ∀ (b : β), b ∉ s → f b = 0) :
If a function f vanishes outside of a finite set s, then it has_sum ∑ b in s, f b.
theorem
summable_of_ne_finset_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{s : finset β}
(hf : ∀ (b : β), b ∉ s → f b = 0) :
summable f
theorem
has_sum_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(b : β)
(hf : ∀ (b' : β), b' ≠ b → f b' = 0) :
has_sum f (f b)
theorem
has_sum_ite_eq
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(b : β)
[decidable_pred (λ (_x : β), _x = b)]
(a : α) :
theorem
has_sum_pi_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[decidable_eq β]
(b : β)
(a : α) :
theorem
equiv.has_sum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
(e : γ ≃ β) :
theorem
function.injective.has_sum_range_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → β}
(hg : function.injective g) :
theorem
equiv.summable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(e : γ ≃ β) :
theorem
summable.prod_symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β × γ → α}
(hf : summable f) :
theorem
equiv.has_sum_iff_of_support
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α}
(e : ↥(function.support f) ≃ ↥(function.support g))
(he : ∀ (x : ↥(function.support f)), g ↑(⇑e x) = f ↑x) :
theorem
has_sum_iff_has_sum_of_ne_zero_bij
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α}
(i : ↥(function.support g) → β)
(hi : ∀ ⦃x y : ↥(function.support g)⦄, i x = i y → ↑x = ↑y)
(hf : function.support f ⊆ set.range i)
(hfg : ∀ (x : ↥(function.support g)), f (i x) = g ↑x) :
theorem
equiv.summable_iff_of_support
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{g : γ → α}
(e : ↥(function.support f) ≃ ↥(function.support g))
(he : ∀ (x : ↥(function.support f)), g ↑(⇑e x) = f ↑x) :
@[protected]
theorem
has_sum.map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
[add_comm_monoid γ]
[topological_space γ]
(hf : has_sum f a)
{G : Type u_4}
[add_monoid_hom_class G α γ]
(g : G)
(hg : continuous ⇑g) :
@[protected]
theorem
summable.map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[add_comm_monoid γ]
[topological_space γ]
(hf : summable f)
{G : Type u_4}
[add_monoid_hom_class G α γ]
(g : G)
(hg : continuous ⇑g) :
@[protected]
theorem
summable.map_iff_of_left_inverse
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[add_comm_monoid γ]
[topological_space γ]
{G : Type u_4}
{G' : Type u_5}
[add_monoid_hom_class G α γ]
[add_monoid_hom_class G' γ α]
(g : G)
(g' : G')
(hg : continuous ⇑g)
(hg' : continuous ⇑g')
(hinv : function.left_inverse ⇑g' ⇑g) :
@[protected]
theorem
summable.map_iff_of_equiv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[add_comm_monoid γ]
[topological_space γ]
{G : Type u_4}
[add_equiv_class G α γ]
(g : G)
(hg : continuous ⇑g)
(hg' : continuous (add_equiv_class.inv g)) :
A special case of summable.map_iff_of_left_inverse for convenience
theorem
has_sum.tendsto_sum_nat
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
{a : α}
{f : ℕ → α}
(h : has_sum f a) :
filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds a)
If f : ℕ → α has sum a, then the partial sums ∑_{i=0}^{n-1} f i converge to a.
theorem
has_sum.unique
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a₁ a₂ : α}
[t2_space α] :
theorem
summable.has_sum_iff_tendsto_nat
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : ℕ → α}
{a : α}
(hf : summable f) :
has_sum f a ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds a)
theorem
function.surjective.summable_iff_of_has_sum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{α' : Type u_4}
[add_comm_monoid α']
[topological_space α']
{e : α' → α}
(hes : function.surjective e)
{f : β → α}
{g : γ → α'}
(he : ∀ {a : α'}, has_sum f (e a) ↔ has_sum g a) :
theorem
has_sum.add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
{a b : α}
[has_continuous_add α]
(hf : has_sum f a)
(hg : has_sum g b) :
theorem
summable.add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
[has_continuous_add α]
(hf : summable f)
(hg : summable g) :
theorem
has_sum_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
{f : γ → β → α}
{a : γ → α}
{s : finset γ} :
theorem
summable_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
{f : γ → β → α}
{s : finset γ}
(hf : ∀ (i : γ), i ∈ s → summable (f i)) :
theorem
has_sum.add_disjoint
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a b : α}
[has_continuous_add α]
{s t : set β}
(hs : disjoint s t)
(ha : has_sum (f ∘ coe) a)
(hb : has_sum (f ∘ coe) b) :
theorem
has_sum.add_is_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a b : α}
[has_continuous_add α]
{s t : set β}
(hs : is_compl s t)
(ha : has_sum (f ∘ coe) a)
(hb : has_sum (f ∘ coe) b) :
theorem
has_sum.add_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a b : α}
[has_continuous_add α]
{s : set β}
(ha : has_sum (f ∘ coe) a)
(hb : has_sum (f ∘ coe) b) :
theorem
summable.add_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[has_continuous_add α]
{s : set β}
(hs : summable (f ∘ coe))
(hsc : summable (f ∘ coe)) :
summable f
theorem
has_sum.compl_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a b : α}
[has_continuous_add α]
{s : set β}
(ha : has_sum (f ∘ coe) a)
(hb : has_sum (f ∘ coe) b) :
theorem
has_sum.even_add_odd
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
{a b : α}
[has_continuous_add α]
{f : ℕ → α}
(he : has_sum (λ (k : ℕ), f (2 * k)) a)
(ho : has_sum (λ (k : ℕ), f (2 * k + 1)) b) :
theorem
summable.compl_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[has_continuous_add α]
{s : set β}
(hs : summable (f ∘ coe))
(hsc : summable (f ∘ coe)) :
summable f
theorem
summable.even_add_odd
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
{f : ℕ → α}
(he : summable (λ (k : ℕ), f (2 * k)))
(ho : summable (λ (k : ℕ), f (2 * k + 1))) :
summable f
theorem
has_sum.sigma
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
{g : β → α}
{a : α}
(ha : has_sum f a)
(hf : ∀ (b : β), has_sum (λ (c : γ b), f ⟨b, c⟩) (g b)) :
has_sum g a
theorem
has_sum.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{f : β × γ → α}
{g : β → α}
{a : α}
(ha : has_sum f a)
(hf : ∀ (b : β), has_sum (λ (c : γ), f (b, c)) (g b)) :
has_sum g a
If a series f on β × γ has sum a and for each b the restriction of f to {b} × γ
has sum g b, then the series g has sum a.
theorem
summable.sigma'
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
(ha : summable f)
(hf : ∀ (b : β), summable (λ (c : γ b), f ⟨b, c⟩)) :
theorem
has_sum.sigma_of_has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[t3_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
{g : β → α}
{a : α}
(ha : has_sum g a)
(hf : ∀ (b : β), has_sum (λ (c : γ b), f ⟨b, c⟩) (g b))
(hf' : summable f) :
has_sum f a
theorem
has_sum.update'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[add_comm_monoid α]
[t2_space α]
[has_continuous_add α]
{f : β → α}
{a a' : α}
(hf : has_sum f a)
(b : β)
(x : α)
(hf' : has_sum (function.update f b x) a') :
Version of has_sum.update for add_comm_monoid rather than add_comm_group.
Rather than showing that f.update has a specific sum in terms of has_sum,
it gives a relationship between the sums of f and f.update given that both exist.
theorem
eq_add_of_has_sum_ite
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[add_comm_monoid α]
[t2_space α]
[has_continuous_add α]
{f : β → α}
{a : α}
(hf : has_sum f a)
(b : β)
(a' : α)
(hf' : has_sum (λ (n : β), ite (n = b) 0 (f n)) a') :
Version of has_sum_ite_sub_has_sum for add_comm_monoid rather than add_comm_group.
Rather than showing that the ite expression has a specific sum in terms of has_sum,
it gives a relationship between the sums of f and ite (n = b) 0 (f n) given that both exist.
theorem
tsum_zero'
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(hz : is_closed {0}) :
@[simp]
theorem
tsum_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t1_space α] :
theorem
has_sum.tsum_eq
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{a : α}
(ha : has_sum f a) :
theorem
summable.has_sum_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{a : α}
(h : summable f) :
@[simp]
theorem
tsum_empty
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
[is_empty β] :
theorem
sum_eq_tsum_indicator
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(f : β → α)
(s : finset β) :
theorem
tsum_congr
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
(hfg : ∀ (b : β), f b = g b) :
theorem
tsum_fintype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[fintype β]
(f : β → α) :
∑' (b : β), f b = finset.univ.sum (λ (b : β), f b)
theorem
tsum_bool
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(f : bool → α) :
∑' (i : bool), f i = f (decidable.to_bool false) + f (decidable.to_bool true)
theorem
tsum_eq_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
(b : β)
(hf : ∀ (b' : β), b' ≠ b → f b' = 0) :
@[simp]
theorem
tsum_ite_eq
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(b : β)
[decidable_pred (λ (_x : β), _x = b)]
(a : α) :
@[simp]
theorem
tsum_pi_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[decidable_eq β]
(b : β)
(a : α) :
theorem
function.surjective.tsum_eq_tsum_of_has_sum_iff_has_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{α' : Type u_4}
[add_comm_monoid α']
[topological_space α']
{e : α' → α}
(hes : function.surjective e)
(h0 : e 0 = 0)
{f : β → α}
{g : γ → α'}
(h : ∀ {a : α'}, has_sum f (e a) ↔ has_sum g a) :
theorem
equiv.tsum_eq_tsum_of_support
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{g : γ → α}
(e : ↥(function.support f) ≃ ↥(function.support g))
(he : ∀ (x : ↥(function.support f)), g ↑(⇑e x) = f ↑x) :
theorem
tsum_eq_tsum_of_ne_zero_bij
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{g : γ → α}
(i : ↥(function.support g) → β)
(hi : ∀ ⦃x y : ↥(function.support g)⦄, i x = i y → ↑x = ↑y)
(hf : function.support f ⊆ set.range i)
(hfg : ∀ (x : ↥(function.support g)), f (i x) = g ↑x) :
@[simp]
theorem
finset.tsum_subtype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(s : finset β)
(f : β → α) :
theorem
tsum_subtype_eq_of_support_subset
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{s : set β}
(hs : function.support f ⊆ s) :
@[simp]
theorem
tsum_singleton
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(b : β)
(f : β → α) :
theorem
tsum_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{g : γ → β}
(f : β → α)
(hg : function.injective g) :
theorem
tsum_eq_add_tsum_ite'
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[has_continuous_add α]
{f : β → α}
(b : β)
(hf : summable (function.update f b 0)) :
Version of tsum_eq_add_tsum_ite for add_comm_monoid rather than add_comm_group.
Requires a different convergence assumption involving function.update.
theorem
tsum_sigma'
{β : Type u_2}
{δ : Type u_4}
[add_comm_monoid δ]
[topological_space δ]
[t3_space δ]
[has_continuous_add δ]
{γ : β → Type u_1}
{f : (Σ (b : β), γ b) → δ}
(h₁ : ∀ (b : β), summable (λ (c : γ b), f ⟨b, c⟩))
(h₂ : summable f) :
theorem
tsum_prod'
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[add_comm_monoid δ]
[topological_space δ]
[t3_space δ]
[has_continuous_add δ]
{f : β × γ → δ}
(h : summable f)
(h₁ : ∀ (b : β), summable (λ (c : γ), f (b, c))) :
theorem
tsum_comm'
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[add_comm_monoid δ]
[topological_space δ]
[t3_space δ]
[has_continuous_add δ]
{f : β → γ → δ}
(h : summable (function.uncurry f))
(h₁ : ∀ (b : β), summable (f b))
(h₂ : ∀ (c : γ), summable (λ (b : β), f b c)) :
theorem
tsum_supr_decode₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[encodable γ]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(s : γ → β) :
You can compute a sum over an encodably type by summing over the natural numbers and taking a supremum. This is useful for outer measures.
theorem
tsum_Union_decode₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[encodable γ]
(m : set β → α)
(m0 : m ∅ = 0)
(s : γ → set β) :
tsum_supr_decode₂ specialized to the complete lattice of sets.
Some properties about measure-like functions.
These could also be functions defined on complete sublattices of sets, with the property
that they are countably sub-additive.
R will probably be instantiated with (≤) in all applications.
theorem
rel_supr_tsum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[countable γ]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(R : α → α → Prop)
(m_supr : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i)))
(s : γ → β) :
If a function is countably sub-additive then it is sub-additive on countable types
theorem
rel_supr_sum
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(R : α → α → Prop)
(m_supr : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i)))
(s : δ → β)
(t : finset δ) :
If a function is countably sub-additive then it is sub-additive on finite sets
theorem
rel_sup_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(R : α → α → Prop)
(m_supr : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i)))
(s₁ s₂ : β) :
If a function is countably sub-additive then it is binary sub-additive
theorem
has_sum.neg
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α}
(h : has_sum f a) :
theorem
summable.neg
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
(hf : summable f) :
theorem
summable.of_neg
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
(hf : summable (λ (b : β), -f b)) :
summable f
theorem
summable_neg_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α} :
theorem
has_sum.sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α}
{a₁ a₂ : α}
(hf : has_sum f a₁)
(hg : has_sum g a₂) :
theorem
summable.sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α}
(hf : summable f)
(hg : summable g) :
theorem
summable.trans_sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α}
(hg : summable g)
(hfg : summable (λ (b : β), f b - g b)) :
summable f
theorem
summable_iff_of_summable_sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α}
(hfg : summable (λ (b : β), f b - g b)) :
theorem
has_sum.update
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a₁ : α}
(hf : has_sum f a₁)
(b : β)
[decidable_eq β]
(a : α) :
has_sum (function.update f b a) (a - f b + a₁)
theorem
summable.update
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
(hf : summable f)
(b : β)
[decidable_eq β]
(a : α) :
summable (function.update f b a)
theorem
has_sum.has_sum_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a₁ a₂ : α}
{s : set β}
(hf : has_sum (f ∘ coe) a₁) :
theorem
has_sum.has_sum_iff_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a₁ a₂ : α}
{s : set β}
(hf : has_sum (f ∘ coe) a₁) :
theorem
summable.summable_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{s : set β}
(hf : summable (f ∘ coe)) :
@[protected]
theorem
finset.has_sum_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α}
(s : finset β) :
@[protected]
theorem
finset.has_sum_iff_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α}
(s : finset β) :
@[protected]
theorem
finset.summable_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
(s : finset β) :
theorem
set.finite.summable_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{s : set β}
(hs : s.finite) :
theorem
has_sum_ite_sub_has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α}
[decidable_eq β]
(hf : has_sum f a)
(b : β) :
theorem
tsum_eq_add_tsum_ite
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
[t2_space α]
[decidable_eq β]
(hf : summable f)
(b : β) :
Let f : β → α be a sequence with summable series and let b ∈ β be an index.
Lemma tsum_eq_add_tsum_ite writes Σ f n as the sum of f b plus the series of the
remaining terms.
Sums on nat #
We show the formula (∑ i in range k, f i) + (∑' i, f (i + k)) = (∑' i, f i), in
sum_add_tsum_nat_add, as well as several results relating sums on ℕ and ℤ.
theorem
has_sum_nat_add_iff
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℕ → α}
(k : ℕ)
{a : α} :
theorem
summable_nat_add_iff
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℕ → α}
(k : ℕ) :
theorem
has_sum_nat_add_iff'
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℕ → α}
(k : ℕ)
{a : α} :
theorem
sum_add_tsum_nat_add
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
[t2_space α]
{f : ℕ → α}
(k : ℕ)
(h : summable f) :
theorem
tsum_eq_zero_add
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
[t2_space α]
{f : ℕ → α}
(hf : summable f) :
theorem
tendsto_sum_nat_add
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
[t2_space α]
(f : ℕ → α) :
filter.tendsto (λ (i : ℕ), ∑' (k : ℕ), f (k + i)) filter.at_top (nhds 0)
For f : ℕ → α, then ∑' k, f (k + i) tends to zero. This does not require a summability
assumption on f, as otherwise all sums are zero.
theorem
has_sum.int_rec
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{a b : α}
{f g : ℕ → α}
(hf : has_sum f a)
(hg : has_sum g b) :
If f₀, f₁, f₂, ... and g₀, g₁, g₂, ... are both convergent then so is the ℤ-indexed
sequence: ..., g₂, g₁, g₀, f₀, f₁, f₂, ....
theorem
has_sum.nonneg_add_neg
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{a b : α}
{f : ℤ → α}
(hnonneg : has_sum (λ (n : ℕ), f ↑n) a)
(hneg : has_sum (λ (n : ℕ), f (-↑(n.succ))) b) :
theorem
has_sum.pos_add_zero_add_neg
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{a b : α}
{f : ℤ → α}
(hpos : has_sum (λ (n : ℕ), f (↑n + 1)) a)
(hneg : has_sum (λ (n : ℕ), f (-↑(n.succ))) b) :
theorem
summable_int_of_summable_nat
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℤ → α}
(hp : summable (λ (n : ℕ), f ↑n))
(hn : summable (λ (n : ℕ), f (-↑n))) :
summable f
theorem
has_sum.sum_nat_of_sum_int
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
{a : α}
{f : ℤ → α}
(hf : has_sum f a) :
theorem
summable_iff_cauchy_seq_finset
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[complete_space α]
{f : β → α} :
summable f ↔ cauchy_seq (λ (s : finset β), s.sum (λ (b : β), f b))
The Cauchy criterion for infinite sums, also known as the Cauchy convergence test
theorem
cauchy_seq_finset_iff_vanishing
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f : β → α} :
theorem
tendsto_tsum_compl_at_top_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
(f : β → α) :
filter.tendsto (λ (s : finset β), ∑' (b : {x // x ∉ s}), f ↑b) filter.at_top (nhds 0)
The sum over the complement of a finset tends to 0 when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero.
theorem
summable_iff_vanishing
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f : β → α}
[complete_space α] :
theorem
summable.summable_of_eq_zero_or_self
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f g : β → α}
[complete_space α]
(hf : summable f)
(h : ∀ (b : β), g b = 0 ∨ g b = f b) :
summable g
@[protected]
theorem
summable.indicator
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f : β → α}
[complete_space α]
(hf : summable f)
(s : set β) :
theorem
summable.comp_injective
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f : β → α}
[complete_space α]
{i : γ → β}
(hf : summable f)
(hi : function.injective i) :
theorem
summable.subtype
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f : β → α}
[complete_space α]
(hf : summable f)
(s : set β) :
theorem
summable_subtype_and_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
{f : β → α}
[complete_space α]
{s : set β} :
theorem
summable.sigma_factor
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
(ha : summable f)
(b : β) :
theorem
summable.sigma
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
(ha : summable f) :
theorem
summable.prod_factor
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{f : β × γ → α}
(h : summable f)
(b : β) :
summable (λ (c : γ), f (b, c))
theorem
tsum_sigma
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[t0_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
(ha : summable f) :
theorem
tsum_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[t0_space α]
{f : β × γ → α}
(h : summable f) :
theorem
tsum_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[t0_space α]
{f : β → γ → α}
(h : summable (function.uncurry f)) :
theorem
tsum_subtype_add_tsum_subtype_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[t2_space α]
{f : β → α}
(hf : summable f)
(s : set β) :
theorem
sum_add_tsum_subtype_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[t2_space α]
{f : β → α}
(hf : summable f)
(s : finset β) :
theorem
summable.tendsto_cofinite_zero
{α : Type u_1}
{G : Type u_5}
[topological_space G]
[add_comm_group G]
[topological_add_group G]
{f : α → G}
(hf : summable f) :
Series divergence test: if f is a convergent series, then f x tends to zero along
cofinite.
theorem
summable.tendsto_at_top_zero
{G : Type u_5}
[topological_space G]
[add_comm_group G]
[topological_add_group G]
{f : ℕ → G}
(hf : summable f) :
filter.tendsto f filter.at_top (nhds 0)
theorem
has_sum.const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[monoid γ]
[topological_space α]
[add_comm_monoid α]
[distrib_mul_action γ α]
[has_continuous_const_smul γ α]
{f : β → α}
{a : α}
(b : γ)
(hf : has_sum f a) :
theorem
summable.const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[monoid γ]
[topological_space α]
[add_comm_monoid α]
[distrib_mul_action γ α]
[has_continuous_const_smul γ α]
{f : β → α}
(b : γ)
(hf : summable f) :
theorem
tsum_const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[monoid γ]
[topological_space α]
[add_comm_monoid α]
[distrib_mul_action γ α]
[has_continuous_const_smul γ α]
{f : β → α}
[t2_space α]
(b : γ)
(hf : summable f) :
Infinite sums commute with scalar multiplication. Version for scalars living in a monoid, but
requiring a summability hypothesis.
theorem
tsum_const_smul'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[add_comm_monoid α]
{f : β → α}
{γ : Type u_3}
[group γ]
[distrib_mul_action γ α]
[has_continuous_const_smul γ α]
[t2_space α]
(g : γ) :
Infinite sums commute with scalar multiplication. Version for scalars living in a group, but
not requiring any summability hypothesis.
theorem
tsum_const_smul''
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[add_comm_monoid α]
{f : β → α}
{γ : Type u_3}
[division_ring γ]
[module γ α]
[has_continuous_const_smul γ α]
[t2_space α]
(g : γ) :
Infinite sums commute with scalar multiplication. Version for scalars living in a
division_ring; no summability hypothesis. This could be made to work for a
[group_with_zero γ] if there was such a thing as distrib_mul_action_with_zero.
Product and pi types #
theorem
has_sum.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[add_comm_monoid γ]
[topological_space γ]
{f : β → α}
{g : β → γ}
{a : α}
{b : γ}
(hf : has_sum f a)
(hg : has_sum g b) :
has_sum (λ (x : β), (f x, g x)) (a, b)
Multiplicative opposite #
theorem
has_sum.op
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
(hf : has_sum f a) :
has_sum (λ (a : β), mul_opposite.op (f a)) (mul_opposite.op a)
theorem
summable.op
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(hf : summable f) :
summable (mul_opposite.op ∘ f)
theorem
has_sum.unop
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → αᵐᵒᵖ}
{a : αᵐᵒᵖ}
(hf : has_sum f a) :
has_sum (λ (a : β), mul_opposite.unop (f a)) (mul_opposite.unop a)
theorem
summable.unop
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → αᵐᵒᵖ}
(hf : summable f) :
@[simp]
theorem
has_sum_op
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α} :
has_sum (λ (a : β), mul_opposite.op (f a)) (mul_opposite.op a) ↔ has_sum f a
@[simp]
theorem
has_sum_unop
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → αᵐᵒᵖ}
{a : αᵐᵒᵖ} :
has_sum (λ (a : β), mul_opposite.unop (f a)) (mul_opposite.unop a) ↔ has_sum f a
@[simp]
theorem
summable_op
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α} :
summable (λ (a : β), mul_opposite.op (f a)) ↔ summable f
@[simp]
theorem
summable_unop
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → αᵐᵒᵖ} :
summable (λ (a : β), mul_opposite.unop (f a)) ↔ summable f
theorem
tsum_op
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[t2_space α] :
∑' (x : β), mul_opposite.op (f x) = mul_opposite.op (∑' (x : β), f x)
theorem
tsum_unop
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → αᵐᵒᵖ} :
∑' (x : β), mul_opposite.unop (f x) = mul_opposite.unop (∑' (x : β), f x)
Interaction with the star #
theorem
has_sum.star
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[star_add_monoid α]
[has_continuous_star α]
{f : β → α}
{a : α}
(h : has_sum f a) :
has_sum (λ (b : β), has_star.star (f b)) (has_star.star a)
theorem
summable.star
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[star_add_monoid α]
[has_continuous_star α]
{f : β → α}
(hf : summable f) :
summable (λ (b : β), has_star.star (f b))
theorem
summable.of_star
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[star_add_monoid α]
[has_continuous_star α]
{f : β → α}
(hf : summable (λ (b : β), has_star.star (f b))) :
summable f
@[simp]
theorem
summable_star_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[star_add_monoid α]
[has_continuous_star α]
{f : β → α} :
summable (λ (b : β), has_star.star (f b)) ↔ summable f
@[simp]
theorem
summable_star_iff'
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[star_add_monoid α]
[has_continuous_star α]
{f : β → α} :
summable (has_star.star f) ↔ summable f
theorem
tsum_star
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[star_add_monoid α]
[has_continuous_star α]
{f : β → α}
[t2_space α] :
has_star.star (∑' (b : β), f b) = ∑' (b : β), has_star.star (f b)
noncomputable
def
add_action.automorphize
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
[add_group α]
[add_action α β]
(f : β → M) :
quotient (add_action.orbit_rel α β) → M
Given an additive group α acting on a type β, and a function f : β → M,
we automorphize f to a function β ⧸ α → M by summing over α orbits,
b ↦ ∑' (a : α), f(a • b).
Equations
- add_action.automorphize f = quotient.lift (λ (b : β), ∑' (a : α), f (a +ᵥ b)) _
noncomputable
def
mul_action.automorphize
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
[group α]
[mul_action α β]
(f : β → M) :
quotient (mul_action.orbit_rel α β) → M
Given a group α acting on a type β, and a function f : β → M, we "automorphize" f to a
function β ⧸ α → M by summing over α orbits, b ↦ ∑' (a : α), f(a • b).
Equations
- mul_action.automorphize f = quotient.lift (λ (b : β), ∑' (a : α), f (a • b)) _
theorem
mul_action.automorphize_smul_left
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
{R : Type u_6}
[division_ring R]
[module R M]
[has_continuous_const_smul R M]
[group α]
[mul_action α β]
(f : β → M)
(g : quotient (mul_action.orbit_rel α β) → R) :
mul_action.automorphize (g ∘ quotient.mk' • f) = g • mul_action.automorphize f
Automorphization of a function into an R-module distributes, that is, commutes with the
R-scalar multiplication.
theorem
add_action.automorphize_smul_left
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
{R : Type u_6}
[division_ring R]
[module R M]
[has_continuous_const_smul R M]
[add_group α]
[add_action α β]
(f : β → M)
(g : quotient (add_action.orbit_rel α β) → R) :
add_action.automorphize (g ∘ quotient.mk' • f) = g • add_action.automorphize f
Automorphization of a function into an R-module distributes, that is, commutes with the
R-scalar multiplication.
noncomputable
def
quotient_add_group.automorphize
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
{G : Type u_7}
[add_group G]
{Γ : add_subgroup G}
(f : G → M) :
Given a subgroup Γ of an additive group G, and a function f : G → M, we
automorphize f to a function G ⧸ Γ → M by summing over Γ orbits,
g ↦ ∑' (γ : Γ), f(γ • g).
Equations
noncomputable
def
quotient_group.automorphize
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
{G : Type u_7}
[group G]
{Γ : subgroup G}
(f : G → M) :
Given a subgroup Γ of a group G, and a function f : G → M, we "automorphize" f to a
function G ⧸ Γ → M by summing over Γ orbits, g ↦ ∑' (γ : Γ), f(γ • g).
Equations
theorem
quotient_group.automorphize_smul_left
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
{R : Type u_6}
[division_ring R]
[module R M]
[has_continuous_const_smul R M]
{G : Type u_7}
[group G]
{Γ : subgroup G}
(f : G → M)
(g : G ⧸ Γ → R) :
Automorphization of a function into an R-module distributes, that is, commutes with the
R-scalar multiplication.
theorem
quotient_add_group.automorphize_smul_left
{M : Type u_5}
[topological_space M]
[add_comm_monoid M]
[t2_space M]
{R : Type u_6}
[division_ring R]
[module R M]
[has_continuous_const_smul R M]
{G : Type u_7}
[add_group G]
{Γ : add_subgroup G}
(f : G → M)
(g : G ⧸ Γ → R) :
Automorphization of a function into an R-module distributes, that is, commutes with the R
-scalar multiplication.