Applying an infinite sum of functions #
This file provides lemmas for (∏'[L] n, f n) x and (∑'[L] n, f n) x where f is a family of
functions. We state this for FunLike objects that are ContinuousEvalConst. This is applicable
to e.g. ContinuousLinearMap.
theorem
hasProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{F : Type u_4}
[TopologicalSpace β]
[CommMonoid β]
[FunLike F α β]
[TopologicalSpace F]
[CommMonoid F]
[ContinuousEvalConst F α β]
[IsMulApply F α β]
[IsOneApply F α β]
{f : γ → F}
{g : F}
{L : SummationFilter γ}
(hf : HasProd f g L)
(x : α)
:
HasProd (fun (x_1 : γ) => (f x_1) x) (g x) L
See also Pi.hasProd for bare pi type.
theorem
hasSum_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{F : Type u_4}
[TopologicalSpace β]
[AddCommMonoid β]
[FunLike F α β]
[TopologicalSpace F]
[AddCommMonoid F]
[ContinuousEvalConst F α β]
[IsAddApply F α β]
[IsZeroApply F α β]
{f : γ → F}
{g : F}
{L : SummationFilter γ}
(hf : HasSum f g L)
(x : α)
:
HasSum (fun (x_1 : γ) => (f x_1) x) (g x) L
See also Pi.hasSum for bare pi type.
theorem
multipliable_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{F : Type u_4}
[TopologicalSpace β]
[CommMonoid β]
[FunLike F α β]
[TopologicalSpace F]
[CommMonoid F]
[ContinuousEvalConst F α β]
[IsMulApply F α β]
[IsOneApply F α β]
{f : γ → F}
{L : SummationFilter γ}
(hf : Multipliable f L)
(x : α)
:
Multipliable (fun (x_1 : γ) => (f x_1) x) L
See also Pi.multipliable for bare pi type.
theorem
summable_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{F : Type u_4}
[TopologicalSpace β]
[AddCommMonoid β]
[FunLike F α β]
[TopologicalSpace F]
[AddCommMonoid F]
[ContinuousEvalConst F α β]
[IsAddApply F α β]
[IsZeroApply F α β]
{f : γ → F}
{L : SummationFilter γ}
(hf : Summable f L)
(x : α)
:
Summable (fun (x_1 : γ) => (f x_1) x) L
See also Pi.summable for bare pi type.
theorem
tprod_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{F : Type u_4}
[TopologicalSpace β]
[CommMonoid β]
[FunLike F α β]
[TopologicalSpace F]
[CommMonoid F]
[ContinuousEvalConst F α β]
[IsMulApply F α β]
[IsOneApply F α β]
{f : γ → F}
{L : SummationFilter γ}
[T2Space β]
[L.NeBot]
(hf : Multipliable f L)
(x : α)
:
See also Pi.tprod_apply for bare pi type.
theorem
tsum_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{F : Type u_4}
[TopologicalSpace β]
[AddCommMonoid β]
[FunLike F α β]
[TopologicalSpace F]
[AddCommMonoid F]
[ContinuousEvalConst F α β]
[IsAddApply F α β]
[IsZeroApply F α β]
{f : γ → F}
{L : SummationFilter γ}
[T2Space β]
[L.NeBot]
(hf : Summable f L)
(x : α)
:
See also Pi.tsum_apply for bare pi type.