Theory Infinite_Product
theory Infinite_Product
imports Infinite_Products
begin
text ‹The recurring theme of the whole development: the sum theory works because
addition is uniformly continuous on UNIV (one uniformity entourage is invariant
under translation by any constant). Multiplication is not, so the sum proofs
cannot be ported verbatim. It is, however, uniformly continuous away from 0,
and in a product with a non-zero value almost all subproducts lie near 1.›
section ‹Unordered infinite products›
definition HAS_SETPROD :: ‹('a ⇒ 'b :: {semidom, topological_semigroup_mult, t2_space}) ⇒ 'a set ⇒ 'b ⇒ bool›
where has_setprod_def: ‹HAS_SETPROD f A x ⟷ (prod f ⤏ x) (finite_subsets_at_top A)›
abbreviation has_setprod (infixr "has'_setprod" 46) where
"(f has_setprod S) A ≡ HAS_SETPROD f A S"
definition multipliable_on :: "('a ⇒ 'b::{semidom, topological_semigroup_mult, t2_space}) ⇒ 'a set ⇒ bool" (infixr "multipliable'_on" 46) where
"f multipliable_on A ≡ (∃x. (f has_setprod x) A)"
definition strongly_multipliable_on :: "('a ⇒ 'b::{semidom, topological_semigroup_mult, t2_space}) ⇒ 'a set ⇒ bool" (infixr "strongly'_multipliable'_on" 46) where
"f strongly_multipliable_on A ≡ finite {x∈A. f x = 0} ∧ (∃P. (f has_setprod P) {x∈A. f x ≠ 0} ∧ P ≠ 0)"
definition infprod :: "('a ⇒ 'b::{semidom,topological_semigroup_mult,t2_space, t2_space}) ⇒ 'a set ⇒ 'b" where
"infprod f A = (if f multipliable_on A then Lim (finite_subsets_at_top A) (prod f) else 1)"
definition abs_multipliable_on :: "('a ⇒ 'b::real_normed_algebra_1) ⇒ 'a set ⇒ bool" (infixr "abs'_multipliable'_on" 46) where
"f abs_multipliable_on A ⟷ (λx. 1 + norm (f x - 1)) multipliable_on A"
syntax (ASCII)
"_infprod" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::topological_comm_monoid_mult" ("(3INFPROD (_/:_)./ _)" [0, 51, 10] 10)
syntax
"_infprod" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::topological_comm_monoid_mult" ("(2∏⇩∞(_/∈_)./ _)" [0, 51, 10] 10)
translations
"∏⇩∞i∈A. b" ⇌ "CONST infprod (λi. b) A"
syntax (ASCII)
"_univinfprod" :: "pttrn ⇒ 'a ⇒ 'a" ("(3INFPROD _./ _)" [0, 10] 10)
syntax
"_univinfprod" :: "pttrn ⇒ 'a ⇒ 'a" ("(2∏⇩∞_./ _)" [0, 10] 10)
translations
"∏⇩∞x. t" ⇌ "CONST infprod (λx. t) (CONST UNIV)"
syntax (ASCII)
"_qinfprod" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a" ("(3INFPROD _ |/ _./ _)" [0, 0, 10] 10)
syntax
"_qinfprod" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a" ("(2∏⇩∞_ | (_)./ _)" [0, 0, 10] 10)
translations
"∏⇩∞x|P. t" => "CONST infprod (λx. t) {x. P}"
print_translation ‹
let
fun prod_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
if x <> y then raise Match
else
let
val x' = Syntax_Trans.mark_bound_body (x, Tx);
val t' = subst_bound (x', t);
val P' = subst_bound (x', P);
in
Syntax.const @{syntax_const "_qinfprod"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
end
| prod_tr' _ = raise Match;
in [(@{const_syntax infprod}, K prod_tr')] end
›
subsection ‹General properties›
lemma has_setprod_imp_multipliable: "(f has_setprod S) A ⟹ f multipliable_on A"
by (auto simp: multipliable_on_def)
lemma has_setprodI:
assumes "((λX. ∏x∈X. f x) ⤏ P) (finite_subsets_at_top A)"
shows "(f has_setprod P) A"
using assms unfolding has_setprod_def .
lemma has_setprodD:
assumes "(f has_setprod P) A"
shows "((λX. ∏x∈X. f x) ⤏ P) (finite_subsets_at_top A)"
using assms unfolding has_setprod_def .
lemma infprodI:
assumes ‹(f has_setprod x) A›
shows ‹infprod f A = x›
using has_setprodD[OF assms] assms unfolding infprod_def multipliable_on_def
by (meson finite_subsets_at_top_neq_bot tendsto_Lim)
lemma infprod_eqI:
fixes f g :: ‹'a ⇒ 'b::{semidom, topological_semigroup_mult, t2_space}›
assumes ‹x = y›
assumes ‹(f has_setprod x) A›
assumes ‹(g has_setprod y) B›
shows ‹infprod f A = infprod g B›
using assms infprodI by blast
lemma infprod_eqI':
fixes f g :: ‹'a ⇒ 'b::{semidom, topological_semigroup_mult, t2_space}›
assumes ‹⋀x. (f has_setprod x) A ⟷ (g has_setprod x) B›
shows ‹infprod f A = infprod g B›
by (metis assms infprod_def infprod_eqI multipliable_on_def)
lemma infprod_not_exists:
fixes f :: ‹'a ⇒ 'b::{semidom, topological_semigroup_mult, t2_space}›
assumes ‹¬ f multipliable_on A›
shows ‹infprod f A = 1›
by (simp add: assms infprod_def)
lemma multipliable_iff_has_setprod_infprod: "f multipliable_on A ⟷ (f has_setprod (infprod f A)) A"
using infprodI multipliable_on_def by metis
lemma has_setprod_infprod[simp]:
assumes ‹f multipliable_on S›
shows ‹(f has_setprod (infprod f S)) S›
using assms multipliable_iff_has_setprod_infprod by blast
lemma filterlim_Un_finite_subsets_at_top:
assumes "finite Y"
shows "filterlim (λX. X ∪ Y) (finite_subsets_at_top (X ∪ Y)) (finite_subsets_at_top X)"
unfolding filterlim_def le_filter_def eventually_filtermap
proof (intro allI impI)
fix P :: "'a set ⇒ bool"
assume "∀⇩F A in finite_subsets_at_top (X ∪ Y). P A"
then obtain A where A: "finite A" "A ⊆ X ∪ Y" "⋀Z. finite Z ⟹ A ⊆ Z ⟹ Z ⊆ X ∪ Y ⟹ P Z"
unfolding eventually_finite_subsets_at_top by metis
show "∀⇩F A in finite_subsets_at_top X. P (A ∪ Y)"
unfolding eventually_finite_subsets_at_top
proof (intro exI allI conjI impI)
show "finite (A - Y)" and "A - Y ⊆ X"
using assms A by auto
next
fix Z assume Z: "finite Z ∧ A - Y ⊆ Z ∧ Z ⊆ X"
show "P (Z ∪ Y)"
by (rule A) (use Z assms in auto)
qed
qed
lemma has_setprod_cong_neutral:
assumes ‹⋀x. x∈T-S ⟹ g x = 1›
assumes ‹⋀x. x∈S-T ⟹ f x = 1›
assumes ‹⋀x. x∈S∩T ⟹ f x = g x›
shows "(f has_setprod x) S ⟷ (g has_setprod x) T"
proof -
have ‹eventually P (filtermap (prod f) (finite_subsets_at_top S))
= eventually P (filtermap (prod g) (finite_subsets_at_top T))› for P
proof
assume ‹eventually P (filtermap (prod f) (finite_subsets_at_top S))›
then obtain F0 where ‹finite F0› and ‹F0 ⊆ S› and F0_P: ‹⋀F. finite F ⟹ F ⊆ S ⟹ F ⊇ F0 ⟹ P (prod f F)›
by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
define F0' where ‹F0' = F0 ∩ T›
have [simp]: ‹finite F0'› ‹F0' ⊆ T›
by (simp_all add: F0'_def ‹finite F0›)
have ‹P (prod g F)› if ‹finite F› ‹F ⊆ T› ‹F ⊇ F0'› for F
proof -
have ‹P (prod f ((F∩S) ∪ (F0∩S)))›
by (intro F0_P) (use ‹F0 ⊆ S› ‹finite F0› that in auto)
also have ‹prod f ((F∩S) ∪ (F0∩S)) = prod g F›
by (intro prod.mono_neutral_cong) (use that ‹finite F0› F0'_def assms in auto)
finally show ?thesis .
qed
with ‹F0' ⊆ T› ‹finite F0'› show ‹eventually P (filtermap (prod g) (finite_subsets_at_top T))›
by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
next
assume ‹eventually P (filtermap (prod g) (finite_subsets_at_top T))›
then obtain F0 where ‹finite F0› and ‹F0 ⊆ T› and F0_P: ‹⋀F. finite F ⟹ F ⊆ T ⟹ F ⊇ F0 ⟹ P (prod g F)›
by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
define F0' where ‹F0' = F0 ∩ S›
have [simp]: ‹finite F0'› ‹F0' ⊆ S›
by (simp_all add: F0'_def ‹finite F0›)
have ‹P (prod f F)› if ‹finite F› ‹F ⊆ S› ‹F ⊇ F0'› for F
proof -
have ‹P (prod g ((F∩T) ∪ (F0∩T)))›
by (intro F0_P) (use ‹F0 ⊆ T› ‹finite F0› that in auto)
also have ‹prod g ((F∩T) ∪ (F0∩T)) = prod f F›
by (intro prod.mono_neutral_cong) (use that ‹finite F0› F0'_def assms in auto)
finally show ?thesis .
qed
with ‹F0' ⊆ S› ‹finite F0'› show ‹eventually P (filtermap (prod f) (finite_subsets_at_top S))›
by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
qed
then have tendsto_x: "(prod f ⤏ x) (finite_subsets_at_top S) ⟷ (prod g ⤏ x) (finite_subsets_at_top T)" for x
by (simp add: le_filter_def filterlim_def)
then show ?thesis
by (simp add: has_setprod_def)
qed
lemma has_setprod_cong:
assumes "⋀x. x∈A ⟹ f x = g x"
shows "(f has_setprod x) A ⟷ (g has_setprod x) A"
using assms by (intro has_setprod_cong_neutral) auto
lemma has_setprod_mult:
assumes ‹(f has_setprod a) A›
assumes ‹(g has_setprod b) A›
shows ‹((λx. f x * g x) has_setprod (a * b)) A›
proof -
from assms have lim_f: ‹(prod f ⤏ a) (finite_subsets_at_top A)›
and lim_g: ‹(prod g ⤏ b) (finite_subsets_at_top A)›
by (simp_all add: has_setprod_def)
then have lim: ‹(prod (λx. f x * g x) ⤏ a * b) (finite_subsets_at_top A)›
unfolding prod.distrib by (rule tendsto_mult)
then show ?thesis using assms
by (simp_all add: has_setprod_def)
qed
lemma has_setprod_Un_disjoint:
assumes "(f has_setprod a) A"
assumes "(f has_setprod b) B"
assumes disj: "A ∩ B = {}"
shows ‹(f has_setprod (a * b)) (A ∪ B)›
proof -
define fA fB where ‹fA x = (if x ∈ A then f x else 1)›
and ‹fB x = (if x ∉ A then f x else 1)› for x
have "(f has_setprod a) A ⟷ (fA has_setprod a) (A ∪ B)"
by (intro has_setprod_cong_neutral) (auto simp: fA_def)
with assms(1) have fA: ‹(fA has_setprod a) (A ∪ B)›
by blast
have "(f has_setprod b) B ⟷ (fB has_setprod b) (A ∪ B)"
using disj by (intro has_setprod_cong_neutral) (auto simp: fB_def)
with assms(2) have fB: ‹(fB has_setprod b) (A ∪ B)›
by blast
have fAB: ‹f x = fA x * fB x› for x
unfolding fA_def fB_def by simp
show ?thesis
unfolding fAB
using fA fB by (rule has_setprod_mult)
qed
lemma has_setprod_finite:
assumes "finite A"
shows "(f has_setprod (∏x∈A. f x)) A"
using assms by (auto simp: finite_subsets_at_top_finite has_setprod_def principal_eq_bot_iff)
lemma has_setprod_unique: "(f has_setprod P) A ⟹ (f has_setprod P') A ⟹ P = P'"
using has_setprodD tendsto_unique finite_subsets_at_top_neq_bot by metis
lemma has_setprod_finite_iff [simp]:
assumes "finite A"
shows "(f has_setprod P) A ⟷ P = (∏x∈A. f x)"
using has_setprod_finite assms has_setprod_unique by fast
lemma multipliable_on_cong_neutral:
assumes ‹⋀x. x∈T-S ⟹ g x = 1›
assumes ‹⋀x. x∈S-T ⟹ f x = 1›
assumes ‹⋀x. x∈S∩T ⟹ f x = g x›
shows "f multipliable_on S ⟷ g multipliable_on T"
using has_setprod_cong_neutral[of T S g f, OF assms]
by (simp add: multipliable_on_def)
lemma infprod_cong_neutral:
assumes ‹⋀x. x∈T-S ⟹ g x = 1›
assumes ‹⋀x. x∈S-T ⟹ f x = 1›
assumes ‹⋀x. x∈S∩T ⟹ f x = g x›
shows ‹infprod f S = infprod g T›
by (smt (verit, best) assms has_setprod_cong_neutral infprod_eqI')
lemma multipliable_on_cong:
assumes "⋀x. x∈A ⟹ f x = g x"
shows "f multipliable_on A ⟷ g multipliable_on A"
by (metis assms multipliable_on_def has_setprod_cong)
lemma abs_multipliable_on_cong_neutral:
assumes ‹⋀x. x∈T-S ⟹ g x = 1›
assumes ‹⋀x. x∈S-T ⟹ f x = 1›
assumes ‹⋀x. x∈S∩T ⟹ f x = g x›
shows "f abs_multipliable_on S ⟷ g abs_multipliable_on T"
unfolding abs_multipliable_on_def by (intro multipliable_on_cong_neutral) (use assms in auto)
lemma abs_multipliable_on_cong:
assumes "⋀x. x∈A ⟹ f x = g x"
shows "f abs_multipliable_on A ⟷ g abs_multipliable_on A"
unfolding abs_multipliable_on_def by (intro multipliable_on_cong) (use assms in auto)
lemma infprod_cong:
assumes "⋀x. x∈A ⟹ f x = g x"
shows "infprod f A = infprod g A"
using assms infprod_eqI' has_setprod_cong by blast
lemma multipliable_on_cofin_subset:
fixes f :: ‹'a ⇒ 'b::real_normed_field›
assumes "f multipliable_on A" and "finite F" and "⋀x. x ∈ F ⟹ f x ≠ 0"
shows "f multipliable_on (A - F)"
proof -
define G where ‹G = A ∩ F›
have G_fin: ‹finite G›
using assms(2) unfolding G_def by blast
have G_sub: ‹G ⊆ A›
unfolding G_def by blast
have G_nz: ‹prod f G ≠ 0›
unfolding G_def using assms(2,3)
by (subst prod_zero_iff) auto
from assms(1) obtain p where hp: ‹(f has_setprod p) A›
unfolding multipliable_on_def by blast
then have lim: ‹(prod f ⤏ p) (finite_subsets_at_top A)›
unfolding has_setprod_def .
have filt: ‹filterlim (λX. X ∪ G) (finite_subsets_at_top A) (finite_subsets_at_top (A - F))›
unfolding filterlim_def le_filter_def eventually_filtermap
proof (intro allI impI)
fix P assume ‹∀⇩F X in finite_subsets_at_top A. P X›
then obtain X0 where X0: ‹finite X0› ‹X0 ⊆ A›
and X0_P: ‹⋀X. finite X ⟹ X0 ⊆ X ⟹ X ⊆ A ⟹ P X›
unfolding eventually_finite_subsets_at_top by metis
show ‹∀⇩F X in finite_subsets_at_top (A - F). P (X ∪ G)›
unfolding eventually_finite_subsets_at_top
proof (intro exI allI conjI impI)
show ‹finite (X0 - F)› using X0(1) by blast
show ‹X0 - F ⊆ A - F› using X0(2) by blast
next
fix X assume X: ‹finite X ∧ X0 - F ⊆ X ∧ X ⊆ A - F›
have ‹X0 ⊆ X ∪ G›
using X X0(2) unfolding G_def by blast
moreover have ‹X ∪ G ⊆ A›
using X G_sub by blast
ultimately show ‹P (X ∪ G)›
by (intro X0_P) (use X G_fin in auto)
qed
qed
have ev_eq: ‹∀⇩F X in finite_subsets_at_top (A - F). prod f (X ∪ G) = prod f X * prod f G›
unfolding eventually_finite_subsets_at_top
proof (intro exI allI conjI impI)
fix X assume X: ‹finite X ∧ {} ⊆ X ∧ X ⊆ A - F›
then have ‹X ∩ G = {}› unfolding G_def by blast
then show ‹prod f (X ∪ G) = prod f X * prod f G›
using X G_fin by (subst prod.union_disjoint) auto
qed auto
have ‹(prod f ⤏ p) (filtermap (λX. X ∪ G) (finite_subsets_at_top (A - F)))›
using lim filt by (metis filterlim_def tendsto_mono)
then have comp: ‹((λX. prod f (X ∪ G)) ⤏ p) (finite_subsets_at_top (A - F))›
by (metis filterlim_filtermap)
have ‹((λX. prod f X * prod f G) ⤏ p) (finite_subsets_at_top (A - F))›
using comp ev_eq by (rule Lim_transform_eventually)
then have ‹((λX. prod f X * prod f G) ⤏ (p / prod f G) * prod f G) (finite_subsets_at_top (A - F))›
by (simp add: G_nz)
then have ‹(prod f ⤏ p / prod f G) (finite_subsets_at_top (A - F))›
using G_nz by (subst (asm) tendsto_mult_right_iff)
thus ?thesis
unfolding multipliable_on_def has_setprod_def by blast
qed
lemma zero_imp_has_setprod_0:
assumes "x ∈ A" "f x = 0"
shows "(f has_setprod 0) A"
proof -
have "eventually (λX. {x} ⊆ X ∧ finite X) (finite_subsets_at_top A)"
unfolding eventually_finite_subsets_at_top using assms by force
hence "eventually (λX. prod f X = 0) (finite_subsets_at_top A)"
by eventually_elim (use assms in auto)
thus ?thesis
unfolding has_setprod_def using tendsto_eventually by blast
qed
lemma
fixes a b :: "'a::real_normed_field"
assumes ‹(f has_setprod b) B› and ‹(f has_setprod a) A› and AB: "A ⊆ B"
assumes [simp]: "a ≠ 0"
shows has_setprod_Diff: "(f has_setprod (b / a)) (B - A)"
proof -
have nonzero: "f x ≠ 0" if "x ∈ A" for x
using that assms(2) using zero_imp_has_setprod_0[of x A f] has_setprod_unique
by fastforce
have finite_subsets1:
"finite_subsets_at_top (B - A) ≤ filtermap (λF. F - A) (finite_subsets_at_top B)"
proof (rule filter_leI)
fix P assume "eventually P (filtermap (λF. F - A) (finite_subsets_at_top B))"
then obtain X where "finite X" and "X ⊆ B"
and P: "finite Y ∧ X ⊆ Y ∧ Y ⊆ B ⟶ P (Y - A)" for Y
unfolding eventually_filtermap eventually_finite_subsets_at_top by auto
hence "finite (X-A)" and "X-A ⊆ B - A"
by auto
moreover have "finite Y ∧ X-A ⊆ Y ∧ Y ⊆ B - A ⟶ P Y" for Y
using P[where Y="Y∪X"] ‹finite X› ‹X ⊆ B›
by (metis Diff_subset Int_Diff Un_Diff finite_Un inf.orderE le_sup_iff sup.orderE sup_ge2)
ultimately show "eventually P (finite_subsets_at_top (B - A))"
unfolding eventually_finite_subsets_at_top by meson
qed
have finite_subsets2:
"filtermap (λF. F ∩ A) (finite_subsets_at_top B) ≤ finite_subsets_at_top A"
using assms unfolding le_filter_def eventually_filtermap eventually_finite_subsets_at_top
by (metis Int_subset_iff finite_Int inf_le2 subset_trans)
have *: "((λF. prod f (F∩A)) ⤏ a) (finite_subsets_at_top B)"
proof (subst asm_rl [of "(λF. prod f (F∩A)) = prod f ∘ (λF. F∩A)"])
show "(λF. prod f (F ∩ A)) = prod f ∘ (λF. F ∩ A)"
unfolding o_def by auto
then show "((prod f ∘ (λF. F ∩ A)) ⤏ a) (finite_subsets_at_top B)"
using tendsto_compose_filtermap finite_subsets2 tendsto_mono assms(2)
by (fastforce simp: has_setprod_def)
qed
have "prod f X / prod f (X ∩ A) = prod f (X - A)"
if "finite X" and "X ⊆ B" for X :: "'b set"
proof (subst prod.Int_Diff[of _ _ A])
have "prod f (X ∩ A) ≠ 0"
using that by (auto simp: nonzero)
thus "prod f (X ∩ A) * prod f (X - A) / prod f (X ∩ A) = prod f (X - A)"
by simp
qed fact+
hence "∀⇩F x in finite_subsets_at_top B. prod f x / prod f (x ∩ A) = prod f (x - A)"
by (rule eventually_finite_subsets_at_top_weakI)
hence "((λF. prod f (F-A)) ⤏ b / a) (finite_subsets_at_top B)"
using * assms tendsto_divide
by (fastforce simp: has_setprod_def cong: tendsto_cong)
hence "(prod f ⤏ b / a) (filtermap (λF. F-A) (finite_subsets_at_top B))"
by (subst tendsto_compose_filtermap[symmetric], simp add: o_def)
thus ?thesis
using finite_subsets1 has_setprod_def tendsto_mono by blast
qed
lemma multipliable_on_finite[simp]:
assumes "finite F"
shows "f multipliable_on F"
using assms multipliable_on_def has_setprod_finite by blast
lemma abs_multipliable_on_finite[simp]:
assumes "finite F"
shows "f abs_multipliable_on F"
unfolding abs_multipliable_on_def using assms by simp
lemma infprod_finite[simp]:
assumes "finite F"
shows "infprod f F = prod f F"
using assms by (simp add: has_setprod_finite infprodI)
lemma has_setprod_finite_approximation:
fixes f :: "'a ⇒ 'b::{semidom,topological_semigroup_mult,metric_space}"
assumes "(f has_setprod x) A" and "ε > 0"
shows "∃F. finite F ∧ F ⊆ A ∧ dist (prod f F) x ≤ ε"
proof -
have "(prod f ⤏ x) (finite_subsets_at_top A)"
by (simp add: assms(1) has_setprodD)
hence *: "∀⇩F F in (finite_subsets_at_top A). dist (prod f F) x < ε"
using assms(2) by (rule tendstoD)
thus ?thesis
unfolding eventually_finite_subsets_at_top by fastforce
qed
lemma infprod_finite_approximation:
fixes f :: "'a ⇒ 'b::{semidom,topological_semigroup_mult,metric_space}"
assumes "f multipliable_on A" and "ε > 0"
shows "∃F. finite F ∧ F ⊆ A ∧ dist (prod f F) (infprod f A) ≤ ε"
by (simp add: assms has_setprod_finite_approximation)
lemma abs_multipliable_multipliable:
fixes f :: ‹'a ⇒ 'b :: {banach, real_normed_div_algebra, semidom}›
assumes ‹f abs_multipliable_on A›
shows ‹f multipliable_on A›
proof -
define g where "g x = 1 + norm (f x - 1)" for x
from assms obtain L where lim: "(prod g ⤏ L) (finite_subsets_at_top A)"
unfolding abs_multipliable_on_def multipliable_on_def has_setprod_def g_def by blast
have g_ge: "g x ≥ 1" for x
unfolding g_def by auto
have g_ge0: "g x ≥ 0" for x
using g_ge[of x] by linarith
have norm_f_le_g: "norm (f x) ≤ g x" for x
using g_def by (metis norm_one norm_triangle_sub)
have norm_prod_le_prod_g: "norm (prod f F) ≤ prod g F" if "finite F" for F
using norm_f_le_g by (metis norm_ge_zero prod_mono prod_norm)
have prod_g_nonneg: "prod g F ≥ 0" if "finite F" for F
by (intro prod_nonneg ballI) (use g_ge0 in auto)
have dist_le: "dist (prod f F1) (prod f F2) ≤ dist (prod g F1) (prod g F2)"
if F12: "F2 ⊆ F1" "finite F1" "F1 ⊆ A" for F1 F2
proof -
from F12 have finF2: "finite F2" using finite_subset by blast
have "prod f F1 = prod f (F1 - F2) * prod f F2"
using prod.subset_diff[OF F12(1,2)] by (simp add: mult.commute)
hence eq1: "prod f F1 - prod f F2 = (prod f (F1 - F2) - 1) * prod f F2"
by (simp add: algebra_simps)
have §: "prod g F1 = prod g (F1 - F2) * prod g F2"
using prod.subset_diff[OF F12(1,2)] by (simp add: mult.commute)
have key1: "norm (prod f (F1 - F2) - 1) ≤ prod g (F1 - F2) - 1"
proof -
have aux: "norm ((∏x∈S. f x) - 1) ≤ (∏x∈S. g x) - 1" if "finite S" for S
using that
proof (induction S)
case empty
then show ?case by simp
next
case (insert x S)
have "norm ((∏y∈insert x S. f y) - 1) = norm (f x * prod f S - 1)"
using insert.hyps by simp
also have "… = norm ((f x - 1) * prod f S + (prod f S - 1))"
by (simp add: algebra_simps)
also have "… ≤ norm ((f x - 1) * prod f S) + norm (prod f S - 1)"
by (rule norm_triangle_ineq)
also have "… = norm (f x - 1) * norm (prod f S) + norm (prod f S - 1)"
by (simp add: norm_mult)
also have "… ≤ norm (f x - 1) * prod g S + (prod g S - 1)"
by (simp add: add_mono insert mult_mono norm_prod_le_prod_g)
also have "… = (1 + norm (f x - 1)) * prod g S - 1"
by (simp add: algebra_simps)
also have "… = g x * prod g S - 1"
unfolding g_def ..
also have "g x * prod g S = (∏y∈insert x S. g y)"
using insert.hyps by simp
finally show ?case by simp
qed
thus ?thesis
using F12(2) by (auto intro: finite_Diff)
qed
have key2: "norm (prod f F2) ≤ prod g F2"
using finF2 by (rule norm_prod_le_prod_g)
have g_diff_ge1: "prod g (F1 - F2) ≥ 1"
by (meson DiffD1 F12(2) finite_Diff g_ge prod_ge_1)
have g_F2_ge0: "prod g F2 ≥ 0"
using finF2 by (rule prod_g_nonneg)
have "norm (prod f F1 - prod f F2) = norm ((prod f (F1 - F2) - 1) * prod f F2)"
by (simp add: eq1)
also have "… = norm (prod f (F1 - F2) - 1) * norm (prod f F2)"
by (rule norm_mult)
also have "… ≤ (prod g (F1 - F2) - 1) * prod g F2"
by (intro mult_mono key1 key2 norm_ge_zero) (use g_diff_ge1 in linarith)
also have "… = prod g F1 - prod g F2"
using § by argo
also have "… ≤ ¦prod g F1 - prod g F2¦"
by linarith
also have "… = dist (prod g F1) (prod g F2)"
unfolding dist_real_def ..
finally show ?thesis unfolding dist_norm .
qed
have cauchy_f: "cauchy_filter (filtermap (prod f) (finite_subsets_at_top A))"
unfolding cauchy_filter_metric_filtermap
proof (intro allI impI)
fix e :: real assume "e > 0"
from lim have cauchy_g: "cauchy_filter (filtermap (prod g) (finite_subsets_at_top A))"
by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)
define d where "d = e / 2"
have "d > 0" using ‹e > 0› unfolding d_def by simp
have "∃P. eventually P (finite_subsets_at_top A) ∧
(∀x y. P x ∧ P y ⟶ dist (prod g x) (prod g y) < d)"
using cauchy_g ‹d > 0› by (simp add: cauchy_filter_metric_filtermap)
then obtain P where ev_P: "eventually P (finite_subsets_at_top A)"
and P_close: "⋀x y. P x ⟹ P y ⟹ dist (prod g x) (prod g y) < d"
by blast
from ev_P obtain F0 where F0: "finite F0" "F0 ⊆ A"
and F0_P: "⋀F. finite F ⟹ F0 ⊆ F ⟹ F ⊆ A ⟹ P F"
unfolding eventually_finite_subsets_at_top by metis
define Q where "Q F ⟷ finite F ∧ F0 ⊆ F ∧ F ⊆ A" for F
have ev_Q: "eventually Q (finite_subsets_at_top A)"
unfolding Q_def eventually_finite_subsets_at_top using F0 by blast
have "dist (prod f x) (prod f y) < e" if "Q x" "Q y" for x y
proof -
define F where "F = x ∪ y"
have F_fin: "finite F" and F_sub: "F ⊆ A" and x_sub: "x ⊆ F" and y_sub: "y ⊆ F"
using that unfolding F_def Q_def by auto
have F0_sub_F: "F0 ⊆ F" using that unfolding F_def Q_def by auto
have "P F" using F0_P F_fin F0_sub_F F_sub by auto
have "P x" using F0_P that unfolding Q_def by auto
have "P y" using F0_P that unfolding Q_def by auto
have fx_le: "dist (prod f F) (prod f x) ≤ dist (prod g F) (prod g x)"
using dist_le[of x F] x_sub F_fin F_sub by auto
have fy_le: "dist (prod f F) (prod f y) ≤ dist (prod g F) (prod g y)"
using dist_le[of y F] y_sub F_fin F_sub by auto
have gx_lt: "dist (prod g F) (prod g x) < d"
using P_close[OF ‹P F› ‹P x›] .
have gy_lt: "dist (prod g F) (prod g y) < d"
using P_close[OF ‹P F› ‹P y›] .
have "dist (prod f x) (prod f y) ≤ dist (prod f F) (prod f x) + dist (prod f F) (prod f y)"
by (rule dist_triangle3)
also have "… ≤ dist (prod g F) (prod g x) + dist (prod g F) (prod g y)"
by (intro add_mono fx_le fy_le)
also have "… < d + d"
by (intro add_strict_mono gx_lt gy_lt)
also have "… = e" unfolding d_def by simp
finally show ?thesis .
qed
thus "∃P. eventually P (finite_subsets_at_top A) ∧
(∀x y. P x ∧ P y ⟶ dist (prod f x) (prod f y) < e)"
using ev_Q by blast
qed
moreover have "complete (UNIV :: 'b set)"
using Cauchy_convergent complete_def convergent_def by blast
ultimately obtain L' where "(prod f ⤏ L') (finite_subsets_at_top A)"
using cauchy_filter_complete_converges[of "filtermap (prod f) (finite_subsets_at_top A)" UNIV]
by (auto simp: filterlim_def filtermap_bot_iff)
thus ?thesis
unfolding multipliable_on_def has_setprod_def by blast
qed
lemma infprod_tendsto:
assumes ‹f multipliable_on S›
shows ‹((λF. prod f F) ⤏ infprod f S) (finite_subsets_at_top S)›
using assms has_setprod_infprod by (simp add: has_setprodD)
lemma has_setprod_1:
assumes ‹⋀x. x ∈ M ⟹ f x = 1›
shows ‹(f has_setprod 1) M›
proof -
have "(f has_setprod 1) M ⟷ ((λ_ :: 'a. 1 :: 'b) has_setprod 1) {}"
by (intro has_setprod_cong_neutral) (use assms in auto)
thus ?thesis
by simp
qed
lemma multipliable_on_1:
assumes ‹⋀x. x∈M ⟹ f x = 1›
shows ‹f multipliable_on M›
using assms multipliable_on_def has_setprod_1 by blast
lemma infprod_1:
assumes ‹⋀x. x∈M ⟹ f x = 1›
shows ‹infprod f M = 1›
using assms by (simp add: has_setprod_1 infprodI)
lemma infprod_0_simp[simp]: ‹infprod (λ_. 1) M = 1›
by (simp_all add: infprod_1)
lemma multipliable_on_0_simp[simp]: ‹(λ_. 1) multipliable_on M›
by (simp_all add: multipliable_on_1)
lemma has_setprod_0_simp[simp]: ‹((λ_. 1) has_setprod 1) M›
by (simp_all add: has_setprod_1)
lemma multipliable_on_mult:
fixes f g :: "'a ⇒ 'b :: {topological_semigroup_mult, field, t2_space}"
assumes ‹f multipliable_on A›
assumes ‹g multipliable_on A›
shows ‹(λx. f x * g x) multipliable_on A›
by (metis (full_types) assms multipliable_on_def has_setprod_mult)
lemma infprod_mult:
fixes f g :: "'a ⇒ 'b :: {topological_semigroup_mult, field, t2_space}"
assumes ‹f multipliable_on A›
assumes ‹g multipliable_on A›
shows ‹infprod (λx. f x * g x) A = infprod f A * infprod g A›
by (simp add: assms has_setprod_mult infprodI)
lemma multipliable_on_Un_disjoint:
fixes f g :: "'a ⇒ 'b :: {topological_semigroup_mult, field, t2_space}"
assumes "f multipliable_on A"
assumes "f multipliable_on B"
assumes disj: "A ∩ B = {}"
shows ‹f multipliable_on (A ∪ B)›
by (meson assms disj multipliable_on_def has_setprod_Un_disjoint)
lemma abs_multipliable_on_Un_disjoint:
fixes f g :: "'a ⇒ 'b :: real_normed_algebra_1"
assumes "f abs_multipliable_on A"
assumes "f abs_multipliable_on B"
assumes disj: "A ∩ B = {}"
shows ‹f abs_multipliable_on (A ∪ B)›
using assms unfolding abs_multipliable_on_def by (intro multipliable_on_Un_disjoint)
lemma infprod_Un_disjoint:
fixes f g :: "'a ⇒ 'b :: {topological_semigroup_mult, field, t2_space}"
assumes "f multipliable_on A"
assumes "f multipliable_on B"
assumes disj: "A ∩ B = {}"
shows ‹infprod f (A ∪ B) = infprod f A * infprod f B›
by (intro infprodI has_setprod_Un_disjoint has_setprod_infprod assms)
lemma abs_convergent_prod_imp_setprod:
fixes f :: "nat ⇒ 'b :: real_normed_field"
assumes "abs_convergent_prod f" and "f has_prod P"
shows "(f has_setprod P) (UNIV :: nat set)"
proof (rule has_setprodI, unfold tendsto_iff, intro allI impI)
fix e :: real assume ‹e > 0›
from assms(2) have seq_lim: ‹(λn. prod f {..n}) ⇢ P›
by (rule has_prod_imp_tendsto)
from assms(1) have ev_nz: ‹∀⇩F n in sequentially. f n ≠ 0›
by (rule abs_convergent_prod_imp_ev_nonzero)
then obtain N0 where N0: ‹⋀n. n ≥ N0 ⟹ f n ≠ 0›
by (auto simp: eventually_at_top_linorder)
define g where ‹g n = 1 + norm (f n - 1)› for n
from assms(1)[unfolded abs_convergent_prod_def]
have abs_conv: ‹convergent_prod g› unfolding g_def .
have g_nz: ‹g n ≠ 0› for n
unfolding g_def by (metis le_add_same_cancel1 norm_ge_zero not_one_le_zero)
then obtain L_abs where L_abs: ‹g has_prod L_abs› and ‹L_abs ≠ 0›
using abs_conv convergent_prod_has_prod prodinf_nonzero by blast
have g_ge1: ‹g n ≥ 1› for n unfolding g_def by auto
have g_ge0: ‹g n ≥ 0› for n using g_ge1[of n] by linarith
from L_abs have g_seq: ‹(λn. prod g {..n}) ⇢ L_abs›
by (rule has_prod_imp_tendsto)
have norm_bound: ‹norm ((∏n∈S. f n) - 1) ≤ (∏n∈S. g n) - 1›
if ‹finite S› for S :: ‹nat set›
using norm_prod_minus1_le_prod_minus1[of ‹λn. f n - 1› S] by (simp add: g_def)
have norm_prod_bound: ‹norm (prod f S) ≤ prod g S›
if ‹finite S› for S :: ‹nat set›
using that
proof induction
case empty
then show ?case by auto
next
case (insert n S)
then show ?case
using norm_bound by (smt (verit) finite_insert norm_one norm_triangle_sub)
qed
have g_partial_le: ‹prod g {..n} ≤ L_abs› for n
proof (rule ccontr)
assume ‹¬ prod g {..n} ≤ L_abs›
then have gt: ‹prod g {..n} > L_abs› by simp
define e' where ‹e' = prod g {..n} - L_abs›
have ‹e' > 0› using gt by (simp add: e'_def)
obtain N' where N': ‹⋀m. m ≥ N' ⟹ dist (prod g {..m}) L_abs < e'›
using ‹0 < e'› g_seq by (metis LIMSEQ_def)
have ‹prod g {..n} ≤ prod g {..max n N'}›
by (intro prod_mono2) (use g_ge1 g_ge0 in auto)
hence ‹dist (prod g {..max n N'}) L_abs ≥ e'›
using gt by (simp add: dist_real_def e'_def)
moreover have ‹dist (prod g {..max n N'}) L_abs < e'›
using N'[of ‹max n N'›] by simp
ultimately show False by linarith
qed
show ‹∀⇩F x in finite_subsets_at_top (UNIV :: nat set). dist (prod f x) P < e›
proof -
obtain N1 where N1: ‹⋀n. n ≥ N1 ⟹ dist (prod f {..n}) P < e/2›
using ‹0 < e› seq_lim by (meson half_gt_zero lim_sequentially)
from g_seq[unfolded tendsto_iff, rule_format, OF half_gt_zero[OF ‹e > 0›]]
obtain N2 where N2: ‹⋀n. n ≥ N2 ⟹ dist (prod g {..n}) L_abs < e/2›
by (auto simp: eventually_at_top_linorder)
define N where ‹N = max N1 N2›
show ?thesis
unfolding eventually_finite_subsets_at_top
proof (intro exI conjI allI impI)
show ‹finite {..N}› by simp
show ‹{..N} ⊆ (UNIV :: nat set)› by simp
next
fix Y
assume Y: ‹finite Y ∧ {..N} ⊆ Y ∧ Y ⊆ UNIV›
then have finY: ‹finite Y› and NY: ‹{..N} ⊆ Y› by auto
define M where ‹M = Max Y›
have ‹Y ≠ {}› using NY by auto
then have MMax: ‹M = Max Y› and MY: ‹Y ⊆ {..M}› and MN: ‹M ≥ N›
using finY NY by (auto simp: M_def intro: Max_ge subset_iff[THEN iffD2])
have finM: ‹finite {..M}› by simp
have factor_f: ‹prod f {..M} = prod f ({..M} - Y) * prod f Y›
using prod.subset_diff[OF MY finM, of f] .
have factor_g: ‹prod g {..M} = prod g ({..M} - Y) * prod g Y›
using prod.subset_diff[OF MY finM, of g] .
have dist_bound: ‹dist (prod f Y) (prod f {..M}) ≤ L_abs - prod g {..N}›
proof -
have ‹dist (prod f Y) (prod f {..M}) = norm (prod f Y - prod f {..M})›
by (simp add: dist_norm)
also have ‹… = norm (prod f Y - prod f ({..M} - Y) * prod f Y)›
by (simp add: factor_f mult.commute)
also have ‹… = norm (prod f Y * (1 - prod f ({..M} - Y)))›
by (simp add: algebra_simps)
also have ‹… = norm (prod f Y) * norm (1 - prod f ({..M} - Y))›
by (simp add: norm_mult)
also have ‹… = norm (prod f Y) * norm (prod f ({..M} - Y) - 1)›
by (metis norm_minus_commute)
also have ‹… ≤ prod g Y * (prod g ({..M} - Y) - 1)›
by (simp add: finY mult_mono' norm_bound norm_prod_bound)
also have ‹… = prod g {..M} - prod g Y›
using factor_g by (simp add: algebra_simps)
also have ‹… ≤ prod g {..M} - prod g {..N}›
by (simp add: NY finY g_ge0 g_ge1 prod_mono2)
also have ‹… ≤ L_abs - prod g {..N}›
using g_partial_le by force
finally show ?thesis .
qed
have tail_bound: ‹L_abs - prod g {..N} < e/2›
proof -
have ‹dist (prod g {..N}) L_abs < e/2›
using N2[of N] by (auto simp: N_def)
moreover have ‹prod g {..N} ≤ L_abs›
using g_partial_le .
ultimately show ?thesis by (simp add: dist_real_def)
qed
have seq_bound: ‹dist (prod f {..M}) P < e/2›
using N1[of M] MN by (auto simp: N_def)
have ‹dist (prod f Y) P ≤ dist (prod f Y) (prod f {..M}) + dist (prod f {..M}) P›
by (rule dist_triangle)
also have ‹… < (L_abs - prod g {..N}) + e/2›
using dist_bound seq_bound by linarith
also have ‹… < e›
using tail_bound by auto
finally show ‹dist (prod f Y) P < e› .
qed
qed
qed
lemma abs_convergent_prod_imp_multipliable_on:
fixes f :: "nat ⇒ 'a :: {real_normed_field,complete_space,comm_ring_1}"
assumes "abs_convergent_prod f"
shows "f multipliable_on UNIV"
unfolding multipliable_on_def
using abs_convergent_prod_imp_convergent_prod abs_convergent_prod_imp_setprod assms
by blast
subsection ‹Subsets›
text ‹
For sums, unordered summability on \<^term>‹A› passes to every subset of \<^term>‹A›
(‹summable_on_subset_banach›). For products the corresponding statement with only the side
condition @{term‹f x ≠ 0›} for @{term‹x ∈ A - B›} is ∗‹false›, and no strengthening of the type class
helps. A counterexample already exists over \<^typ>‹real›: take the index type
\<^typ>‹bool × nat›, let \<^term>‹A = UNIV› and let ‹B› be the ‹True› half, and put
@{term‹f p = (if fst p then -1 else 1/2)›}. The factors ‹1/2› force the partial products over
\<^term>‹A› to tend to ‹0›, so ‹f› is multipliable on \<^term>‹A›, and ‹f› is non-zero
everywhere; but over ‹B› the partial products are ‹1› and ‹-1› alternately, so ‹f› is not
multipliable on ‹B›.
The obstruction is a product equal to ‹0›: it lets the partial products shrink to ‹0› along
\<^term>‹A› while oscillating along ‹B›. Excluding it -- that is, assuming a ∗‹non-zero›
product, equivalently strong multipliability -- makes the subset principle true, and that is
what we prove here. The engine is the multiplicative Cauchy criterion
‹has_setprod_prods_near_1›: multiplication is not uniformly continuous on all of \<^term>‹UNIV›,
which is why the additive proof cannot be transferred, but it is uniformly continuous away
from ‹0›, and for a non-zero product all the far-out subproducts live near ‹1›.
›
text ‹
The multiplicative Cauchy criterion: if the product over \<^term>‹M› converges to a non-zero
limit then, outside a suitable finite set, ∗‹every› finite subproduct is close to ‹1›.
This strengthens ‹has_setprod_factors_tend_to_1› below, which is the special case of
singleton subproducts.
›
lemma has_setprod_prods_near_1:
fixes f :: "'a ⇒ 'b :: {real_normed_div_algebra, comm_monoid_mult}"
assumes lim: "(prod f ⤏ L) (finite_subsets_at_top M)" and nz: "L ≠ 0" and ε: "ε > 0"
shows "∃F. finite F ∧ F ⊆ M ∧ (∀D. finite D ⟶ D ⊆ M - F ⟶ dist (prod f D) 1 < ε)"
proof -
have L0: "norm L > 0"
using nz by simp
define δ where "δ = min (ε * norm L / 4) (norm L / 4)"
have δ0: "δ > 0"
unfolding δ_def using ε L0 by simp
have δ1: "δ ≤ ε * norm L / 4" and δ2: "δ ≤ norm L / 4"
unfolding δ_def by auto
from tendstoD[OF lim δ0] obtain F where F: "finite F" "F ⊆ M"
and Fclose: "⋀Y. finite Y ⟹ F ⊆ Y ⟹ Y ⊆ M ⟹ dist (prod f Y) L < δ"
unfolding eventually_finite_subsets_at_top by metis
have dF: "dist (prod f F) L < δ"
using Fclose F by blast
have "norm L - norm (prod f F - L) ≤ norm (prod f F)"
by (metis dist_commute dist_diff(1) dist_norm norm_triangle_ineq2)
with dF δ2 L0 have normF: "norm (prod f F) > norm L / 2"
unfolding dist_norm by linarith
have "dist (prod f D) 1 < ε" if D: "finite D" "D ⊆ M - F" for D
proof -
have "dist (prod f (F ∪ D)) L < δ"
using Fclose[of "F ∪ D"] F D by auto
with dF have "dist (prod f (F ∪ D)) (prod f F) < 2 * δ"
by (smt (verit) dist_commute dist_triangle)
moreover have "prod f (F ∪ D) = prod f F * prod f D"
using F(1) D by (subst prod.union_disjoint) auto
ultimately have "dist (prod f F * prod f D) (prod f F * 1) < 2 * δ"
by simp
hence "norm (prod f F) * dist (prod f D) 1 < 2 * δ"
by (metis dist_norm norm_mult right_diff_distrib)
hence n_d: "dist (prod f D) 1 * norm (prod f F) < 2 * δ"
by (simp add: mult.commute)
have nF0: "norm (prod f F) > 0"
using normF L0 by linarith
from n_d nF0 have "dist (prod f D) 1 < 2 * δ / norm (prod f F)"
by (simp add: pos_less_divide_eq)
also have "… ≤ 2 * δ / (norm L / 2)"
using normF δ0 L0 nF0 by (intro divide_left_mono mult_pos_pos) auto
also have "… ≤ ε"
using δ1 L0 by (simp add: field_simps)
finally show ?thesis .
qed
with F show ?thesis
by blast
qed
text ‹
For a non-vanishing multipliable family the partial products are uniformly bounded, whatever
the value of the product. (Non-vanishing is essential: if ‹f› has a zero in \<^term>‹M› then
‹f› is multipliable on \<^term>‹M› with product ‹0›, and the remaining partial products are
unconstrained.)
›
lemma multipliable_on_imp_bdd_prods:
fixes f :: "'a ⇒ 'b :: real_normed_field"
assumes lim: "(prod f ⤏ L) (finite_subsets_at_top M)"
and nz: "⋀x. x ∈ M ⟹ f x ≠ 0"
shows "∃C>0. ∀X. finite X ⟶ X ⊆ M ⟶ norm (prod f X) ≤ C"
proof -
from tendstoD[OF lim zero_less_one] obtain F where F: "finite F" "F ⊆ M"
and Fclose: "⋀Y. finite Y ⟹ F ⊆ Y ⟹ Y ⊆ M ⟹ dist (prod f Y) L < 1"
unfolding eventually_finite_subsets_at_top by metis
define m where "m = (∏x∈F. min (norm (f x)) 1)"
have m0: "m > 0"
unfolding m_def using F nz by (intro prod_pos) auto
have m_le: "m ≤ norm (prod f G)" if GF: "G ⊆ F" for G
proof -
have "m = (∏x∈F-G. min (norm (f x)) 1) * (∏x∈G. min (norm (f x)) 1)"
unfolding m_def using GF F(1) by (intro prod.subset_diff)
also have "… ≤ 1 * (∏x∈G. min (norm (f x)) 1)"
by (intro mult_right_mono prod_le_1 prod_nonneg) auto
also have "… = (∏x∈G. min (norm (f x)) 1)"
by simp
also have "… ≤ (∏x∈G. norm (f x))"
by (intro prod_mono) auto
also have "… = norm (prod f G)"
by (simp add: prod_norm)
finally show ?thesis .
qed
have bound: "norm (prod f X) ≤ (norm L + 1) / m" if X: "finite X" "X ⊆ M" for X
proof -
have "prod f (X ∪ F) = prod f (X ∪ (F - X))"
by (simp add: Un_Diff_cancel2)
also have "… = prod f X * prod f (F - X)"
using X(1) F(1) by (intro prod.union_disjoint) auto
finally have eq: "prod f (X ∪ F) = prod f X * prod f (F - X)" .
have "dist (prod f (X ∪ F)) L < 1"
using Fclose[of "X ∪ F"] X F by auto
hence lt: "norm (prod f (X ∪ F)) < norm L + 1"
using norm_triangle_sub[of "prod f (X ∪ F)" L] by (simp add: dist_norm)
have "norm (prod f X) * m ≤ norm (prod f X) * norm (prod f (F - X))"
by (intro mult_left_mono m_le) auto
also have "… < norm L + 1"
using eq lt by (metis norm_mult)
finally have "norm (prod f X) * m ≤ norm L + 1"
by simp
with m0 show ?thesis
by (simp add: mult_imp_le_div_pos)
qed
have "(norm L + 1) / m > 0"
using m0 norm_ge_zero[of L] by (intro divide_pos_pos) linarith+
with bound show ?thesis
by blast
qed
text ‹
If only finitely many factors are dropped, no extra hypothesis beyond non-vanishing of those
factors is needed: one simply divides them out.
›
lemma multipliable_on_subset_finite_Diff:
fixes f :: "'a ⇒ 'b :: real_normed_field"
assumes mult: "f multipliable_on A" and BA: "B ⊆ A" and fin: "finite (A - B)"
and nz: "⋀x. x ∈ A - B ⟹ f x ≠ 0"
shows "f multipliable_on B"
proof -
from mult obtain S where S: "(f has_setprod S) A"
using multipliable_on_def by blast
have "(f has_setprod prod f (A - B)) (A - B)"
using fin by (rule has_setprod_finite)
moreover have "prod f (A - B) ≠ 0"
using fin nz by auto
ultimately have "(f has_setprod (S / prod f (A - B))) (A - (A - B))"
using S by (intro has_setprod_Diff) auto
moreover have "A - (A - B) = B"
using BA by blast
ultimately show ?thesis
using has_setprod_imp_multipliable by metis
qed
text ‹
The subset principle, in the form that is actually true: a product with a ∗‹non-zero› value
restricts to every subset, and the restricted product is again non-zero.
›
lemma has_setprod_subset_nonzero:
fixes f :: "'a ⇒ 'b :: {real_normed_field, complete_space}"
assumes lim: "(f has_setprod L) A" and nz: "L ≠ 0" and BA: "B ⊆ A"
shows "∃P. (f has_setprod P) B ∧ P ≠ 0"
proof -
from lim have limA: "(prod f ⤏ L) (finite_subsets_at_top A)"
by (simp add: has_setprod_def)
have fnz: "f x ≠ 0" if "x ∈ A" for x
using that lim nz has_setprod_unique zero_imp_has_setprod_0[of x A f] by fastforce
have half: "(1/2::real) > 0"
by simp
obtain F1 where F1: "finite F1" "F1 ⊆ A"
and F1_near: "⋀D. finite D ⟹ D ⊆ A - F1 ⟹ dist (prod f D) 1 < 1/2"
using has_setprod_prods_near_1[OF limA nz half] by blast
define c where "c = prod f (F1 ∩ B)"
have c0: "norm c > 0"
unfolding c_def using F1 fnz BA by (simp add: prod_norm prod_pos subset_eq)
have split: "prod f X = c * prod f (X - F1)" if X: "finite X" "F1 ∩ B ⊆ X" "X ⊆ B" for X
using c_def that by (metis inf.absorb_iff2 inf.orderE inf_assoc prod.Int_Diff)
have tail: "norm (prod f (X - F1)) ≤ 3/2" and tail': "norm (prod f (X - F1)) ≥ 1/2"
if X: "finite X" "X ⊆ B" for X
proof -
have less: "norm (prod f (X - F1) - 1) < 1/2"
using X BA by (intro F1_near[unfolded dist_norm]) auto
have n1: "norm (1::'b) = 1"
by simp
show "norm (prod f (X - F1)) ≤ 3/2"
using norm_triangle_ineq2[of "prod f (X - F1)" 1] less n1 by linarith
show "norm (prod f (X - F1)) ≥ 1/2"
using norm_triangle_ineq2[of 1 "prod f (X - F1)"] less n1
norm_minus_commute[of 1 "prod f (X - F1)"] by linarith
qed
have upper: "norm (prod f X) ≤ 3/2 * norm c" and lower: "norm (prod f X) ≥ norm c / 2"
if X: "finite X" "F1 ∩ B ⊆ X" "X ⊆ B" for X
proof -
have "norm (prod f X) = norm c * norm (prod f (X - F1))"
using split[OF X] by (simp add: norm_mult)
thus "norm (prod f X) ≤ 3/2 * norm c" and "norm (prod f X) ≥ norm c / 2"
using tail tail' X c0 by (simp_all add: mult_left_mono)
qed
have "cauchy_filter (filtermap (prod f) (finite_subsets_at_top B))"
unfolding cauchy_filter_metric_filtermap
proof (intro allI impI)
fix e :: real assume "e > 0"
define ε where "ε = e / (4 * norm c)"
have ε0: "ε > 0"
unfolding ε_def using ‹e > 0› c0 by simp
obtain F2 where F2: "finite F2" "F2 ⊆ A"
and F2_near: "⋀D. finite D ⟹ D ⊆ A - F2 ⟹ dist (prod f D) 1 < ε"
using has_setprod_prods_near_1[OF limA nz ε0] by blast
define F where "F = F1 ∪ F2"
have Ffin: "finite F" and FA: "F ⊆ A"
unfolding F_def using F1 F2 by auto
define P where "P = (λX. finite X ∧ F ∩ B ⊆ X ∧ X ⊆ B)"
have ev: "eventually P (finite_subsets_at_top B)"
unfolding eventually_finite_subsets_at_top P_def
using Ffin by (intro exI[of _ "F ∩ B"]) auto
have "dist (prod f X) (prod f Y) < e" if "P X" "P Y" for X Y
proof -
from that have X: "finite X" "F ∩ B ⊆ X" "X ⊆ B"
and Y: "finite Y" "F ∩ B ⊆ Y" "Y ⊆ B"
unfolding P_def by auto
have XY: "finite (X ∩ Y)" "F1 ∩ B ⊆ X ∩ Y" "X ∩ Y ⊆ B"
using X Y unfolding F_def by auto
have diff: "X - Y ⊆ A - F2" "Y - X ⊆ A - F2"
using X Y BA unfolding F_def by auto
have "prod f X - prod f Y = prod f (X ∩ Y) * (prod f (X - Y) - prod f (Y - X))"
using X(1) Y(1)
by (metis Int_commute prod.Int_Diff right_diff_distrib)
hence "norm (prod f X - prod f Y)
= norm (prod f (X ∩ Y)) * norm (prod f (X - Y) - prod f (Y - X))"
by (simp add: norm_mult)
also have "… ≤ (3/2 * norm c) * (2 * ε)"
proof (intro mult_mono)
show "norm (prod f (X ∩ Y)) ≤ 3/2 * norm c"
by (rule upper[OF XY])
have "dist (prod f (X - Y)) 1 < ε" "dist (prod f (Y - X)) 1 < ε"
using X Y diff by (auto intro!: F2_near)
thus "norm (prod f (X - Y) - prod f (Y - X)) ≤ 2 * ε"
using norm_triangle_ineq4[of "prod f (X - Y) - 1" "prod f (Y - X) - 1"]
by (simp add: dist_norm)
qed (use ε0 c0 in auto)
also have "… < e"
unfolding ε_def using c0 ‹e > 0› by (simp add: field_simps)
finally show ?thesis
by (simp add: dist_norm)
qed
with ev show "∃P. eventually P (finite_subsets_at_top B)
∧ (∀X Y. P X ∧ P Y ⟶ dist (prod f X) (prod f Y) < e)"
by blast
qed
from cauchy_filter_complete_converges[OF this complete_UNIV]
obtain P where "filtermap (prod f) (finite_subsets_at_top B) ≤ nhds P"
by (auto simp: filtermap_bot_iff)
hence limB: "(prod f ⤏ P) (finite_subsets_at_top B)"
by (simp add: filterlim_def)
have "norm c / 2 ≤ norm P"
proof (rule tendsto_lowerbound[OF tendsto_norm[OF limB]])
show "∀⇩F X in finite_subsets_at_top B. norm c / 2 ≤ norm (prod f X)"
unfolding eventually_finite_subsets_at_top
using F1 lower by (intro exI[of _ "F1 ∩ B"]) auto
qed auto
with c0 have "P ≠ 0"
by auto
with limB show ?thesis
by (auto simp: has_setprod_def)
qed
corollary multipliable_on_subset_nonzero:
fixes f :: "'a ⇒ 'b :: {real_normed_field, complete_space}"
assumes "(f has_setprod L) A" and "L ≠ 0" and "B ⊆ A"
shows "f multipliable_on B"
using has_setprod_subset_nonzero[OF assms] has_setprod_imp_multipliable by blast
text ‹
A non-zero product splits along any decomposition of the index set. Note that this needs the
subset principle: without it one does not know that either part is multipliable at all.
›
lemma infprod_split:
fixes f :: "'a ⇒ 'b :: {real_normed_field, complete_space}"
assumes mult: "f multipliable_on A" and nz: "infprod f A ≠ 0" and BA: "B ⊆ A"
shows "infprod f A = infprod f B * infprod f (A - B)"
proof -
have P: "(f has_setprod infprod f A) A"
using mult by (rule has_setprod_infprod)
obtain Q where Q: "(f has_setprod Q) B" "Q ≠ 0"
using has_setprod_subset_nonzero[OF P nz BA] by blast
obtain R where R: "(f has_setprod R) (A - B)" "R ≠ 0"
using has_setprod_subset_nonzero[OF P nz Diff_subset] by blast
have "(f has_setprod Q * R) (B ∪ (A - B))"
using Q(1) R(1) by (intro has_setprod_Un_disjoint) auto
moreover have "B ∪ (A - B) = A"
using BA by auto
ultimately have "(f has_setprod Q * R) A"
by simp
with P show ?thesis
using Q(1) R(1) infprodI by blast
qed
text ‹
In the language of strong multipliability the subset principle takes its cleanest form:
it is simply inherited by subsets.
›
lemma strongly_multipliable_on_subset:
fixes f :: "'a ⇒ 'b :: {real_normed_field, complete_space}"
assumes A: "f strongly_multipliable_on A" and BA: "B ⊆ A"
shows "f strongly_multipliable_on B"
proof -
from A obtain P where P: "finite {x∈A. f x = 0}" "(f has_setprod P) {x∈A. f x ≠ 0}" "P ≠ 0"
by (auto simp: strongly_multipliable_on_def)
have "{x∈B. f x ≠ 0} ⊆ {x∈A. f x ≠ 0}"
using BA by blast
from has_setprod_subset_nonzero[OF P(2) P(3) this]
obtain Q where Q: "(f has_setprod Q) {x∈B. f x ≠ 0}" "Q ≠ 0"
by blast
have "finite {x∈B. f x = 0}"
by (rule finite_subset[OF _ P(1)]) (use BA in auto)
with Q show ?thesis
unfolding strongly_multipliable_on_def by blast
qed
lemma has_setprod_empty[simp]: ‹(f has_setprod 1) {}›
by (meson ex_in_conv has_setprod_1)
lemma multipliable_on_empty[simp]: ‹f multipliable_on {}›
by auto
lemma infprod_empty[simp]: ‹infprod f {} = 1›
by simp
lemma prod_has_setprod:
fixes f :: ‹'a ⇒ 'b::{banach, field, topological_semigroup_mult}›
assumes ‹finite A›
assumes ‹⋀a. a ∈ A ⟹ (f has_setprod (s a)) (B a)›
assumes ‹⋀a a'. a∈A ⟹ a'∈A ⟹ a≠a' ⟹ B a ∩ B a' = {}›
shows ‹(f has_setprod (prod s A)) (⋃a∈A. B a)›
using assms
proof (induction)
case empty
then show ?case
by simp
next
case (insert x A)
have ‹(f has_setprod (s x)) (B x)›
by (simp add: insert.prems)
moreover have IH: ‹(f has_setprod (prod s A)) (⋃a∈A. B a)›
using insert by simp
ultimately have ‹(f has_setprod (s x * prod s A)) (B x ∪ (⋃a∈A. B a))›
using insert by (intro has_setprod_Un_disjoint) auto
then show ?case
using insert.hyps by auto
qed
lemma multipliable_on_finite_union_disjoint:
fixes f :: ‹'a ⇒ 'b::{banach, field, topological_semigroup_mult}›
assumes finite: ‹finite A›
assumes conv: ‹⋀a. a ∈ A ⟹ f multipliable_on (B a)›
assumes disj: ‹⋀a a'. a∈A ⟹ a'∈A ⟹ a≠a' ⟹ B a ∩ B a' = {}›
shows ‹f multipliable_on (⋃a∈A. B a)›
using prod_has_setprod [of A f B] assms unfolding multipliable_on_def by metis
lemma prod_infprod:
fixes f :: ‹'a ⇒ 'b::{banach, field, topological_semigroup_mult}›
assumes finite: ‹finite A›
assumes conv: ‹⋀a. a ∈ A ⟹ f multipliable_on (B a)›
assumes disj: ‹⋀a a'. a∈A ⟹ a'∈A ⟹ a≠a' ⟹ B a ∩ B a' = {}›
shows ‹prod (λa. infprod f (B a)) A = infprod f (⋃a∈A. B a)›
by (metis (no_types, lifting) assms has_setprod_infprod infprodI prod_has_setprod)
lemma has_setprod_comm_multiplicative_general:
fixes f :: ‹'b::{banach, field, topological_semigroup_mult} ⇒ 'c::{banach, field, topological_semigroup_mult}›
assumes f_sum: ‹⋀F. finite F ⟹ F ⊆ S ⟹ prod (f ∘ g) F = f (prod g F)›
assumes cont: ‹f ─x→ f x›
assumes infprod: ‹(g has_setprod x) S›
shows ‹((f ∘ g) has_setprod (f x)) S›
proof -
from infprod have lim_g: ‹(prod g ⤏ x) (finite_subsets_at_top S)›
by (simp add: has_setprod_def)
have ‹((f ∘ prod g) ⤏ f x) (finite_subsets_at_top S)›
proof (rule topological_tendstoI)
fix U assume ‹open U› ‹f x ∈ U›
with cont
obtain V where ‹open V› ‹x ∈ V› and V_sub: ‹⋀y. y ∈ V ⟹ f y ∈ U›
by (metis continuous_at_open continuous_at_open isCont_def)
from lim_g[THEN topological_tendstoD, OF ‹open V› ‹x ∈ V›]
show ‹∀⇩F F in finite_subsets_at_top S. (f ∘ prod g) F ∈ U›
by (eventually_elim) (auto intro: V_sub)
qed
moreover have ‹∀⇩F F in finite_subsets_at_top S. prod (f ∘ g) F = (f ∘ prod g) F›
by (rule eventually_finite_subsets_at_top_weakI) (use f_sum in auto)
ultimately have ‹(prod (f ∘ g) ⤏ f x) (finite_subsets_at_top S)›
using tendsto_cong by blast
then show ?thesis
by (simp add: has_setprod_def)
qed
lemma multipliable_on_comm_multiplicative_general:
fixes f :: ‹'b :: {banach, field, topological_semigroup_mult} ⇒ 'c :: {banach, field, topological_semigroup_mult}›
assumes ‹⋀F. finite F ⟹ F ⊆ S ⟹ prod (f ∘ g) F = f (prod g F)›
assumes ‹⋀x. (g has_setprod x) S ⟹ f ─x→ f x›
assumes ‹g multipliable_on S›
shows ‹(f ∘ g) multipliable_on S›
by (meson assms multipliable_on_def has_setprod_comm_multiplicative_general has_setprod_def infprod_tendsto)
lemma infprod_comm_additive_general:
fixes f :: ‹'b :: {banach, field, topological_semigroup_mult} ⇒ 'c :: {banach, field, topological_semigroup_mult}›
assumes f_sum: ‹⋀F. finite F ⟹ F ⊆ S ⟹ prod (f ∘ g) F = f (prod g F)›
assumes ‹isCont f (infprod g S)›
assumes ‹g multipliable_on S›
shows ‹infprod (f ∘ g) S = f (infprod g S)›
using assms
by (meson has_setprod_comm_multiplicative_general has_setprod_infprod infprodI isCont_def)
lemma has_setprod_reindex:
assumes ‹inj_on h A›
shows ‹(g has_setprod P) (h ` A) ⟷ ((g ∘ h) has_setprod P) A›
proof -
have ‹(g has_setprod P) (h ` A) ⟷ (prod g ⤏ P) (finite_subsets_at_top (h ` A))›
by (simp add: has_setprod_def)
also have ‹… ⟷ ((λF. prod g (h ` F)) ⤏ P) (finite_subsets_at_top A)›
by (metis assms filterlim_filtermap filtermap_image_finite_subsets_at_top)
also have ‹… ⟷ (prod (g ∘ h) ⤏ P) (finite_subsets_at_top A)›
proof (intro tendsto_cong eventually_finite_subsets_at_top_weakI prod.reindex)
show "⋀X. ⟦finite X; X ⊆ A⟧ ⟹ inj_on h X"
using assms inj_on_subset by blast
qed
also have ‹… ⟷ ((g ∘ h) has_setprod P) A›
by (simp add: has_setprod_def)
finally show ?thesis .
qed
lemma multipliable_on_reindex:
assumes ‹inj_on h A›
shows ‹g multipliable_on (h ` A) ⟷ (g ∘ h) multipliable_on A›
by (simp add: assms multipliable_on_def has_setprod_reindex)
lemma infprod_reindex:
assumes ‹inj_on h A›
shows ‹infprod g (h ` A) = infprod (g ∘ h) A›
by (metis assms has_setprod_infprod has_setprod_reindex infprodI infprod_def)
lemma multipliable_on_reindex_bij_betw:
assumes "bij_betw g A B"
shows "(λx. f (g x)) multipliable_on A ⟷ f multipliable_on B"
by (smt (verit) assms bij_betw_def o_apply multipliable_on_cong multipliable_on_reindex)
lemma infprod_reindex_bij_betw:
assumes "bij_betw g A B"
shows "infprod (λx. f (g x)) A = infprod f B"
by (metis (mono_tags, lifting) assms bij_betw_def infprod_cong infprod_reindex o_def)
lemma prod_uniformity:
assumes times_cont: ‹uniformly_continuous_on UNIV (λ(x::'b::{uniform_space,comm_monoid_mult},y). x*y)›
assumes EE: ‹eventually E uniformity›
obtains D where ‹eventually D uniformity›
and ‹⋀M::'a set. ⋀f f' :: 'a ⇒ 'b. card M ≤ n ∧ (∀m∈M. D (f m, f' m)) ⟹ E (prod f M, prod f' M)›
proof (atomize_elim, insert EE, induction n arbitrary: E rule:nat_induct)
case 0
then show ?case
by (metis card_eq_0_iff equals0D le_zero_eq prod.infinite prod.not_neutral_contains_not_neutral uniformity_refl)
next
case (Suc n)
from times_cont[unfolded uniformly_continuous_on_uniformity filterlim_def le_filter_def, rule_format, OF Suc.prems]
obtain D1 D2 where ‹eventually D1 uniformity› and ‹eventually D2 uniformity›
and D1D2E: ‹D1 (x, y) ⟹ D2 (x', y') ⟹ E (x * x', y * y')› for x y x' y'
apply atomize_elim
by (auto simp: eventually_prod_filter case_prod_beta uniformity_prod_def eventually_filtermap)
from Suc.IH[OF ‹eventually D2 uniformity›]
obtain D3 where ‹eventually D3 uniformity› and D3: ‹card M ≤ n ⟹ (∀m∈M. D3 (f m, f' m)) ⟹ D2 (prod f M, prod f' M)›
for M :: ‹'a set› and f f'
by metis
define D where ‹D x ≡ D1 x ∧ D3 x› for x
have ‹eventually D uniformity›
using D_def ‹eventually D1 uniformity› ‹eventually D3 uniformity› eventually_elim2 by blast
have ‹E (prod f M, prod f' M)›
if ‹card M ≤ Suc n› and DM: ‹∀m∈M. D (f m, f' m)›
for M :: ‹'a set› and f f'
proof (cases ‹card M = 0›)
case True
then show ?thesis
by (metis Suc.prems card_eq_0_iff prod.empty prod.infinite uniformity_refl)
next
case False
with ‹card M ≤ Suc n› obtain N x where ‹card N ≤ n› and ‹x ∉ N› and ‹M = insert x N›
by (metis card_Suc_eq less_Suc_eq_0_disj less_Suc_eq_le)
from DM have ‹⋀m. m∈N ⟹ D (f m, f' m)›
using ‹M = insert x N› by blast
with D3[OF ‹card N ≤ n›]
have D2_N: ‹D2 (prod f N, prod f' N)›
using D_def by blast
from DM
have ‹D (f x, f' x)›
using ‹M = insert x N› by blast
then have ‹D1 (f x, f' x)›
by (simp add: D_def)
with D2_N
have ‹E (f x * prod f N, f' x * prod f' N)›
using D1D2E by presburger
then show ‹E (prod f M, prod f' M)›
by (metis False ‹M = insert x N› ‹x ∉ N› card.infinite finite_insert prod.insert)
qed
with ‹eventually D uniformity› show ?case
by auto
qed
text ‹Metric "splitting lemma" for products, the multiplicative replacement for the uniformity
machinery of @{thm [source] prod_uniformity}: a finite product is Lipschitz in its factors,
PROVIDED the factors stay bounded. (Multiplication is uniformly continuous on bounded sets,
which is enough here -- the factors that occur are partial products near the nonzero limits.)›
lemma norm_prod_diff_le:
fixes g g' :: "'i ⇒ 'b :: real_normed_field"
assumes "finite M"
and "⋀m. m ∈ M ⟹ norm (g m) ≤ C" and "⋀m. m ∈ M ⟹ norm (g' m) ≤ C"
and "⋀m. m ∈ M ⟹ norm (g m - g' m) ≤ d" and "C ≥ 1" and "d ≥ 0"
shows "norm (prod g M - prod g' M) ≤ real (card M) * C ^ (card M) * d"
using assms
proof (induction M rule: finite_induct)
case empty
then show ?case by simp
next
case (insert x M)
have gx: "norm (g x) ≤ C" and gM: "⋀m. m ∈ M ⟹ norm (g m) ≤ C" using insert.prems(1) by auto
have g'x: "norm (g' x) ≤ C" and g'M: "⋀m. m ∈ M ⟹ norm (g' m) ≤ C" using insert.prems(2) by auto
have dx: "norm (g x - g' x) ≤ d" and dM: "⋀m. m ∈ M ⟹ norm (g m - g' m) ≤ d" using insert.prems(3) by auto
have C0: "C ≥ 1" and d0: "d ≥ 0" using insert.prems(4,5) by auto
have Cnn: "C ≥ 0" using C0 by simp
have IH: "norm (prod g M - prod g' M) ≤ real (card M) * C ^ (card M) * d"
using insert.IH[OF gM g'M dM C0 d0] .
define P P' where "P = prod g M" and "P' = prod g' M"
have "norm P' = (∏m∈M. norm (g' m))" unfolding P'_def by (simp add: prod_norm)
also have "… ≤ (∏m∈M. C)" by (intro prod_mono conjI g'M) auto
also have "… = C ^ (card M)" by (simp add: prod_constant)
finally have normP': "norm P' ≤ C ^ (card M)" .
have pownn: "C ^ (card M) ≥ 0" using Cnn by simp
have prod_eq: "prod g (insert x M) - prod g' (insert x M) = g x * P - g' x * P'"
using insert.hyps by (simp add: P_def P'_def)
have split: "g x * P - g' x * P' = g x * (P - P') + (g x - g' x) * P'"
by (simp add: algebra_simps)
have B: "norm (g x * P - g' x * P') ≤ norm (g x) * norm (P - P') + norm (g x - g' x) * norm P'"
unfolding split by (smt (verit) norm_triangle_ineq norm_mult)
have step1: "norm (g x) * norm (P - P') ≤ C * (real (card M) * C ^ (card M) * d)"
using IH gx P_def P'_def Cnn by (intro mult_mono) auto
have step2: "norm (g x - g' x) * norm P' ≤ d * C ^ (card M)"
using dx normP' d0 pownn by (intro mult_mono) auto
have "norm (prod g (insert x M) - prod g' (insert x M)) = norm (g x * P - g' x * P')"
by (simp add: prod_eq)
also have "… ≤ C * (real (card M) * C ^ (card M) * d) + d * C ^ (card M)"
using B step1 step2 by linarith
also have "… = real (card M) * (C ^ (Suc (card M))) * d + C ^ (card M) * d"
by (simp add: algebra_simps)
also have "… ≤ real (card M) * (C ^ (Suc (card M))) * d + C ^ (Suc (card M)) * d"
using C0 pownn d0 by (simp add: mult_right_mono mult_left_mono)
also have "… = real (card (insert x M)) * C ^ (card (insert x M)) * d"
using insert.hyps by (simp add: algebra_simps)
finally show ?case .
qed
lemma prod_close_of_factors_close:
fixes M :: "'i set" and C ε :: real
assumes "finite M" and "C ≥ 1" and "ε > 0"
shows "∃δ>0. ∀h h' :: 'i ⇒ 'b :: real_normed_field.
(∀m∈M. norm (h m) ≤ C ∧ norm (h' m) ≤ C ∧ dist (h m) (h' m) < δ)
⟶ dist (prod h M) (prod h' M) < ε"
proof -
define K where "K = real (card M) * C ^ (card M) + 1"
have K0: "K > 0" using assms by (simp add: K_def add_nonneg_pos)
define δ where "δ = ε / K"
have δ0: "δ > 0" using assms K0 by (simp add: δ_def)
have "dist (prod h M) (prod h' M) < ε"
if H: "∀m∈M. norm (h m) ≤ C ∧ norm (h' m) ≤ C ∧ dist (h m) (h' m) < δ"
for h h' :: "'i ⇒ 'b"
proof -
have "norm (prod h M - prod h' M) ≤ real (card M) * C ^ (card M) * δ"
using norm_prod_diff_le assms
by (metis (no_types) H δ0 dist_norm order_less_imp_le that)
also have "… < ε"
using δ0 K0 assms unfolding δ_def K_def by (simp add: field_simps)
finally show ?thesis by (simp add: dist_norm)
qed
thus ?thesis using δ0 by blast
qed
lemma has_setprod_Sigma:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a × 'b ⇒ 'c::real_normed_field›
assumes multipliableAB: "(f has_setprod a) (Sigma A B)"
assumes multipliableB: ‹⋀x. x∈A ⟹ ((λy. f (x, y)) has_setprod b x) (B x)›
shows "(b has_setprod a) A"
proof -
define F FB FA where ‹F = finite_subsets_at_top (Sigma A B)› and ‹FB x = finite_subsets_at_top (B x)›
and ‹FA = finite_subsets_at_top A› for x
from multipliableB
have sum_b: ‹(prod (λy. f (x, y)) ⤏ b x) (FB x)› if ‹x ∈ A› for x
using FB_def[abs_def] has_setprod_def that by auto
from multipliableAB
have sum_S: ‹(prod f ⤏ a) F›
using F_def has_setprod_def by blast
have finite_proj: ‹finite {b| b. (a,b) ∈ H}› if ‹finite H› for H :: ‹('a×'b) set› and a
by (metis (no_types, lifting) finite_imageI finite_subset image_eqI mem_Collect_eq snd_conv subsetI that)
have ‹(prod b ⤏ a) FA›
proof (rule tendsto_iff_uniformity[THEN iffD2, rule_format])
fix E :: ‹('c × 'c) ⇒ bool›
assume ‹eventually E uniformity›
then obtain D where D_uni: ‹eventually D uniformity› and DDE': ‹⋀x y z. D (x, y) ⟹ D (y, z) ⟹ E (x, z)›
by (metis (no_types, lifting) ‹eventually E uniformity› uniformity_transE)
from sum_S obtain G where ‹finite G› and ‹G ⊆ Sigma A B›
and G_sum: ‹G ⊆ H ⟹ H ⊆ Sigma A B ⟹ finite H ⟹ D (prod f H, a)› for H
unfolding tendsto_iff_uniformity
by (metis (mono_tags, lifting) D_uni F_def eventually_finite_subsets_at_top)
have ‹finite (fst ` G)› and ‹fst ` G ⊆ A›
using ‹finite G› ‹G ⊆ Sigma A B› by auto
define Ga where ‹Ga a = {b. (a,b) ∈ G}› for a
have Ga_fin: ‹finite (Ga a)› and Ga_B: ‹Ga a ⊆ B a› for a
using ‹finite G› ‹G ⊆ Sigma A B› finite_proj by (auto simp: Ga_def finite_proj)
have ‹E (prod b M, a)› if ‹M ⊇ fst ` G› and ‹finite M› and ‹M ⊆ A› for M
proof -
define FMB where ‹FMB = finite_subsets_at_top (Sigma M B)›
have ‹eventually (λH. D (∏a∈M. b a, ∏(a,b)∈H. f (a,b))) FMB›
proof -
from D_uni obtain eD where eD0: ‹eD > 0›
and eD_D: ‹⋀x y::'c. dist x y < eD ⟹ D (x, y)›
by (auto simp: eventually_uniformity_metric)
define C where ‹C = Max (insert 1 ((λa. norm (b a) + 1) ` M))›
have C1: ‹C ≥ 1› using ‹finite M› by (simp add: C_def)
have bC: ‹norm (b a) + 1 ≤ C› if ‹a ∈ M› for a
using that ‹finite M› by (simp add: C_def)
obtain δ0 where δ00: ‹δ0 > 0›
and δ0_prod: ‹⋀h h'::'a⇒'c. (∀m∈M. norm (h m) ≤ C ∧ norm (h' m) ≤ C ∧ dist (h m) (h' m) < δ0)
⟹ dist (prod h M) (prod h' M) < eD›
using prod_close_of_factors_close[OF ‹finite M› C1 eD0] by blast
define δ where ‹δ = min δ0 1›
have δ0: ‹δ > 0› using δ00 by (simp add: δ_def)
define D' where ‹D' = (λ(x::'c,y::'c). dist x y < δ)›
have D'_uni: ‹eventually D' uniformity›
unfolding D'_def using δ0 by (auto simp: eventually_uniformity_metric)
obtain Ha where ‹Ha a ⊇ Ga a› and Ha_fin: ‹finite (Ha a)› and Ha_B: ‹Ha a ⊆ B a›
and D'_sum_Ha: ‹Ha a ⊆ L ⟹ L ⊆ B a ⟹ finite L ⟹ D' (b a, prod (λb. f (a,b)) L)› if ‹a ∈ A› for a L
proof -
from sum_b[unfolded tendsto_iff_uniformity, rule_format, OF _ D'_uni[THEN uniformity_sym]]
obtain Ha0 where ‹finite (Ha0 a)› and ‹Ha0 a ⊆ B a›
and ‹Ha0 a ⊆ L ⟹ L ⊆ B a ⟹ finite L ⟹ D' (b a, prod (λb. f (a,b)) L)› if ‹a ∈ A› for a L
unfolding FB_def eventually_finite_subsets_at_top unfolding prod.case by metis
moreover define Ha where ‹Ha a = Ha0 a ∪ Ga a› for a
ultimately show ?thesis
using that[where Ha=Ha] Ga_fin Ga_B by auto
qed
have ‹D (∏a∈M. b a, ∏(a,b)∈H. f (a,b))› if ‹finite H› and ‹H ⊆ Sigma M B› and ‹H ⊇ Sigma M Ha› for H
proof -
define Ha' where ‹Ha' a = {b| b. (a,b) ∈ H}› for a
have [simp]: ‹finite (Ha' a)› and [simp]: ‹Ha' a ⊇ Ha a› and [simp]: ‹Ha' a ⊆ B a› if ‹a ∈ M› for a
unfolding Ha'_def using ‹finite H› ‹H ⊆ Sigma M B› ‹Sigma M Ha ⊆ H› that finite_proj by auto
have ‹Sigma M Ha' = H›
using that by (auto simp: Ha'_def)
then have *: ‹(∏(a,b)∈H. f (a,b)) = (∏a∈M. ∏b∈Ha' a. f (a,b))›
by (simp add: ‹finite M› prod.Sigma)
have D'close: ‹D' (b a, prod (λb. f (a,b)) (Ha' a))› if ‹a ∈ M› for a
using D'_sum_Ha ‹M ⊆ A› that by auto
have bnd: ‹norm (b a) ≤ C ∧ norm (prod (λb. f (a,b)) (Ha' a)) ≤ C
∧ dist (b a) (prod (λb. f (a,b)) (Ha' a)) < δ0› if ‹a ∈ M› for a
proof -
have d1: ‹dist (b a) (prod (λb. f (a,b)) (Ha' a)) < δ›
using D'close[OF that] by (simp add: D'_def)
have nb: ‹norm (b a) ≤ C› using bC[OF that] by simp
have ‹norm (prod (λb. f (a,b)) (Ha' a)) ≤ norm (b a) + dist (b a) (prod (λb. f (a,b)) (Ha' a))›
proof -
have ‹norm (prod (λb. f (a,b)) (Ha' a))
= norm (b a + (prod (λb. f (a,b)) (Ha' a) - b a))› by simp
also have ‹… ≤ norm (b a) + norm (prod (λb. f (a,b)) (Ha' a) - b a)›
by (rule norm_triangle_ineq)
also have ‹norm (prod (λb. f (a,b)) (Ha' a) - b a) = dist (b a) (prod (λb. f (a,b)) (Ha' a))›
by (simp add: dist_norm norm_minus_commute)
finally show ?thesis by simp
qed
also have ‹… ≤ norm (b a) + 1› using d1 by (simp add: δ_def)
also have ‹… ≤ C› using bC[OF that] by simp
finally show ?thesis using nb d1 by (simp add: δ_def)
qed
have ‹dist (∏a∈M. b a) (∏a∈M. prod (λb. f (a,b)) (Ha' a)) < eD›
by (rule δ0_prod) (use bnd in blast)
then have ‹D (∏a∈M. b a, ∏a∈M. prod (λb. f (a,b)) (Ha' a))›
by (rule eD_D)
with * show ?thesis
by auto
qed
moreover have ‹Sigma M Ha ⊆ Sigma M B›
using Ha_B ‹M ⊆ A› by auto
ultimately show ?thesis
unfolding FMB_def eventually_finite_subsets_at_top
by (metis (no_types, lifting) Ha_fin finite_SigmaI subsetD that(2) that(3))
qed
moreover have ‹eventually (λH. D (∏(a,b)∈H. f (a,b), a)) FMB›
unfolding FMB_def eventually_finite_subsets_at_top
proof (rule exI[of _ G], safe)
fix Y assume Y: "finite Y" "G ⊆ Y" "Y ⊆ Sigma M B"
thus "D (∏(a,b)∈Y. f (a, b), a)"
using G_sum[of Y] Y using that(3) by fastforce
qed (use ‹finite G› ‹G ⊆ Sigma A B› that in auto)
ultimately have ‹∀⇩F x in FMB. E (prod b M, a)›
by eventually_elim (use DDE' in auto)
then show ‹E (prod b M, a)›
using FMB_def by force
qed
then show ‹∀⇩F x in FA. E (prod b x, a)›
using ‹finite (fst ` G)› and ‹fst ` G ⊆ A›
by (metis (mono_tags, lifting) FA_def eventually_finite_subsets_at_top)
qed
then show ?thesis
by (simp add: FA_def has_setprod_def)
qed
lemma has_setprod_SigmaI:
fixes f :: "_ ⇒ 'a :: real_normed_field"
assumes f: "⋀x. x ∈ A ⟹ ((λy. f (x, y)) has_setprod g x) (B x)"
assumes g: "(g has_setprod S) A"
assumes multipliable: "f multipliable_on Sigma A B"
shows "(f has_setprod S) (Sigma A B)"
by (metis f g has_setprod_Sigma has_setprod_infprod has_setprod_unique local.multipliable)
lemma multipliable_on_Sigma:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a ⇒ 'b ⇒ 'c::real_normed_field›
assumes multipliableAB: "(λ(x,y). f x y) multipliable_on (Sigma A B)"
assumes multipliableB: ‹⋀x. x∈A ⟹ (f x) multipliable_on (B x)›
shows ‹(λx. infprod (f x) (B x)) multipliable_on A›
proof -
from multipliableAB obtain a where a: ‹((λ(x,y). f x y) has_setprod a) (Sigma A B)›
using has_setprod_infprod by blast
from multipliableB have b: ‹⋀x. x∈A ⟹ (f x has_setprod infprod (f x) (B x)) (B x)›
by (auto intro!: has_setprod_infprod)
show ?thesis
unfolding multipliable_on_def
using a b has_setprod_Sigma by fastforce
qed
lemma infprod_Sigma:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a × 'b ⇒ 'c::real_normed_field›
assumes multipliableAB: "f multipliable_on (Sigma A B)"
assumes multipliableB: ‹⋀x. x∈A ⟹ (λy. f (x, y)) multipliable_on (B x)›
shows "infprod f (Sigma A B) = infprod (λx. infprod (λy. f (x, y)) (B x)) A"
proof -
from multipliableAB have a: ‹(f has_setprod infprod f (Sigma A B)) (Sigma A B)›
using has_setprod_infprod by blast
from multipliableB have b: ‹⋀x. x∈A ⟹ ((λy. f (x, y)) has_setprod infprod (λy. f (x, y)) (B x)) (B x)›
by (auto intro!: has_setprod_infprod)
show ?thesis
using a b by (auto intro: infprodI[symmetric] has_setprod_Sigma simp: multipliable_on_def)
qed
lemma infprod_Sigma':
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a ⇒ 'b ⇒ 'c::real_normed_field›
assumes multipliableAB: "(λ(x,y). f x y) multipliable_on (Sigma A B)"
assumes multipliableB: ‹⋀x. x∈A ⟹ (f x) multipliable_on (B x)›
shows ‹infprod (λx. infprod (f x) (B x)) A = infprod (λ(x,y). f x y) (Sigma A B)›
using infprod_Sigma[of ‹λ(x,y). f x y› A B]
using assms by auto
text ‹
These are the variants that do ∗‹not› assume multipliability of each fibre but derive it.
This needs more than multipliability of the whole family: it needs the
product to be non-zero (see ‹has_setprod_subset_nonzero› and the counterexample discussed
there). Note that a non-zero product also implies that no factor vanishes, so this replaces
-- rather than adds to -- the former pointwise non-vanishing hypothesis.
›
lemma
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a ⇒ 'b ⇒ 'c::{banach,real_normed_field}›
assumes [simp]: "(λ(x,y). f x y) multipliable_on (Sigma A B)"
assumes nz: ‹infprod (λ(x,y). f x y) (Sigma A B) ≠ 0›
shows infprod_Sigma'_banach: ‹infprod (λx. infprod (f x) (B x)) A = infprod (λ(x,y). f x y) (Sigma A B)› (is ?thesis1)
and multipliable_on_Sigma_banach: ‹(λx. infprod (f x) (B x)) multipliable_on A› (is ?thesis2)
proof -
have mult_B: ‹(f x) multipliable_on (B x)› if xA: ‹x ∈ A› for x
proof -
have inj: ‹inj_on snd (Sigma {x} B)›
by (auto intro!: inj_onI simp: Sigma_def)
have §: ‹snd ` Sigma {x} B = B x›
by (force simp: Sigma_def)
have ‹(λ(x,y). f x y) multipliable_on Sigma {x} B›
proof (rule multipliable_on_subset_nonzero[OF _ nz])
show ‹Sigma {x} B ⊆ Sigma A B› using xA by auto
qed auto
then have ‹(λy. f x y) ∘ snd multipliable_on Sigma {x} B›
using multipliable_on_cong[of ‹Sigma {x} B› ‹λ(a,b). f a b› ‹(λy. f x y) ∘ snd›]
by auto
then have ‹(λy. f x y) multipliable_on snd ` Sigma {x} B›
using multipliable_on_reindex[OF inj, of ‹λy. f x y›] by simp
with § show ?thesis by simp
qed
then show ?thesis1
using infprod_Sigma' assms by blast
show ?thesis2
unfolding multipliable_on_def
proof -
have ‹(λ(x,y). f x y) multipliable_on (Sigma A B)› by simp
then have ab: ‹((λ(x,y). f x y) has_setprod infprod (λ(x,y). f x y) (Sigma A B)) (Sigma A B)›
by (rule has_setprod_infprod)
have bx: ‹(f x has_setprod infprod (f x) (B x)) (B x)› if ‹x ∈ A› for x
using mult_B[OF that] has_setprod_infprod by auto
have bx': ‹((λy. (case (x,y) of (a,b) ⇒ f a b)) has_setprod infprod (f x) (B x)) (B x)› if ‹x ∈ A› for x
using bx[OF that] by simp
from has_setprod_Sigma[OF ab bx']
show ‹∃a. ((λx. infprod (f x) (B x)) has_setprod a) A›
by blast
qed
qed
lemma infprod_Sigma_banach:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a × 'b ⇒ 'c::{banach,real_normed_field}›
assumes [simp]: "f multipliable_on (Sigma A B)"
assumes ‹infprod f (Sigma A B) ≠ 0›
shows ‹infprod (λx. infprod (λy. f (x,y)) (B x)) A = infprod f (Sigma A B)›
using assms
by (simp add: infprod_Sigma'_banach)
lemma infprod_swap:
fixes A :: "'a set" and B :: "'b set"
fixes f :: "'a ⇒ 'b ⇒ 'c::real_normed_field"
assumes ‹(λ(x, y). f x y) multipliable_on (A × B)›
assumes ‹⋀a. a∈A ⟹ (f a) multipliable_on B›
assumes ‹⋀b. b∈B ⟹ (λa. f a b) multipliable_on A›
shows ‹infprod (λx. infprod (λy. f x y) B) A = infprod (λy. infprod (λx. f x y) A) B›
proof -
have "(λ(x, y). f y x) ∘ prod.swap multipliable_on A × B"
by (simp add: assms(1) multipliable_on_cong)
then have fyx: ‹(λ(x, y). f y x) multipliable_on (B × A)›
by (metis has_setprod_reindex infprod_reindex inj_swap product_swap multipliable_iff_has_setprod_infprod)
have ‹infprod (λx. infprod (λy. f x y) B) A = infprod (λ(x,y). f x y) (A × B)›
using infprod_Sigma' assms by blast
also have ‹… = infprod (λ(x,y). f y x) (B × A)›
by (simp add: product_swap [symmetric, of B] infprod_reindex o_def)
also have ‹… = infprod (λy. infprod (λx. f x y) A) B›
using assms(3) fyx infprod_Sigma by force
finally show ?thesis .
qed
lemma infprod_swap_banach:
fixes A :: "'a set" and B :: "'b set"
fixes f :: "'a ⇒ 'b ⇒ 'c::{banach,real_normed_field}"
assumes mult: ‹(λ(x, y). f x y) multipliable_on (A × B)›
assumes nz: ‹infprod (λ(x, y). f x y) (A × B) ≠ 0›
shows "infprod (λx. infprod (λy. f x y) B) A = infprod (λy. infprod (λx. f x y) A) B"
proof -
have §: ‹(λ(x, y). f y x) multipliable_on (B × A)›
by (metis (mono_tags, lifting) mult case_swap inj_swap o_apply product_swap multipliable_on_cong multipliable_on_reindex)
have swap: ‹infprod (λ(x,y). f y x) (B × A) = infprod (λ(x,y). f x y) (A × B)›
apply (subst product_swap[symmetric])
apply (subst infprod_reindex)
using mult by (auto simp: o_def)
have ‹infprod (λx. infprod (λy. f x y) B) A = infprod (λ(x,y). f x y) (A × B)›
using mult nz infprod_Sigma'_banach by blast
also have ‹… = infprod (λ(x,y). f y x) (B × A)›
by (simp add: swap)
also have ‹… = infprod (λy. infprod (λx. f x y) A) B›
using § nz swap by (intro infprod_Sigma'_banach [symmetric]) auto
finally show ?thesis .
qed
lemma has_setprod_constant[simp]:
assumes ‹finite F›
shows ‹((λ_. c) has_setprod c ^ card F) F›
by (metis assms has_setprod_finite prod_constant)
lemma infprod_constant[simp]:
assumes ‹finite F›
shows ‹infprod (λ_. c) F = c ^ card F›
by (simp add: assms)
lemma has_setprod_power:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "(f has_setprod P) A"
shows "((λx. f x ^ n) has_setprod (P ^ n)) A"
using assms by (induction n) (auto intro!: has_setprod_mult)
lemma multipliable_on_power:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A"
shows "(λx. f x ^ n) multipliable_on A"
using assms by (induction n) (auto intro!: multipliable_on_mult)
lemma infprod_power:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A"
shows ‹infprod (λx. f x ^ n) A = infprod f A ^ n›
using assms by (simp add: has_setprod_power infprodI)
lemma has_setprod_inverse:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "(f has_setprod (inverse a)) A" and "a ≠ 0"
shows ‹((λx. inverse (f x)) has_setprod a) A›
proof (rule has_setprodI)
have ‹((λX. inverse (prod f X)) ⤏ inverse (inverse a)) (finite_subsets_at_top A)›
using assms has_setprodD tendsto_inverse by fastforce
also have ‹inverse (inverse a) = a› using assms(2) by simp
finally show ‹((λX. prod (λx. inverse (f x)) X) ⤏ a) (finite_subsets_at_top A)›
by (simp add: prod_inversef[symmetric] o_def)
qed
lemma has_setprod_inverse_iff:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "a ≠ 0"
shows ‹((λx. inverse (f x)) has_setprod a) A ⟷ (f has_setprod (inverse a)) A›
proof
assume h: ‹((λx. inverse (f x)) has_setprod a) A›
have ‹a = inverse (inverse a)› using assms by simp
with h have ‹((λx. inverse (f x)) has_setprod (inverse (inverse a))) A› by simp
from has_setprod_inverse[OF this] assms show ‹(f has_setprod (inverse a)) A›
by (simp add: inverse_inverse_eq)
next
assume ‹(f has_setprod (inverse a)) A›
from has_setprod_inverse[OF this] assms show ‹((λx. inverse (f x)) has_setprod a) A› by simp
qed
lemma multipliable_on_inverse:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A" and "infprod f A ≠ 0"
shows "(λx. inverse (f x)) multipliable_on A"
proof -
from assms(1) have ‹(f has_setprod (infprod f A)) A›
by (rule has_setprod_infprod)
moreover have ‹infprod f A = inverse (inverse (infprod f A))›
using assms(2) by simp
ultimately have ‹(f has_setprod (inverse (inverse (infprod f A)))) A›
by simp
from has_setprod_inverse[OF this] assms(2)
show ?thesis
unfolding multipliable_on_def by auto
qed
lemma infprod_inverse:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes ‹f multipliable_on A› and ‹infprod f A ≠ 0›
shows ‹infprod (λx. inverse (f x)) A = inverse (infprod f A)›
proof -
have ‹(f has_setprod (infprod f A)) A›
using assms(1) by (rule has_setprod_infprod)
moreover have ‹infprod f A = inverse (inverse (infprod f A))›
using assms(2) by simp
ultimately have ‹(f has_setprod (inverse (inverse (infprod f A)))) A›
by simp
from has_setprod_inverse[OF this] assms(2)
show ?thesis
by (simp add: infprodI)
qed
text ‹
Quotients. ‹has_setprod_mult› and ‹has_setprod_inverse› are here already; this is the
combination one actually writes.
›
lemma has_setprod_divide:
fixes f g :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes f: "(f has_setprod a) A" and g: "(g has_setprod b) A" and b: "b ≠ 0"
shows "((λx. f x / g x) has_setprod (a / b)) A"
by (simp add: b divide_inverse f g has_setprod_inverse has_setprod_mult)
lemma multipliable_on_divide:
fixes f g :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A" "g multipliable_on A" "infprod g A ≠ 0"
shows "(λx. f x / g x) multipliable_on A"
using assms has_setprod_divide has_setprod_infprod multipliable_on_def by blast
lemma infprod_divide:
fixes f g :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A" "g multipliable_on A" "infprod g A ≠ 0"
shows "infprod (λx. f x / g x) A = infprod f A / infprod g A"
by (simp add: assms has_setprod_divide infprodI)
lemma multipliable_on_inverse_iff:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
shows ‹(f multipliable_on A ∧ infprod f A ≠ 0) ⟷
((λx. inverse (f x)) multipliable_on A ∧ infprod (λx. inverse (f x)) A ≠ 0)›
proof (intro iffI conjI)
assume asm: ‹f multipliable_on A ∧ infprod f A ≠ 0›
then show ‹(λx. inverse (f x)) multipliable_on A›
by (intro multipliable_on_inverse) auto
from asm show ‹infprod (λx. inverse (f x)) A ≠ 0›
by (simp add: infprod_inverse)
next
assume asm: ‹(λx. inverse (f x)) multipliable_on A ∧ infprod (λx. inverse (f x)) A ≠ 0›
then have mult_inv: ‹(λx. inverse (f x)) multipliable_on A› and
nz_inv: ‹infprod (λx. inverse (f x)) A ≠ 0› by auto
from multipliable_on_inverse[OF mult_inv nz_inv]
have inv_mult: ‹(λx. inverse (inverse (f x))) multipliable_on A› .
then show ‹f multipliable_on A›
using multipliable_on_cong[of A ‹λx. inverse (inverse (f x))› f] by auto
from infprod_inverse[OF mult_inv nz_inv]
have ‹infprod (λx. inverse (inverse (f x))) A = inverse (infprod (λx. inverse (f x)) A)› .
moreover have ‹infprod (λx. inverse (inverse (f x))) A = infprod f A›
by (intro infprod_cong) auto
ultimately show ‹infprod f A ≠ 0›
using nz_inv by simp
qed
lemma has_setprod_power_int:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "(f has_setprod P) A" and "P ≠ 0"
shows "((λx. f x powi n) has_setprod (P powi n)) A"
proof (cases ‹n ≥ 0›)
case True
then show ?thesis
using assms(1) by (auto simp: power_int_def intro!: has_setprod_power)
next
case False
then have ‹P ^ nat (- n) ≠ 0› using assms(2) by auto
with False show ?thesis
using assms(1) by (auto simp: power_int_def power_inverse intro!: has_setprod_power has_setprod_inverse)
qed
lemma multipliable_on_power_int:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A" and "infprod f A ≠ 0"
shows "(λx. f x powi n) multipliable_on A"
using assms has_setprod_power_int infprodI multipliable_on_def by blast
lemma infprod_power_int:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f multipliable_on A" and "infprod f A ≠ 0"
shows ‹infprod (λx. f x powi n) A = infprod f A powi n›
using assms has_setprod_infprod has_setprod_power_int infprodI by blast
lemma has_sum_imp_has_setprod_exp:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "(f has_sum S) A"
shows "((λx. exp (f x)) has_setprod exp S) A"
proof (rule has_setprodI)
have "((λX. exp (sum f X)) ⤏ exp S) (finite_subsets_at_top A)"
using assms by (intro tendsto_exp) (auto simp: has_sum_def)
also have "?this ⟷ ((λX. (∏x∈X. exp (f x))) ⤏ exp S) (finite_subsets_at_top A)"
by (intro filterlim_cong refl eventually_finite_subsets_at_top_weakI) (auto simp: exp_sum)
finally show "((λX. (∏x∈X. exp (f x))) ⤏ exp S) (finite_subsets_at_top A)" .
qed
lemma multipliable_on_exp:
fixes f :: ‹'a ⇒ 'b::{banach,real_normed_field}›
assumes "f summable_on A"
shows "(λx. exp (f x)) multipliable_on A"
using assms has_sum_imp_has_setprod_exp multipliable_on_def summable_on_def by blast
lemma has_setprod_reindex_bij_betw:
assumes "bij_betw g A B"
shows "((λx. f (g x)) has_setprod S) A = (f has_setprod S) B"
proof -
have "((λx. f (g x)) has_setprod S) A ⟷ (f has_setprod S) (g ` A)"
by (subst has_setprod_reindex) (use assms in ‹auto dest: bij_betw_imp_inj_on simp: o_def›)
then show ?thesis
using assms bij_betw_imp_surj_on by blast
qed
lemma has_setprod_reindex_bij_witness:
assumes "⋀a. a ∈ S ⟹ i (j a) = a"
assumes "⋀a. a ∈ S ⟹ j a ∈ T"
assumes "⋀b. b ∈ T ⟹ j (i b) = b"
assumes "⋀b. b ∈ T ⟹ i b ∈ S"
assumes "⋀a. a ∈ S ⟹ h (j a) = g a"
assumes "s = s'"
shows "(g has_setprod s) S = (h has_setprod s') T"
by (smt (verit, del_insts) assms bij_betwI' has_setprod_cong has_setprod_reindex_bij_betw)
lemma has_setprod_homomorphism:
assumes "(f has_setprod S) A" "h 1 = 1" "⋀a b. h (a * b) = h a * h b" "continuous_on UNIV h"
shows "((λx. h (f x)) has_setprod (h S)) A"
proof -
have "prod (h ∘ f) X = h (prod f X)" for X
by (induction X rule: infinite_finite_induct) (simp_all add: assms)
hence prod_h: "prod (h ∘ f) = h ∘ prod f"
by (intro ext) auto
have "((λx. h (prod f x)) ⤏ h S) (finite_subsets_at_top A)"
by (rule continuous_on_tendsto_compose[OF assms(4) has_setprodD[OF assms(1)]]) auto
hence "((h ∘ f) has_setprod h S) A"
unfolding has_setprod_def prod_h unfolding o_def by simp
thus ?thesis
by (simp add: o_def)
qed
lemma multipliable_on_homomorphism:
assumes "f multipliable_on A" "h 1 = 1" "⋀a b. h (a * b) = h a * h b" "continuous_on UNIV h"
shows "(λx. h (f x)) multipliable_on A"
using assms has_setprod_homomorphism has_setprod_imp_multipliable has_setprod_infprod
by blast
lemma infprod_homomorphism_strong:
fixes h :: "'a :: {t2_space, topological_comm_monoid_mult, semidom} ⇒
'b :: {t2_space, topological_comm_monoid_mult, semidom}"
assumes "(λx. h (f x)) multipliable_on A ⟷ f multipliable_on A"
assumes "h 1 = 1"
assumes "⋀S. (f has_setprod S) A ⟹ ((λx. h (f x)) has_setprod (h S)) A"
shows "infprod (λx. h (f x)) A = h (infprod f A)"
by (metis assms has_setprod_infprod infprodI infprod_not_exists)
lemma has_setprod_of_nat: "(f has_setprod S) A ⟹ ((λx. of_nat (f x)) has_setprod of_nat S) A"
by (erule has_setprod_homomorphism) (auto intro!: continuous_intros)
lemma has_setprod_of_int: "(f has_setprod S) A ⟹ ((λx. of_int (f x)) has_setprod of_int S) A"
by (erule has_setprod_homomorphism) (auto intro!: continuous_intros)
lemma multipliable_on_of_nat: "f multipliable_on A ⟹ (λx. of_nat (f x)) multipliable_on A"
by (erule multipliable_on_homomorphism) (auto intro!: continuous_intros)
lemma multipliable_on_of_int: "f multipliable_on A ⟹ (λx. of_int (f x)) multipliable_on A"
by (erule multipliable_on_homomorphism) (auto intro!: continuous_intros)
text ‹The same for the embedding of the reals, which is how a real product becomes a complex one.›
lemma has_setprod_of_real:
"(f has_setprod S) A ⟹
((λx. of_real (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult})
has_setprod of_real S) A"
by (erule has_setprod_homomorphism) (auto intro!: continuous_intros)
lemma multipliable_on_of_real:
"f multipliable_on A ⟹
(λx. of_real (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult})
multipliable_on A"
by (erule multipliable_on_homomorphism) (auto intro!: continuous_intros)
lemma infprod_of_real:
assumes "f multipliable_on A"
shows "infprod (λx. of_real (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult}) A
= of_real (infprod f A)"
using has_setprod_of_real[OF has_setprod_infprod[OF assms]] by (rule infprodI)
lemma multipliable_on_discrete_iff:
fixes f :: "'a ⇒ 'b :: {ring_1_no_zero_divisors, discrete_topology, topological_comm_monoid_mult, semidom}"
shows "f multipliable_on A ⟷ (∃x∈A. f x = 0) ∨ finite {x∈A. f x ≠ 1}"
proof
assume ‹(∃x∈A. f x = 0) ∨ finite {x∈A. f x ≠ 1}›
then show ‹f multipliable_on A›
proof
assume ‹∃x∈A. f x = 0›
then obtain x where ‹x ∈ A› ‹f x = 0› by auto
with zero_imp_has_setprod_0
show ‹f multipliable_on A› unfolding multipliable_on_def by metis
next
assume *: ‹finite {x∈A. f x ≠ 1}›
hence ‹f multipliable_on {x∈A. f x ≠ 1}›
by (rule multipliable_on_finite)
then show ‹f multipliable_on A›
by (smt (verit) DiffE mem_Collect_eq multipliable_on_cong_neutral)
qed
next
assume ‹f multipliable_on A›
then obtain S where S: ‹(f has_setprod S) A›
by (auto simp: multipliable_on_def)
hence ‹∀⇩F x in finite_subsets_at_top A. prod f x = S›
unfolding has_setprod_def tendsto_discrete .
then obtain X where X: ‹finite X› ‹X ⊆ A› ‹⋀Y. finite Y ⟹ X ⊆ Y ⟹ Y ⊆ A ⟹ prod f Y = S›
unfolding eventually_finite_subsets_at_top by metis
have prodX: ‹prod f X = S› using X by auto
show ‹(∃x∈A. f x = 0) ∨ finite {x∈A. f x ≠ 1}›
proof (cases ‹S = 0›)
case True
then have ‹prod f X = 0› using prodX by simp
then obtain x where ‹x ∈ X› ‹f x = 0›
using X(1) by (metis prod_zero_iff)
with X(2) show ?thesis by auto
next
case False
have ‹{x∈A. f x ≠ 1} ⊆ X›
proof
fix x assume x: ‹x ∈ {x∈A. f x ≠ 1}›
show ‹x ∈ X›
proof (rule ccontr)
assume [simp]: ‹x ∉ X›
have ‹prod f (insert x X) = S›
using X x by (intro X) auto
with False X(1) prodX x show False by auto
qed
qed
thus ?thesis using X(1) finite_subset by blast
qed
qed
lemma has_setprod_imp_has_prod:
fixes f :: ‹nat ⇒ 'a::real_normed_field›
assumes ‹(f has_setprod S) (UNIV :: nat set)› and ‹convergent_prod f›
shows ‹f has_prod S›
proof -
have ‹(λn. prod f {..n}) ⇢ S›
using filterlim_atMost_at_top filterlim_compose assms(1) has_setprodD by blast
then have ‹S = prodinf f›
using LIMSEQ_unique assms(2) convergent_prod_LIMSEQ by blast
with assms(2) show ‹f has_prod S›
using convergent_prod_has_prod by blast
qed
lemma multipliable_on_imp_convergent_prod:
fixes f :: ‹nat ⇒ 'a::real_normed_field›
assumes ‹f multipliable_on (UNIV :: nat set)› and ‹infprod f UNIV ≠ 0›
shows ‹convergent_prod f›
proof -
define S where ‹S = infprod f UNIV›
from assms(1) have ‹(f has_setprod S) UNIV›
unfolding S_def by (rule has_setprod_infprod)
then have lim: ‹(prod f ⤏ S) (finite_subsets_at_top UNIV)›
by (simp add: has_setprod_def)
then have seq_lim: ‹(λn. prod f {..n}) ⇢ S›
using filterlim_atMost_at_top filterlim_compose by blast
from seq_lim assms(2)[folded S_def] have ‹∀⇩F n in sequentially. prod f {..n} ≠ 0›
by (intro tendsto_imp_eventually_ne) auto
then obtain N where N: ‹⋀n. n ≥ N ⟹ prod f {..n} ≠ 0›
by (auto simp: eventually_at_top_linorder)
have fnz: ‹f n ≠ 0› if ‹n > N› for n
using N[of n] N[of ‹n - 1›] that by auto
have ‹convergent_prod (λi. f (i + Suc N))›
proof -
have lim: ‹(λn. ∏i≤n. f (i + Suc N)) ⇢ S / prod f {..N}›
proof -
have ‹(λn. prod f {..n + Suc N}) ⇢ S›
using seq_lim LIMSEQ_ignore_initial_segment
by blast
moreover have ‹prod f {..n + Suc N} = prod f {..N} * prod (λi. f (i + Suc N)) {..n}› for n
proof -
have ‹{..n + Suc N} = {..N} ∪ {Suc N..n + Suc N}› by auto
also have ‹prod f … = prod f {..N} * prod f {Suc N..n + Suc N}›
by (subst prod.union_disjoint) auto
also have ‹prod f {Suc N..n + Suc N} = prod (λi. f (i + Suc N)) {..n}›
by (metis (no_types) add_0 atMost_atLeast0 prod.shift_bounds_cl_nat_ivl)
finally show ?thesis .
qed
ultimately have ‹(λn. prod f {..N} * prod (λi. f (i + Suc N)) {..n}) ⇢ S›
by (simp add: tendsto_cong)
then have ‹(λn. prod f {..N} * prod (λi. f (i + Suc N)) {..n} / prod f {..N}) ⇢ S / prod f {..N}›
using N[of N] by (intro tendsto_divide tendsto_const) auto
then show ?thesis
using N[of N] by (simp add: field_simps)
qed
moreover have ‹S / prod f {..N} ≠ 0›
using assms(2)[folded S_def] N[of N, simplified] by auto
ultimately have ‹raw_has_prod (λi. f (i + Suc N)) 0 (S / prod f {..N})›
by (simp add: raw_has_prod_def)
then show ?thesis
unfolding convergent_prod_def by blast
qed
then show ‹convergent_prod f›
by (rule convergent_prod_offset)
qed
lemma has_prod_imp_sums_ln_real:
fixes f :: "'a ⇒ real"
assumes "(f has_setprod p) A" "p ≠ 0"
shows "((λx. ln (f x)) has_sum (ln p)) A"
proof -
have nz: "f x ≠ 0" if "x ∈ A" for x
using assms that by (metis infprodI zero_imp_has_setprod_0)
have "((λX. ln (prod f X)) ⤏ ln p) (finite_subsets_at_top A)"
proof (rule tendsto_ln)
show "(prod f ⤏ p) (finite_subsets_at_top A)"
using assms(1) unfolding has_setprod_def by blast
qed (use assms in auto)
also have "?this ⟷ (sum (λx. ln (f x)) ⤏ ln p) (finite_subsets_at_top A)"
proof (intro filterlim_cong)
have "∀⇩F X in finite_subsets_at_top A. X ⊆ A ∧ finite X"
by (rule eventually_finite_subsets_at_top_weakI) auto
thus "∀⇩F x in finite_subsets_at_top A. ln (prod f x) = (∑x∈x. ln (f x))"
by eventually_elim (subst ln_prod, use nz in auto)
qed auto
finally show ?thesis
unfolding has_sum_def .
qed
subsection ‹Strong multipliability›
text ‹
A finite family is strongly multipliable, with no side condition: the set of vanishing factors is
trivially finite, and a finite product of non-zero elements of a semidom is non-zero. Compare
‹multipliable_on_finite› and ‹abs_multipliable_on_finite›.
›
lemma strongly_multipliable_on_finite [simp]:
assumes "finite A"
shows "f strongly_multipliable_on A"
proof -
have "finite {x ∈ A. f x ≠ 0}"
using assms by simp
hence "(f has_setprod prod f {x ∈ A. f x ≠ 0}) {x ∈ A. f x ≠ 0}"
by (rule has_setprod_finite)
moreover have "prod f {x ∈ A. f x ≠ 0} ≠ 0"
using assms by (subst prod_zero_iff) auto
ultimately show ?thesis
unfolding strongly_multipliable_on_def using assms by auto
qed
lemma strongly_multipliable_imp_multipliable:
assumes "f strongly_multipliable_on A"
shows "f multipliable_on A"
proof -
from assms obtain P where P: "finite {x∈A. f x = 0}" "(f has_setprod P) {x∈A. f x ≠ 0}"
by (auto simp: strongly_multipliable_on_def)
have "(f has_setprod (P * prod f {x∈A. f x = 0})) ({x∈A. f x ≠ 0} ∪ {x∈A. f x = 0})"
by (intro has_setprod_Un_disjoint P has_setprod_finite) auto
also have "{x∈A. f x ≠ 0} ∪ {x∈A. f x = 0} = A"
by auto
finally show ?thesis
by (rule has_setprod_imp_multipliable)
qed
text ‹
For a non-zero family, strong multipliability is equivalent to the product being non-zero.
›
lemma strongly_multipliable_on_nonzero_iff:
assumes "⋀x. x ∈ A ⟹ f x ≠ 0"
shows "f strongly_multipliable_on A ⟷ (∃P. (f has_setprod P) A ∧ P ≠ 0)"
proof
assume *: "(∃P. (f has_setprod P) A ∧ P ≠ 0)"
from assms have [simp]: "{x∈A. f x = 0} = {}" "{x∈A. f x ≠ 0} = A"
by auto
from * obtain P where P: "(f has_setprod P) A" "P ≠ 0"
by blast
thus "f strongly_multipliable_on A"
by (auto simp: strongly_multipliable_on_def assms)
next
assume "f strongly_multipliable_on A"
then obtain P where "(f has_setprod P) {x∈A. f x ≠ 0} ∧ P ≠ 0"
by (auto simp: strongly_multipliable_on_def)
also have "{x∈A. f x ≠ 0} = A"
using assms by auto
finally show "∃P. (f has_setprod P) A ∧ P ≠ 0"
by blast
qed
text ‹
When the product is ∗‹strongly› multipliable its value vanishes only for the obvious reason. Some
hypothesis of that kind is needed: over an infinite index set \<^term>‹λ_. 1/2 :: real› is
multipliable with value ‹0› and no vanishing factor.
›
lemma has_setprod_eq_0_iff:
assumes "f strongly_multipliable_on A" and P: "(f has_setprod P) A"
shows "P = 0 ⟷ (∃x∈A. f x = 0)"
proof
assume "∃x∈A. f x = 0"
then obtain x where "x ∈ A" "f x = 0"
by blast
hence "(f has_setprod 0) A"
by (rule zero_imp_has_setprod_0)
with P show "P = 0"
by (rule has_setprod_unique)
next
assume P0: "P = 0"
show "∃x∈A. f x = 0"
proof (rule ccontr)
assume "¬ (∃x∈A. f x = 0)"
hence nz: "⋀x. x ∈ A ⟹ f x ≠ 0"
by blast
then obtain Q where "(f has_setprod Q) A" "Q ≠ 0"
using assms(1) by (meson strongly_multipliable_on_nonzero_iff)
with has_setprod_unique[OF P] P0 show False
by simp
qed
qed
corollary infprod_eq_0_iff:
assumes "f strongly_multipliable_on A"
shows "infprod f A = 0 ⟷ (∃x∈A. f x = 0)"
using assms by (metis infprodI strongly_multipliable_on_nonzero_iff zero_imp_has_setprod_0)
lemma strongly_multipliable_on_Diff_finite:
fixes f :: "_ ⇒ 'a :: real_normed_field"
assumes "f strongly_multipliable_on A" "finite B"
shows "f strongly_multipliable_on (A - B)"
proof -
from assms(1) obtain P where P: "finite {x∈A. f x = 0}" "(f has_setprod P) {x∈A. f x ≠ 0}" "P ≠ 0"
by (auto simp: strongly_multipliable_on_def)
define Q where "Q = prod f {x∈B∩A. f x ≠ 0}"
have Q: "(f has_setprod Q) {x∈B∩A. f x ≠ 0}"
unfolding Q_def by (intro has_setprod_finite) (use assms(2) in auto)
have [simp]: "Q ≠ 0"
using assms(2) by (auto simp: Q_def)
have "(f has_setprod (P / Q)) ({x∈A. f x ≠ 0} - {x∈B∩A. f x ≠ 0})"
by (intro has_setprod_Diff P Q) auto
also have "{x∈A. f x ≠ 0} - {x∈B∩A. f x ≠ 0} = {x∈A-B. f x ≠ 0}"
by blast
finally have "(f has_setprod P / Q) {x∈A-B. f x ≠ 0}" .
moreover have "finite {x∈A-B. f x = 0}"
by (rule finite_subset[OF _ P(1)]) auto
moreover have "P / Q ≠ 0"
using P(3) by auto
ultimately show ?thesis
unfolding strongly_multipliable_on_def by blast
qed
subsection ‹Absolute convergence›
lemma has_setprod_factors_tend_to_1:
fixes f :: "'a ⇒ 'b :: {real_normed_div_algebra,comm_monoid_mult}"
assumes lim: "(prod f ⤏ L) (finite_subsets_at_top M)" and nz: "L ≠ 0" and "ε>0"
shows "∃F. finite F ∧ F ⊆ M ∧ (∀x∈M - F. dist (f x) 1 < ε)"
proof -
obtain F where F: "finite F" "F ⊆ M"
and near: "⋀D. finite D ⟹ D ⊆ M - F ⟹ dist (prod f D) 1 < ε"
using has_setprod_prods_near_1[OF lim nz ‹ε>0›] by blast
have "dist (f x) 1 < ε" if "x ∈ M - F" for x
using near[of "{x}"] that by simp
with F show "∃F. finite F ∧ F ⊆ M ∧ (∀x∈M - F. dist (f x) 1 < ε)"
by blast
qed
lemma has_setprod_factors_tend_to_1':
fixes f :: "'a ⇒ 'b :: {real_normed_div_algebra, comm_monoid_mult}"
assumes lim: "(prod f ⤏ L) (finite_subsets_at_top M)" and nz: "L ≠ 0"
assumes X: "open X" "1 ∈ X"
shows "∃F. finite F ∧ F ⊆ M ∧ (∀x∈M - F. f x ∈ X)"
proof -
from X obtain ε where "ε > 0" and ball_sub: "ball 1 ε ⊆ X"
using openE by blast
from has_setprod_factors_tend_to_1[OF lim nz ‹ε > 0›]
obtain F where "finite F" "F ⊆ M" "⋀x. x ∈ M - F ⟹ dist (f x) 1 < ε"
by blast
then show ?thesis
using ball_sub by (intro exI[of _ F]) (auto simp: ball_def dist_commute)
qed
text ‹
For a strongly multipliable family, all but finitely many values are close to 1.
›
lemma strongly_multipliable_on_imp_nhds_1:
fixes f :: "_ ⇒ 'a :: {real_normed_div_algebra,semidom}"
assumes "f strongly_multipliable_on A" "open X" "1 ∈ X"
shows "∃B. B ⊆ A ∧ finite B ∧ (∀x∈A-B. f x ∈ X)"
proof -
from assms(1) obtain P
where P: "finite {x∈A. f x = 0}" "(f has_setprod P) {x∈A. f x ≠ 0}" "P ≠ 0"
by (auto simp: strongly_multipliable_on_def)
have "∃F. finite F ∧ F ⊆ {x ∈ A. f x ≠ 0} ∧ (∀x∈{x ∈ A. f x ≠ 0} - F. f x ∈ X)"
by (rule has_setprod_factors_tend_to_1'[where L = P])
(use assms P in ‹auto simp: has_setprod_def›)
then obtain F where F: "finite F" "F ⊆ {x∈A. f x ≠ 0}" "∀x∈{x ∈ A. f x ≠ 0} - F. f x ∈ X"
by blast
define B where "B = F ∪ {x∈A. f x = 0}"
have "B ⊆ A" "finite B" "∀x∈A-B. f x ∈ X"
unfolding B_def using F P by auto
thus ?thesis
by blast
qed
text ‹
The equivalent for summable familes: In a summable family, all but finitely many elements are
close to 0.
›
lemma summable_on_imp_nhds_0:
fixes f :: "'a ⇒ 'b :: real_normed_field"
assumes lim: "f summable_on M"
assumes X: "open X" "0 ∈ X"
shows "∃F. finite F ∧ F ⊆ M ∧ (∀x∈M - F. f x ∈ X)"
proof -
from lim obtain S where S: "(f has_sum S) M"
unfolding summable_on_def by blast
hence tend: "((λU. sum f U) ⤏ S) (finite_subsets_at_top M)"
by (auto simp: has_sum_def)
have "continuous_on UNIV (λ(a::'b, b). a - b)"
by (auto intro!: continuous_intros simp: case_prod_unfold)
hence cont: "isCont (λ(a::'b, b). a - b) (S, S)"
by (simp add: continuous_on_eq_continuous_at)
from cont[unfolded isCont_def] have "((λ(a,b). a - b) ⤏ (0::'b)) (nhds (S, S))"
by (simp add: tendsto_nhds_iff)
from this[unfolded tendsto_def, rule_format, OF X(1) X(2)]
have "eventually (λ(a,b). a - b ∈ X) (nhds (S, S))"
by (simp add: case_prod_unfold)
hence "∀⇩F (a, b) in nhds S ×⇩F nhds S. a - b ∈ X"
by (simp add: nhds_prod[symmetric])
then obtain Q where Q_ev: "eventually Q (nhds S)" and Q_sub: "⋀a b. Q a ⟹ Q b ⟹ a - b ∈ X"
unfolding eventually_prod_same by auto
then obtain W where W: "open W" "S ∈ W" "W ⊆ Collect Q"
unfolding eventually_nhds by auto
have W_sub: "a - b ∈ X" if "a ∈ W" "b ∈ W" for a b
using Q_sub that W(3) by auto
from tend have "eventually (λU. sum f U ∈ W) (finite_subsets_at_top M)"
using topological_tendstoD W by blast
then obtain F where F: "finite F" "F ⊆ M"
"⋀U. finite U ⟹ F ⊆ U ⟹ U ⊆ M ⟹ sum f U ∈ W"
unfolding eventually_finite_subsets_at_top by metis
show ?thesis
proof (intro exI conjI ballI)
show "finite F" "F ⊆ M" by fact+
fix x assume "x ∈ M - F"
hence xM: "x ∈ M" and xF: "x ∉ F" by auto
have "sum f (insert x F) ∈ W"
by (intro F) (use F xM in auto)
moreover have "sum f F ∈ W"
by (intro F) (use F in auto)
ultimately have "sum f (insert x F) - sum f F ∈ X"
by (rule W_sub)
also have "sum f (insert x F) - sum f F = f x"
using F(1) xF by simp
finally show "f x ∈ X" .
qed
qed
lemma has_setprod_imp_has_prod_nonzero:
assumes ‹(f has_setprod S) (UNIV :: nat set)› and ‹S ≠ 0›
shows ‹f has_prod S›
proof -
from assms(1) have ‹(prod f ⤏ S) (finite_subsets_at_top UNIV)›
by (simp add: has_setprod_def)
then have ‹(λn. prod f {..n}) ⇢ S›
using filterlim_atMost_at_top filterlim_compose by blast
with ‹S ≠ 0› show ‹f has_prod S›
by (simp add: raw_has_prod_def has_prod_def)
qed
text ‹
Could the hypothesis \<^term>‹1 ≤ f x› could be replaced by strong multipliability
together with \<^term>‹0 ≤ f x›? It cannot: that statement is FALSE. Take
\<^term>‹A = (UNIV :: nat set)› and \<^term>‹f = (λk. 1 - 1 / 2 ^ (k + 2))›. Every factor is positive
and $\sum_k 2^{-(k+2)}$ converges, so this \<^term>‹f› is strongly multipliable with a positive
value $L$; but every factor is smaller than $1$, so $L < 3/4 = $ \<^term>‹prod f {0}› and the
inequality goes the wrong way. Factors below $1$ shrink the product, and monotonicity of the
partial products is precisely what the conclusion needs.
What can be weakened is where the hypothesis is required: only the factors OUTSIDE \<^term>‹F›
need to be at least $1$, those inside merely non-negative. That covers a product with finitely
many small factors, which is the case that occurs in practice.
›
lemma finite_prod_le_infprod:
fixes f :: "'a ⇒ real"
assumes "f multipliable_on A" "finite F" "F ⊆ A"
and ge1: "⋀x. x ∈ A - F ⟹ 1 ≤ f x" and nonneg: "⋀x. x ∈ F ⟹ 0 ≤ f x"
shows "prod f F ≤ infprod f A"
proof -
have tendsto: "(prod f ⤏ infprod f A) (finite_subsets_at_top A)"
using infprod_tendsto[OF assms(1)] .
have "Limsup (finite_subsets_at_top A) (prod f) = infprod f A"
using finite_subsets_at_top_neq_bot tendsto tendsto_iff_Liminf_eq_Limsup by blast
moreover have "prod f F ≤ Limsup (finite_subsets_at_top A) (prod f)"
proof (rule le_Limsup[OF finite_subsets_at_top_neq_bot])
show "∀⇩F X in finite_subsets_at_top A. ereal (prod f F) ≤ ereal (prod f X)"
unfolding eventually_finite_subsets_at_top
using assms ge1 nonneg by (smt (verit) Diff_iff ereal_less_eq(3) prod_mono2 subset_eq)
qed
ultimately show ?thesis by simp
qed
lemma abs_multipliable_on_iff_bdd_above:
shows ‹f abs_multipliable_on A ⟷ bdd_above (prod (λx. 1 + norm (f x - 1)) ` {F. F⊆A ∧ finite F})›
proof (rule iffI)
assume asm: ‹f abs_multipliable_on A›
then have mult: ‹(λx. 1 + norm (f x - 1)) multipliable_on A›
by (simp add: abs_multipliable_on_def)
show ‹bdd_above (prod (λx. 1 + norm (f x - 1)) ` {F. F ⊆ A ∧ finite F})›
proof (rule bdd_aboveI2)
fix F assume F: "F ∈ {F. F ⊆ A ∧ finite F}"
then have "finite F" "F ⊆ A" by auto
show "(∏x∈F. 1 + norm (f x - 1)) ≤ (∏⇩∞x∈A. 1 + norm (f x - 1))"
by (rule finite_prod_le_infprod[OF mult ‹finite F› ‹F ⊆ A›]) auto
qed
next
assume bdd: ‹bdd_above (prod (λx. 1 + norm (f x - 1)) ` {F. F⊆A ∧ finite F})›
show ‹f abs_multipliable_on A›
unfolding abs_multipliable_on_def
proof -
define g where ‹g x = 1 + norm (f x - 1)› for x
have g_ge1: ‹g x ≥ 1› for x unfolding g_def by auto
from bdd obtain C where C: ‹prod g F ≤ C› if ‹F ⊆ A› ‹finite F› for F
unfolding bdd_above_def g_def by auto
have g_ge0: ‹g x ≥ 0› for x using g_ge1[of x] by linarith
have mono: ‹prod g F ≤ prod g G› if ‹F ⊆ G› ‹G ⊆ A› ‹finite G› for F G
using that g_ge1 g_ge0 by (intro prod_mono2) auto
have ‹(prod g ⤏ (SUP F∈{F. F ⊆ A ∧ finite F}. prod g F)) (finite_subsets_at_top A)›
proof (rule order_tendstoI)
fix a :: real assume ‹a < (SUP F∈{F. F ⊆ A ∧ finite F}. prod g F)›
then obtain F where F: ‹F ⊆ A› ‹finite F› ‹a < prod g F›
using less_cSUP_iff[of ‹{F. F ⊆ A ∧ finite F}› ‹prod g› a]
bdd[unfolded g_def[abs_def]]
unfolding g_def by auto
show ‹∀⇩F X in finite_subsets_at_top A. a < prod g X›
unfolding eventually_finite_subsets_at_top
using F g_ge0 g_ge1 by (meson order_less_le_trans prod_mono2)
next
fix a :: real assume ‹(SUP F∈{F. F ⊆ A ∧ finite F}. prod g F) < a›
show ‹∀⇩F X in finite_subsets_at_top A. prod g X < a›
unfolding eventually_finite_subsets_at_top
proof (intro exI conjI allI impI)
fix Y assume ‹finite Y ∧ {} ⊆ Y ∧ Y ⊆ A›
then have ‹prod g Y ≤ (SUP F∈{F. F ⊆ A ∧ finite F}. prod g F)›
using bdd
by (intro cSUP_upper bdd[unfolded g_def[abs_def]]) (auto simp: g_def)
also have ‹… < a› by fact
finally show ‹prod g Y < a› .
qed auto
qed
then show ‹(λx. 1 + norm (f x - 1)) multipliable_on A›
unfolding g_def multipliable_on_def has_setprod_def by blast
qed
qed
lemma multipliable_on_comparison_test:
fixes f g :: "'b ⇒ real"
assumes "f multipliable_on A" and "⋀x. x ∈ A ⟹ g x ≤ f x" and "⋀x. x ∈ A ⟹ 1 ≤ g x"
shows "g multipliable_on A"
proof -
from assms(1) obtain S where S: "(prod f ⤏ S) (finite_subsets_at_top A)"
unfolding multipliable_on_def has_setprod_def by blast
have g_ge1: "1 ≤ g x" if "x ∈ A" for x
using assms(3)[OF that] .
have g_nonneg: "0 ≤ g x" if "x ∈ A" for x
using g_ge1[OF that] by (meson dual_order.trans zero_le_one)
have g_le_f_prod: "prod g X ≤ prod f X" if "X ⊆ A" "finite X" for X
proof (rule prod_mono)
fix i assume "i ∈ X"
with that have "i ∈ A" by auto
thus "0 ≤ g i ∧ g i ≤ f i"
using g_nonneg assms(2) by auto
qed
have g_mono: "prod g X ≤ prod g Y" if "X ⊆ Y" "Y ⊆ A" "finite Y" for X Y
proof (rule prod_mono2[OF ‹finite Y› ‹X ⊆ Y›])
fix b assume "b ∈ Y - X"
with that have "b ∈ A" by auto
thus "1 ≤ g b" using g_ge1 by auto
next
fix a assume "a ∈ X"
with that have "a ∈ A" by auto
thus "0 ≤ g a" using g_nonneg by auto
qed
have f_bound: "∃C. ∀⇩F X in finite_subsets_at_top A. prod f X ≤ C"
proof (cases "∃C. C > S")
case True
then obtain C where C: "C > S" by blast
have "∀⇩F X in finite_subsets_at_top A. prod f X < C"
using S C by (rule order_tendstoD)
thus ?thesis
by (meson eventually_mono nless_le)
next
case False thus ?thesis
by (meson not_eventuallyD not_le_imp_less)
qed
then obtain C where C: "∀⇩F X in finite_subsets_at_top A. prod f X ≤ C"
by blast
from C obtain X0 where X0: "finite X0" "X0 ⊆ A"
and X0_bound: "⋀X. finite X ⟹ X0 ⊆ X ⟹ X ⊆ A ⟹ prod f X ≤ C"
unfolding eventually_finite_subsets_at_top by auto
have g_bdd: "prod g X ≤ C" if "finite X" "X ⊆ A" for X
proof -
have "prod g X ≤ prod g (X ∪ X0)"
using that X0 by (intro g_mono) auto
also have "… ≤ prod f (X ∪ X0)"
using that X0 by (intro g_le_f_prod) auto
also have "… ≤ C"
using that X0 X0_bound[of "X ∪ X0"] by auto
finally show ?thesis .
qed
hence bdd: "bdd_above (prod g ` {X. X ⊆ A ∧ finite X})"
by (auto simp: bdd_above_def)
show ?thesis unfolding multipliable_on_def has_setprod_def
proof (rule exI, rule increasing_tendsto)
show "∀⇩F X in finite_subsets_at_top A. prod g X ≤ Sup (prod g ` {X. X ⊆ A ∧ finite X})"
by (intro eventually_finite_subsets_at_top_weakI cSUP_upper[OF _ bdd]) auto
next
fix y assume "y < Sup (prod g ` {X. X ⊆ A ∧ finite X})"
then obtain X where X: "X ⊆ A" "finite X" "y < prod g X"
by (subst (asm) less_cSUP_iff[OF _ bdd]) auto
from X have "eventually (λX'. X ⊆ X' ∧ X' ⊆ A ∧ finite X') (finite_subsets_at_top A)"
by (auto simp: eventually_finite_subsets_at_top)
thus "eventually (λX'. y < prod g X') (finite_subsets_at_top A)"
using X(3) g_mono by (smt (verit) eventually_mono)
qed
qed
lemma multipliable_on_imp_bdd_above_prods:
fixes f :: "_ ⇒ 'a :: {topological_semigroup_mult, linorder_topology, semidom, t2_space}"
assumes f: "f multipliable_on A"
shows "∃C. eventually (λX. prod f X ≤ C) (finite_subsets_at_top A)"
proof -
from assms obtain S where S: "(prod f ⤏ S) (finite_subsets_at_top A)"
unfolding multipliable_on_def has_setprod_def by blast
show ?thesis
proof (cases "∃C. C > S")
case True
then obtain C where C: "C > S"
by blast
have "∀⇩F X in finite_subsets_at_top A. prod f X < C"
using S C by (rule order_tendstoD(2))
thus ?thesis
by (meson eventually_mono nless_le)
next
case False thus ?thesis
by (meson not_eventuallyD not_le_imp_less)
qed
qed
context
assumes "SORT_CONSTRAINT('a :: {topological_semigroup_mult, order_topology,
conditionally_complete_linorder, linordered_idom, t2_space})"
begin
text ‹
Any family of non-negative numbers with bounded partial sums is multipliable, and the sum
is simply the supremum of the partial sums.
›
lemma ge_1_bdd_above_prods_imp_has_setprod_SUP:
assumes nonneg: "⋀x. x ∈ A ⟹ f x ≥ (1::'a)"
and bound: "eventually (λX. prod f X ≤ C) (finite_subsets_at_top A)"
shows "(f has_setprod (SUP X∈{X. X ⊆ A ∧ finite X}. prod f X)) A"
proof -
from bound obtain X0
where X0: "X0 ⊆ A" "finite X0" "⋀X. X0 ⊆ X ⟹ X ⊆ A ⟹ finite X ⟹ prod f X ≤ C"
by (force simp: eventually_finite_subsets_at_top)
have bound': "prod f X ≤ C" if "X ⊆ A" "finite X" for X
proof -
have "prod f X ≤ prod f (X ∪ X0)"
using that X0 assms(1) ‹finite X0›
by (smt (verit, best) DiffE dual_order.trans finite_Un nle_le not_one_le_zero prod_mono2 subset_eq sup.bounded_iff)
also have "… ≤ C"
by (simp add: X0 that)
finally show ?thesis .
qed
hence bdd: "bdd_above (prod f ` {X. X ⊆ A ∧ finite X})"
by (auto simp: bdd_above_def)
show ?thesis unfolding has_setprod_def
proof (rule increasing_tendsto)
show "∀⇩F X in finite_subsets_at_top A. prod f X ≤ Sup (prod f ` {X. X ⊆ A ∧ finite X})"
by (intro eventually_finite_subsets_at_top_weakI cSUP_upper[OF _ bdd]) auto
next
fix y assume "y < Sup (prod f ` {X. X ⊆ A ∧ finite X})"
then obtain X where X: "X ⊆ A" "finite X" "y < prod f X"
by (subst (asm) less_cSUP_iff[OF _ bdd]) auto
from X have "eventually (λX'. X ⊆ X' ∧ X' ⊆ A ∧ finite X') (finite_subsets_at_top A)"
by (auto simp: eventually_finite_subsets_at_top)
thus "eventually (λX'. y < prod f X') (finite_subsets_at_top A)"
proof eventually_elim
case (elim X')
note ‹y < prod f X›
also have "prod f X ≤ prod f X'"
by (smt (verit) Diff_iff dual_order.trans elim nonneg prod_mono2 subset_iff zero_le_one)
finally show ?case .
qed
qed
qed
lemma ge_1_bdd_above_prods_imp_multipliable_on:
assumes nonneg: "⋀x. x ∈ A ⟹ f x ≥ (1::'a)"
and bound: "eventually (λX. prod f X ≤ C) (finite_subsets_at_top A)"
shows "f multipliable_on A"
using ge_1_bdd_above_prods_imp_has_setprod_SUP[OF assms] by (auto simp: multipliable_on_def)
end
lemma abs_multipliable_on_iff_summable_on:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_algebra_1}"
shows "f abs_multipliable_on A ⟷ (λn. norm (f n - 1)) summable_on A"
proof
define g where ‹g n = norm (f n - 1)› for n
have g_nn: ‹g n ≥ 0› for n unfolding g_def by simp
assume ‹f abs_multipliable_on A›
then obtain L where lim: ‹((λF. ∏x∈F. 1 + g x) ⤏ L) (finite_subsets_at_top A)›
unfolding abs_multipliable_on_def multipliable_on_def has_setprod_def g_def by blast
show ‹(λn. norm (f n - 1)) summable_on A›
unfolding g_def[symmetric]
proof (rule nonneg_bounded_partial_sums_imp_summable_on)
show ‹⋀x. x ∈ A ⟹ 0 ≤ g x› using g_nn by simp
from lim have ‹∀⇩F X in finite_subsets_at_top A. dist (prod (λx. 1 + g x) X) L < 1›
unfolding tendsto_iff by auto
then have ‹∀⇩F X in finite_subsets_at_top A. prod (λx. 1 + g x) X < L + 1›
by (eventually_elim) (auto simp: dist_real_def)
then show ‹∀⇩F X in finite_subsets_at_top A. sum g X ≤ L + 1›
proof eventually_elim
case (elim X)
have ‹sum g X ≤ prod (λx. 1 + g x) X›
by (rule sum_le_prod) (use g_nn in auto)
also have ‹… < L + 1› by (rule elim)
finally show ?case by linarith
qed
qed
next
define g where ‹g n = norm (f n - 1)› for n
have g_nn: ‹g n ≥ 0› for n unfolding g_def by simp
assume ‹(λn. norm (f n - 1)) summable_on A›
then obtain L where lim: ‹(sum g ⤏ L) (finite_subsets_at_top A)›
unfolding summable_on_def has_sum_def g_def by blast
show ‹f abs_multipliable_on A›
unfolding abs_multipliable_on_def g_def[symmetric]
proof (rule ge_1_bdd_above_prods_imp_multipliable_on)
show ‹⋀x. x ∈ A ⟹ 1 ≤ (λx. 1 + g x) x› using g_nn by auto
from lim have ‹∀⇩F X in finite_subsets_at_top A. dist (sum g X) L < 1›
unfolding tendsto_iff by auto
then have sum_bound: ‹∀⇩F X in finite_subsets_at_top A. sum g X < L + 1›
by (eventually_elim) (auto simp: dist_real_def)
show ‹∀⇩F X in finite_subsets_at_top A. prod (λx. 1 + g x) X ≤ exp (L + 1)›
using sum_bound
proof eventually_elim
case (elim X)
have ‹prod (λx. 1 + g x) X ≤ exp (sum g X)›
by (rule prod_le_exp_sum) (use g_nn in auto)
also have ‹… ≤ exp (L + 1)›
using elim by simp
finally show ?case .
qed
qed
qed
text ‹
Absolute multipliability, unlike plain multipliability, does pass to arbitrary subsets without
further ado -- it is just absolute summability of \<^term>‹λx. norm (f x - 1)› in disguise.
›
lemma abs_multipliable_on_subset:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_algebra_1}"
assumes "f abs_multipliable_on A" and "B ⊆ A"
shows "f abs_multipliable_on B"
using assms unfolding abs_multipliable_on_iff_summable_on
by (rule summable_on_subset_banach)
lemma abs_multipliable_on_comparison_test:
fixes f :: ‹'a ⇒ 'b::{banach, real_normed_algebra_1}›
and g :: ‹'a ⇒ 'c::{banach, real_normed_algebra_1}›
assumes ‹g abs_multipliable_on A›
assumes ‹⋀x. x ∈ A ⟹ norm (f x - 1) ≤ norm (g x - 1)›
shows ‹f abs_multipliable_on A›
proof -
define gn where ‹gn x = norm (g x - 1)› for x
define fn where ‹fn x = norm (f x - 1)› for x
have gn_nn: ‹gn x ≥ 0› for x unfolding gn_def by simp
have fn_nn: ‹fn x ≥ 0› for x unfolding fn_def by simp
have fn_le_gn: ‹fn x ≤ gn x› if ‹x ∈ A› for x
unfolding fn_def gn_def using assms(2)[OF that] by simp
from assms(1) have k_mult: ‹(λx. 1 + gn x) multipliable_on A›
unfolding abs_multipliable_on_def gn_def by simp
from infprod_tendsto[OF k_mult]
have k_tendsto: ‹(prod (λx. 1 + gn x) ⤏ infprod (λx. 1 + gn x) A) (finite_subsets_at_top A)› .
from tendstoD[OF k_tendsto, of 1]
have ‹∀⇩F F in finite_subsets_at_top A. dist (prod (λx. 1 + gn x) F) (infprod (λx. 1 + gn x) A) < 1›
by simp
then have prod_bound: ‹∀⇩F F in finite_subsets_at_top A. prod (λx. 1 + gn x) F < infprod (λx. 1 + gn x) A + 1›
by (eventually_elim) (auto simp: dist_real_def)
have sum_bound: ‹∀⇩F F in finite_subsets_at_top A. sum gn F ≤ infprod (λx. 1 + gn x) A + 1›
using prod_bound
proof eventually_elim
case (elim F)
have ‹sum gn F ≤ prod (λx. 1 + gn x) F›
by (rule sum_le_prod) (use gn_nn in auto)
also have ‹… < infprod (λx. 1 + gn x) A + 1› by (rule elim)
finally show ?case by linarith
qed
have gn_summable: ‹gn summable_on A›
by (rule nonneg_bounded_partial_sums_imp_summable_on) (use gn_nn sum_bound in auto)
have fn_bound: ‹∃C. ∀⇩F F in finite_subsets_at_top A. sum fn F ≤ C›
proof -
from summable_on_imp_bounded_partial_sums[OF gn_summable]
obtain C where C: ‹∀⇩F F in finite_subsets_at_top A. sum gn F ≤ C› by auto
have FA: ‹∀⇩F F in finite_subsets_at_top A. F ⊆ A›
by (auto simp: eventually_finite_subsets_at_top)
from C FA have ‹∀⇩F F in finite_subsets_at_top A. sum fn F ≤ C›
proof eventually_elim
case (elim F)
have ‹sum fn F ≤ sum gn F›
by (intro sum_mono) (use fn_le_gn elim in auto)
also have ‹… ≤ C› by (rule elim)
finally show ?case .
qed
thus ?thesis by auto
qed
have fn_summable: ‹fn summable_on A›
using fn_bound fn_nn
by (auto intro!: nonneg_bounded_partial_sums_imp_summable_on)
show ‹f abs_multipliable_on A›
using fn_summable unfolding fn_def
by (subst abs_multipliable_on_iff_summable_on)
qed
lemma abs_multipliable_product:
fixes x :: "'a ⇒ 'b::{real_normed_div_algebra,banach,second_countable_topology}"
assumes x2_sum: "x abs_multipliable_on A"
and y2_sum: "y abs_multipliable_on A"
shows "(λi. x i * y i) abs_multipliable_on A"
proof -
define xn yn where "xn i = norm (x i - 1)" and "yn i = norm (y i - 1)" for i
have xn_nn: "xn i ≥ 0" for i unfolding xn_def by simp
have yn_nn: "yn i ≥ 0" for i unfolding yn_def by simp
have prod_ineq: "1 + norm (x i * y i - 1) ≤ (1 + xn i) * (1 + yn i)" for i
proof -
have "x i * y i - 1 = (x i - 1) * (y i - 1) + (x i - 1) + (y i - 1)"
by (simp add: algebra_simps)
then have "norm (x i * y i - 1) ≤ norm ((x i - 1) * (y i - 1)) + norm (x i - 1) + norm (y i - 1)"
by (metis dual_order.refl norm_triangle_mono)
also have "… = xn i * yn i + xn i + yn i"
by (simp add: norm_mult xn_def yn_def)
finally have "1 + norm (x i * y i - 1) ≤ 1 + xn i * yn i + xn i + yn i"
by linarith
also have "… = (1 + xn i) * (1 + yn i)"
by (simp add: algebra_simps)
finally show ?thesis .
qed
from x2_sum have xn_mult: "(λi. 1 + xn i) multipliable_on A"
unfolding abs_multipliable_on_def xn_def by simp
from y2_sum have yn_mult: "(λi. 1 + yn i) multipliable_on A"
unfolding abs_multipliable_on_def yn_def by simp
have prod_mult: "(λi. (1 + xn i) * (1 + yn i)) multipliable_on A"
by (rule multipliable_on_mult[OF xn_mult yn_mult])
show "(λi. x i * y i) abs_multipliable_on A"
unfolding abs_multipliable_on_def
proof (rule multipliable_on_comparison_test[OF prod_mult])
fix i assume "i ∈ A"
show "1 + norm (x i * y i - 1) ≤ (1 + xn i) * (1 + yn i)"
by (rule prod_ineq)
next
fix i assume "i ∈ A"
show "(1::real) ≤ 1 + norm (x i * y i - 1)" by simp
qed
qed
lemma abs_multipliable_on_inverse:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field}"
assumes "f abs_multipliable_on A" and nz: "⋀x. x ∈ A ⟹ f x ≠ 0"
shows "(λx. inverse (f x)) abs_multipliable_on A"
proof -
have norm_sum: "(λx. norm (f x - 1)) summable_on A"
using assms(1) by (subst (asm) abs_multipliable_on_iff_summable_on)
from summable_on_imp_nhds_0[OF norm_sum, of "ball 0 (1/2 :: real)"]
obtain F where F_fin: "finite F" and F_sub: "F ⊆ A"
and F_small: "⋀x. x ∈ A - F ⟹ norm (f x - 1) ∈ ball 0 (1/2)"
by auto
have inv_bound: "norm (inverse (f x) - 1) ≤ 2 * norm (f x - 1)" if xSF: "x ∈ A - F" for x
proof -
have fx_nz: "f x ≠ 0" using xSF nz by auto
have small: "norm (f x - 1) < 1/2" using F_small xSF by auto
have "inverse (f x) - 1 = inverse (f x) * (1 - f x)"
using fx_nz by (simp add: field_simps)
hence "norm (inverse (f x) - 1) = norm (inverse (f x)) * norm (f x - 1)"
by (simp add: norm_mult norm_minus_commute)
moreover have "norm (inverse (f x)) ≤ 2"
proof -
have "norm (f x) ≥ 1 - norm (f x - 1)"
by (smt (verit, ccfv_SIG) norm_minus_commute norm_one norm_triangle_ineq2)
hence "norm (f x) > 1/2" using small by linarith
hence "norm (inverse (f x)) = inverse (norm (f x))"
by (simp add: norm_inverse)
also have "… ≤ 2" using ‹norm (f x) > 1/2›
by (simp add: inverse_less_imp_less less_eq_real_def)
finally show ?thesis .
qed
ultimately show ?thesis
by (simp add: mult_right_mono)
qed
have "(λx. norm (inverse (f x) - 1)) summable_on (A - F)"
proof (rule summable_on_comparison_test)
show "(λx. 2 * norm (f x - 1)) summable_on (A - F)"
using norm_sum F_sub F_fin summable_on_cmult_right summable_on_cofin_subset by blast
fix x assume "x ∈ A - F"
thus "norm (inverse (f x) - 1) ≤ 2 * norm (f x - 1)"
using inv_bound by simp
qed auto
moreover have "(λx. norm (inverse (f x) - 1)) summable_on F"
using F_fin by simp
ultimately have "(λx. norm (inverse (f x) - 1)) summable_on (A - F ∪ F)"
by (intro summable_on_Un_disjoint) auto
also have "A - F ∪ F = A" using F_sub by auto
finally show "(λx. inverse (f x)) abs_multipliable_on A"
by (subst abs_multipliable_on_iff_summable_on)
qed
text ‹The types @{typ ennreal}, @{typ ereal}, and @{typ enat} cannot be used with the
infinite-product framework (@{const multipliable_on}, @{const has_setprod}, @{const infprod})
because it requires @{class semidom}, which demands additive cancellation.
These types fail cancellation: e.g.\ @{term ‹(∞::ennreal) + 1 = ∞ + 2›} but @{term ‹(1::ennreal) ≠ 2›}.
Supporting them would require weakening the type class constraints on the framework definitions.›
lemma multipliable_countable:
fixes f :: ‹'a ⇒ 'b :: {real_normed_div_algebra, semidom}›
assumes ‹f strongly_multipliable_on A›
shows ‹countable {x∈A. f x ≠ 1}›
proof -
have "∃F. finite F ∧ F ⊆ A ∧ (∀x∈A - F. f x ∈ ball 1 (1 / real (Suc n)))" for n
using strongly_multipliable_on_imp_nhds_1[OF assms, of "ball 1 (1 / real (Suc n))"] by auto
then obtain F where F_fin: "⋀n. finite (F n)" and F_sub: "⋀n. F n ⊆ A"
and F_ball: "⋀n x. x ∈ A - F n ⟹ f x ∈ ball 1 (1 / real (Suc n))"
by metis
have "{x∈A. f x ≠ 1} ⊆ (⋃n. F n)"
proof (rule subsetI)
fix x assume "x ∈ {x∈A. f x ≠ 1}"
hence "x ∈ A" "f x ≠ 1" by auto
hence "dist (f x) 1 > 0" by auto
then obtain n where "1 / real (Suc n) < dist (f x) 1"
using reals_Archimedean by (metis inverse_eq_divide)
hence "f x ∉ ball 1 (1 / real (Suc n))"
by (simp add: dist_commute)
hence "x ∉ A - F n"
using F_ball[of x n] by blast
hence "x ∈ F n"
using ‹x ∈ A› by auto
thus "x ∈ (⋃n. F n)" by auto
qed
moreover have "countable (⋃n. F n)"
using F_fin by (intro countable_UN) (auto intro: countable_finite)
ultimately show ?thesis
by (rule countable_subset)
qed
text ‹
Taking norms turns an unordered product into an unordered product of reals; this is the bridge
to the real theory (and to ‹strongly_multipliable_on_iff_abs_multipliable_on_real›).
›
lemma has_setprod_norm:
fixes f :: "'a ⇒ 'b :: {real_normed_div_algebra, semidom}"
assumes "(f has_setprod P) A"
shows "((λx. norm (f x)) has_setprod norm P) A"
proof -
have "((λX. norm (prod f X)) ⤏ norm P) (finite_subsets_at_top A)"
using assms unfolding has_setprod_def by (intro tendsto_norm)
moreover have "norm (prod f X) = (∏x∈X. norm (f x))" for X
by (simp add: Real_Vector_Spaces.prod_norm)
ultimately show ?thesis
unfolding has_setprod_def by simp
qed
corollary multipliable_on_norm:
fixes f :: "'a ⇒ 'b :: {real_normed_div_algebra, semidom}"
assumes "f multipliable_on A"
shows "(λx. norm (f x)) multipliable_on A"
using assms has_setprod_norm has_setprod_imp_multipliable multipliable_on_def by blast
lemma prod_norm_le:
fixes f::"'b ⇒ 'a::real_normed_field"
assumes "⋀x. x ∈ S ⟹ norm (f x) ≤ g x"
shows "norm (prod f S) ≤ prod g S"
by (metis norm_ge_zero prod_mono prod_norm assms)
lemma norm_infprod_le:
fixes f::"'b ⇒ 'a::real_normed_field"
assumes "(f has_setprod S) X"
assumes "(g has_setprod T) X"
assumes "⋀x. x ∈ X ⟹ norm (f x) ≤ g x"
shows "norm S ≤ T"
proof (rule tendsto_le)
show "((λY. norm (∏x∈Y. f x)) ⤏ norm S) (finite_subsets_at_top X)"
using assms(1) unfolding has_setprod_def by (intro tendsto_norm)
show "((λY. ∏x∈Y. g x) ⤏ T) (finite_subsets_at_top X)"
using assms(2) unfolding has_setprod_def .
show "∀⇩F x in finite_subsets_at_top X. norm (prod f x) ≤ (∏x∈x. g x)"
by (simp add: assms(3) eventually_finite_subsets_at_top_weakI in_mono prod_norm_le)
qed auto
lemma abs_multipliable_on_exp:
fixes f :: "'a ⇒ 'b :: {real_normed_field, banach}"
assumes "f abs_summable_on A"
shows "(λx. exp (f x)) abs_multipliable_on A"
unfolding abs_multipliable_on_iff_summable_on
proof -
obtain B where B: "finite B" "B ⊆ A" "∀x∈A-B. f x ∈ ball 0 (1/2)"
using summable_on_imp_nhds_0[OF abs_summable_summable[OF assms(1)], of "ball 0 (1/2)"] by auto
have "(λx. exp (f x) - 1) abs_summable_on (A-B)"
proof (rule summable_on_comparison_test)
show "(λx. 3/2 * norm (f x)) summable_on (A - B)"
by (intro summable_on_cmult_right summable_on_subset[OF assms]) auto
next
fix x assume x: "x ∈ A - B"
have "norm (f x) ≤ 1 / 2"
by (intro less_imp_le) (use B x in auto)
thus "norm (exp (f x) - 1) ≤ 3/2 * norm (f x)"
using norm_exp_bounds(2)[of "f x"] by simp
qed auto
hence "(λx. exp (f x) - 1) abs_summable_on (A - B ∪ B)"
by (intro summable_on_Un_disjoint) (use B in auto)
also have "A - B ∪ B = A"
using B by blast
finally show "(λx. exp (f x) - 1) abs_summable_on A" .
qed
lemma abs_multipliable_on_imp_strongly_multipliable_on:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field}"
assumes "f abs_multipliable_on A"
shows "f strongly_multipliable_on A"
proof -
have norm_sum: "(λx. norm (f x - 1)) summable_on A"
using assms by (subst (asm) abs_multipliable_on_iff_summable_on)
have fin_zeros: "finite {x∈A. f x = 0}"
proof -
from summable_on_imp_nhds_0[OF abs_summable_summable[OF norm_sum], of "ball 0 (1::real)"]
obtain F where F: "finite F" "F ⊆ A" "∀x∈A - F. norm (f x - 1) ∈ ball 0 1"
by auto
show ?thesis
by (rule finite_subset[OF _ F(1)]) (use F(3) in force)
qed
define S where "S = {x∈A. f x ≠ 0}"
have S_sub: "S ⊆ A" unfolding S_def by auto
have nz: "⋀x. x ∈ S ⟹ f x ≠ 0" unfolding S_def by auto
have norm_sum_S: "(λx. norm (f x - 1)) summable_on S"
using norm_sum S_sub by (rule summable_on_subset_banach)
have abs_mult_S: "f abs_multipliable_on S"
using norm_sum_S by (subst abs_multipliable_on_iff_summable_on)
have mult_S: "f multipliable_on S"
by (rule abs_multipliable_multipliable[OF abs_mult_S])
have inv_abs_mult_S: "(λx. inverse (f x)) abs_multipliable_on S"
by (rule abs_multipliable_on_inverse) fact+
have inv_mult_S: "(λx. inverse (f x)) multipliable_on S"
by (rule abs_multipliable_multipliable[OF inv_abs_mult_S])
have "infprod (λx. f x * inverse (f x)) S = infprod f S * infprod (λx. inverse (f x)) S"
by (rule infprod_mult[OF mult_S inv_mult_S])
moreover have "infprod (λx. f x * inverse (f x)) S = 1"
by (intro infprod_1) (use nz in auto)
ultimately have prod_nz: "infprod f S ≠ 0"
by (metis mult_zero_left zero_neq_one)
from mult_S prod_nz obtain P where "(f has_setprod P) S" "P ≠ 0"
using has_setprod_infprod multipliable_on_def by fastforce
with fin_zeros show ?thesis
unfolding strongly_multipliable_on_def S_def by blast
qed
lemma multipliable_on_union:
fixes f :: "_ ⇒ 'a :: {real_normed_field, complete_space}"
assumes "f multipliable_on A" "f multipliable_on B"
shows "f multipliable_on (A ∪ B)"
proof (cases "∃x∈A ∪ B. f x = 0")
case True
then obtain x where "x ∈ A ∪ B" "f x = 0" by auto
then show ?thesis
unfolding multipliable_on_def using zero_imp_has_setprod_0
by metis
next
case False
hence nz: "⋀x. x ∈ A ∪ B ⟹ f x ≠ 0" by auto
from assms(2) obtain T where T: "(f has_setprod T) B"
using multipliable_on_def by blast
show ?thesis
proof (cases "T = 0")
case False
then obtain P where "(f has_setprod P) (B - A)"
using has_setprod_subset_nonzero[OF T] by blast
then have "f multipliable_on (B - A)"
by (rule has_setprod_imp_multipliable)
then show ?thesis
using assms(1)
by (metis Diff_disjoint Un_Diff_cancel multipliable_on_Un_disjoint)
next
case True
have limA: "(prod f ⤏ infprod f A) (finite_subsets_at_top A)"
using has_setprod_infprod[OF assms(1)] by (simp add: has_setprod_def)
obtain C where C: "C > 0"
and Cbd: "⋀Y. finite Y ⟹ Y ⊆ A ⟹ norm (prod f Y) ≤ C"
using multipliable_on_imp_bdd_prods[OF limA] nz by blast
have "(f has_setprod 0) (A ∪ B)"
unfolding has_setprod_def
proof (rule tendstoI)
fix e :: real assume "e > 0"
with C have eC: "e / C > 0" by simp
from T True have "(prod f ⤏ 0) (finite_subsets_at_top B)"
by (simp add: has_setprod_def)
from tendstoD[OF this eC] obtain W where W: "finite W" "W ⊆ B"
and Wclose: "⋀Y. finite Y ⟹ W ⊆ Y ⟹ Y ⊆ B ⟹ dist (prod f Y) 0 < e / C"
unfolding eventually_finite_subsets_at_top by metis
show "∀⇩F X in finite_subsets_at_top (A ∪ B). dist (prod f X) 0 < e"
unfolding eventually_finite_subsets_at_top
proof (intro exI[of _ W] conjI allI impI)
show "finite W" "W ⊆ A ∪ B" using W by auto
fix X assume X: "finite X ∧ W ⊆ X ∧ X ⊆ A ∪ B"
hence Xf: "finite X" and WX: "W ⊆ X" and XAB: "X ⊆ A ∪ B" by auto
have XB: "X - B ⊆ A"
using XAB by blast
have "prod f X = prod f (X ∩ B) * prod f (X - B)"
using Xf by (rule prod.Int_Diff)
hence "norm (prod f X) = norm (prod f (X ∩ B)) * norm (prod f (X - B))"
by (simp add: norm_mult)
also have "… < e / C * C"
proof (rule mult_less_le_imp_less)
show "norm (prod f (X ∩ B)) < e / C"
using Wclose[of "X ∩ B"] Xf WX W by (auto simp: dist_norm)
show "norm (prod f (X - B)) ≤ C"
using Cbd[of "X - B"] Xf XB by auto
show "0 ≤ norm (prod f (X ∩ B))" by simp
show "0 < norm (prod f (X - B))"
using Xf XB nz by (auto simp: prod_norm intro!: prod_pos)
qed
also have "… = e"
using C by simp
finally show "dist (prod f X) 0 < e"
by simp
qed
qed
thus ?thesis
by (rule has_setprod_imp_multipliable)
qed
qed
lemma multipliable_on_insert_iff:
fixes f :: "_ ⇒ 'a :: {real_normed_field, complete_space}"
assumes "f x ≠ 0"
shows "f multipliable_on insert x A ⟷ f multipliable_on A"
proof
assume "f multipliable_on A"
then show "f multipliable_on insert x A"
using multipliable_on_union[of f A "{x}"] by simp
next
assume *: "f multipliable_on insert x A"
show "f multipliable_on A"
proof (rule multipliable_on_subset_finite_Diff[OF *])
show "finite (insert x A - A)"
by (rule finite_subset[of _ "{x}"]) auto
qed (use assms in auto)
qed
lemma has_setprod_finiteI: "finite A ⟹ S = prod f A ⟹ (f has_setprod S) A"
by simp
lemma has_setprod_insert:
fixes f :: "'a ⇒ 'b :: {topological_comm_monoid_mult, semidom, t2_space}"
assumes "x ∉ A" and "(f has_setprod S) A"
shows "(f has_setprod (f x * S)) (insert x A)"
proof -
have "(f has_setprod (f x * S)) ({x} ∪ A)"
using assms by (intro has_setprod_Un_disjoint) (auto intro: has_setprod_finiteI)
thus ?thesis by simp
qed
lemma infprod_insert:
fixes f :: "_ ⇒ 'a :: {topological_comm_monoid_mult, semidom, t2_space}"
assumes "f multipliable_on A" "a ∉ A"
shows "infprod f (insert a A) = f a * infprod f A"
by (meson assms has_setprod_insert infprodI multipliable_iff_has_setprod_infprod)
text ‹
Restricting a product to one fibre again needs a non-zero product: for a family that is merely
multipliable this fails, even when all the factors off the fibre are non-zero. (Take
\<^term>‹A = {True, False}›, both fibres \<^term>‹UNIV :: nat set›, ‹f True b = -1› and
‹f False b = 1/2›: the whole family is multipliable with product ‹0›, but the fibre over
\<^term>‹True› is not multipliable.)
›
lemma multipliable_on_SigmaD1:
fixes f :: "_ ⇒ _ ⇒ 'a :: {real_normed_field, complete_space}"
assumes f: "(λ(x,y). f x y) strongly_multipliable_on Sigma A B"
assumes x: "x ∈ A"
shows "f x multipliable_on B x"
proof -
have "Sigma {x} B ⊆ Sigma A B"
using x by auto
from strongly_multipliable_on_subset[OF f this]
have step1: "(λ(x,y). f x y) multipliable_on Sigma {x} B"
by (rule strongly_multipliable_imp_multipliable)
have step2: "(λy. f x y) ∘ snd multipliable_on Sigma {x} B"
using step1 multipliable_on_cong[of "Sigma {x} B" "λ(a,b). f a b" "(λy. f x y) ∘ snd"]
by auto
have inj: "inj_on snd (Sigma {x} B)"
by (auto intro!: inj_onI simp: Sigma_def)
have step3: "(λy. f x y) multipliable_on snd ` Sigma {x} B"
using step2 multipliable_on_reindex[OF inj, of "λy. f x y"] by simp
have "snd ` Sigma {x} B = B x"
by (force simp: Sigma_def)
with step3 show ?thesis by simp
qed
lemma has_setprod_swap:
"(f has_setprod S) (A × B) ⟷ ((λ(x,y). f (y,x)) has_setprod S) (B × A)"
proof -
have "bij_betw (λ(x,y). (y,x)) (B × A) (A × B)"
by (rule bij_betwI[of _ _ _ "λ(x,y). (y,x)"]) auto
from has_setprod_reindex_bij_betw[OF this, where f = f] show ?thesis
by (simp add: case_prod_unfold)
qed
lemma multipliable_on_swap:
"f multipliable_on (A × B) ⟷ (λ(x,y). f (y,x)) multipliable_on (B × A)"
by (metis has_setprod_swap multipliable_on_def)
text ‹
❙‹Not› lemmas. For \<^term>‹c ≠ 0›, neither
‹((λx. c * f x) has_setprod S) A› nor ‹((λx. f x * c) has_setprod S) A› is
equivalent to ‹(f has_setprod S / c) A›: scaling every factor scales the product by
\<^term>‹c ^ card A›, not by \<^term>‹c›. Counterexample: for \<^term>‹A = {1, 2 :: nat}›,
\<^term>‹f = (λ_. 1 :: real)› and \<^term>‹c = (2 :: real)› the scaled product is $4$,
while the product of \<^term>‹f› is $1$ and \<^term>‹S / c› is $2$.
›
lemma finite_nonzero_values_imp_multipliable_on:
assumes "finite {x∈X. f x ≠ 0}"
shows "f multipliable_on X"
proof (cases "finite X")
case True
then show ?thesis by simp
next
case False
then have "X - {x∈X. f x ≠ 0} ≠ {}"
using assms by (metis Collect_mem_eq Diff_eq_empty_iff finite_subset subset_refl)
then obtain x where "x ∈ X" "f x = 0" by auto
then have "(f has_setprod 0) X"
by (rule zero_imp_has_setprod_0)
then show ?thesis
unfolding multipliable_on_def by blast
qed
lemma multipliable_on_of_int_iff:
"(λx::'a. of_int (f x) :: 'b :: {real_normed_algebra_1, topological_semigroup_mult, semidom}) multipliable_on A ⟷ f multipliable_on A"
proof
assume "f multipliable_on A"
thus "(λx. of_int (f x)) multipliable_on A"
by (rule multipliable_on_homomorphism) auto
next
assume "(λx. of_int (f x) :: 'b) multipliable_on A"
then obtain S where "((λx. of_int (f x) :: 'b) has_setprod S) A"
by (auto simp: multipliable_on_def)
hence "(prod (λx. of_int (f x) :: 'b) ⤏ S) (finite_subsets_at_top A)"
unfolding has_setprod_def .
moreover have "1/2 > (0 :: real)"
by auto
ultimately have "eventually (λX. dist (prod (λx. of_int (f x) :: 'b) X) S < 1/2)
(finite_subsets_at_top A)"
unfolding tendsto_iff by blast
then obtain X where X: "finite X" "X ⊆ A"
"⋀Y. finite Y ⟹ X ⊆ Y ⟹ Y ⊆ A ⟹ dist (prod (λx. of_int (f x)) Y) S < 1/2"
unfolding eventually_finite_subsets_at_top by metis
have "prod f Y = prod f X" if "finite Y" "X ⊆ Y" "Y ⊆ A" for Y
proof -
have "dist (prod (λx. of_int (f x)) X) S < 1/2"
by (intro X) auto
moreover have "dist (prod (λx. of_int (f x)) Y) S < 1/2"
by (intro X that)
ultimately have "dist (prod (λx. of_int (f x)) X) (prod (λx. of_int (f x) :: 'b) Y) <
1/2 + 1/2"
using dist_triangle_less_add by blast
have eq: "of_int (prod f X) = (of_int (prod f Y) :: 'b)"
proof (rule ccontr)
assume "of_int (prod f X) ≠ (of_int (prod f Y) :: 'b)"
hence "prod f X ≠ prod f Y" by auto
hence "abs (prod f X - prod f Y) ≥ 1"
by (simp del: of_int_prod of_nat_prod)
hence "norm (of_int (prod f X - prod f Y) :: 'b) ≥ 1"
by (simp add: norm_of_int del: of_int_prod of_nat_prod of_int_diff)
hence "norm (of_int (prod f X) - (of_int (prod f Y) :: 'b)) ≥ 1"
by (simp add: of_int_diff)
moreover have "(of_int (prod f X) :: 'b) = prod (λx. of_int (f x)) X"
using X(1) by (induction X rule: finite_induct) (auto simp: of_int_mult)
moreover have "(of_int (prod f Y) :: 'b) = prod (λx. of_int (f x)) Y"
using that(1) by (induction Y rule: finite_induct) (auto simp: of_int_mult)
ultimately show False
using ‹dist (prod (λx. of_int (f x)) X) (prod (λx. of_int (f x) :: 'b) Y) < 1/2 + 1/2›
by (simp add: dist_norm)
qed
thus ?thesis
using eq by (simp add: of_int_eq_iff del: of_int_prod of_nat_prod)
qed
have "(prod f ⤏ prod f X) (finite_subsets_at_top A)"
proof (rule tendsto_eventually)
show "∀⇩F Y in finite_subsets_at_top A. prod f Y = prod f X"
unfolding eventually_finite_subsets_at_top
using X(1,2) ‹⋀Y. finite Y ⟹ X ⊆ Y ⟹ Y ⊆ A ⟹ prod f Y = prod f X›
by blast
qed
thus "f multipliable_on A"
unfolding multipliable_on_def has_setprod_def by blast
qed
lemma multipliable_on_of_nat_iff:
"(λx::'a. of_nat (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult}) multipliable_on A ⟷ f multipliable_on A"
proof
assume "f multipliable_on A"
thus "(λx. of_nat (f x) :: 'b) multipliable_on A"
by (rule multipliable_on_homomorphism) auto
next
assume "(λx. of_nat (f x) :: 'b) multipliable_on A"
hence "(λx. of_int (int (f x)) :: 'b) multipliable_on A"
by simp
also have "?this ⟷ (λx. int (f x)) multipliable_on A"
by (rule multipliable_on_of_int_iff)
also have "… ⟷ f multipliable_on A"
proof
have prod_int: "prod (λx. int (f x)) X = int (prod f X)" if "finite X" for X
using that by (induction X rule: finite_induct) auto
show "(λx. int (f x)) multipliable_on A ⟹ f multipliable_on A"
proof -
assume "(λx. int (f x)) multipliable_on A"
then obtain S where lim: "(prod (λx. int (f x)) ⤏ S) (finite_subsets_at_top A)"
by (auto simp: multipliable_on_def has_setprod_def)
have "∀⇩F X in finite_subsets_at_top A. prod (λx. int (f x)) X = S"
using lim by (simp add: tendsto_discrete)
then obtain X where X: "finite X" "X ⊆ A"
"⋀Y. finite Y ⟹ X ⊆ Y ⟹ Y ⊆ A ⟹ prod (λx. int (f x)) Y = S"
unfolding eventually_finite_subsets_at_top by metis
have "prod f Y = prod f X" if "finite Y" "X ⊆ Y" "Y ⊆ A" for Y
proof -
have "int (prod f X) = prod (λx. int (f x)) X"
using prod_int[OF X(1)] by simp
also have "… = S" by (rule X(3)) (use X in auto)
also have "… = prod (λx. int (f x)) Y" by (rule X(3)[symmetric]) (use that in auto)
also have "… = int (prod f Y)"
using prod_int[OF that(1)] by simp
finally show ?thesis by presburger
qed
hence "(prod f ⤏ prod f X) (finite_subsets_at_top A)"
by (intro tendsto_eventually)
(auto simp: eventually_finite_subsets_at_top intro!: exI[of _ X] X(1,2))
thus "f multipliable_on A"
unfolding multipliable_on_def has_setprod_def by blast
qed
show "f multipliable_on A ⟹ (λx. int (f x)) multipliable_on A"
by (rule multipliable_on_homomorphism) auto
qed
finally show "f multipliable_on A" .
qed
lemma infprod_of_nat:
"infprod (λx::'a. of_nat (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult}) A = of_nat (infprod f A)"
by (metis has_setprod_empty has_setprod_infprod has_setprod_of_nat infprodI infprod_def
multipliable_on_of_nat_iff)
lemma infprod_of_int:
"infprod (λx::'a. of_int (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult}) A = of_int (infprod f A)"
by (metis has_setprod_infprod has_setprod_of_int infprodI infprod_not_exists
multipliable_on_of_int_iff of_int_1)
text ‹
The ‹has_setprod› forms of the two lemmas above. ‹has_setprod_of_nat› and ‹has_setprod_of_int›
only go one way; here the embedded product converges only for an embedded value, and only when
the original product converges to it.
›
lemma has_setprod_of_nat_iff:
"((λx::'a. of_nat (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult})
has_setprod S) A ⟷ (∃S'. S = of_nat S' ∧ (f has_setprod S') A)"
proof
assume *: "((λx. of_nat (f x) :: 'b) has_setprod S) A"
hence "(f has_setprod infprod f A) A"
using has_setprod_infprod multipliable_on_def multipliable_on_of_nat_iff by blast
moreover from this have "S = of_nat (infprod f A)"
using * has_setprod_of_nat has_setprod_unique by blast
ultimately show "∃S'. S = of_nat S' ∧ (f has_setprod S') A"
by blast
qed (use has_setprod_of_nat in blast)
lemma has_setprod_of_int_iff:
"((λx::'a. of_int (f x) :: 'b :: {real_normed_algebra_1, semidom, topological_semigroup_mult})
has_setprod S) A ⟷ (∃S'. S = of_int S' ∧ (f has_setprod S') A)"
proof
assume *: "((λx. of_int (f x) :: 'b) has_setprod S) A"
hence "f multipliable_on A"
using has_setprod_imp_multipliable multipliable_on_of_int_iff by blast
hence "(f has_setprod infprod f A) A"
by (rule has_setprod_infprod)
moreover from this have "S = of_int (infprod f A)"
using * has_setprod_of_int has_setprod_unique by blast
ultimately show "∃S'. S = of_int S' ∧ (f has_setprod S') A"
by blast
qed (use has_setprod_of_int in blast)
text ‹
❙‹Fubini for absolute multipliability.› The criterion below replaces an earlier
‹multipliable_on_SigmaI› whose hypotheses were \<^term>‹f (x, y) ≥ 1› together with the order
classes \<^class>‹conditionally_complete_linorder› and \<^class>‹linordered_idom›. Those were not
arbitrary -- they are the multiplicative transcription of the library's own
‹summable_on_SigmaI›, which assumes \<^term>‹f (x, y) ≥ 0› and proves summability through a
supremum -- but products admit a route that sums do not: absolute multipliability is
∗‹summability of the norms of the deviations from› ‹1› (‹abs_multipliable_on_iff_summable_on›),
so the whole question can be handed to ‹abs_summable_on_Sigma_iff› in
\<^theory>‹HOL-Analysis.Infinite_Sum›. That needs no order at all, only a Banach algebra, and it
gives an iff rather than one implication.
Nothing is lost over the reals: for a family with \<^term>‹f x ≥ 1› one has
\<^term>‹1 + norm (f x - 1) = f x›, so multipliability and absolute multipliability coincide there.
The hypotheses have a different shape, though -- summability of the fibre sums
\<^term>‹∑⇩∞y∈B x. norm (f (x, y) - 1)› in place of multipliability of the fibre products -- and
the equivalence of the two shapes is not proved here.
›
lemma abs_multipliable_on_Sigma_iff:
fixes f :: "'a × 'b ⇒ 'c :: {banach, real_normed_algebra_1}"
shows "f abs_multipliable_on Sigma A B ⟷
(∀x∈A. (λy. f (x, y)) abs_multipliable_on B x) ∧
((λx. ∑⇩∞y∈B x. norm (f (x, y) - 1)) summable_on A)"
proof -
define g where "g = (λp. norm (f p - 1))"
have nn: "g p ≥ 0" for p
by (simp add: g_def)
have norm_g: "norm (g p) = g p" for p
using nn by simp
have "f abs_multipliable_on Sigma A B ⟷ g summable_on Sigma A B"
unfolding g_def by (rule abs_multipliable_on_iff_summable_on)
also have "… ⟷ g abs_summable_on Sigma A B"
by (rule summable_on_iff_abs_summable_on_real)
also have "… ⟷ (∀x∈A. (λy. g (x, y)) abs_summable_on B x) ∧
((λx. ∑⇩∞y∈B x. norm (g (x, y))) abs_summable_on A)"
by (rule Infinite_Sum.abs_summable_on_Sigma_iff)
also have "… ⟷ (∀x∈A. (λy. g (x, y)) summable_on B x) ∧
((λx. ∑⇩∞y∈B x. g (x, y)) summable_on A)"
proof -
have "(λx. ∑⇩∞y∈B x. g (x, y)) abs_summable_on A
⟷ (λx. ∑⇩∞y∈B x. g (x, y)) summable_on A"
by (rule summable_on_iff_abs_summable_on_real[symmetric])
thus ?thesis
unfolding norm_g by blast
qed
also have "… ⟷ (∀x∈A. (λy. f (x, y)) abs_multipliable_on B x) ∧
((λx. ∑⇩∞y∈B x. norm (f (x, y) - 1)) summable_on A)"
by (simp add: abs_multipliable_on_iff_summable_on g_def)
finally show ?thesis .
qed
corollary abs_multipliable_on_SigmaI:
fixes f :: "'a × 'b ⇒ 'c :: {banach, real_normed_algebra_1}"
assumes "⋀x. x ∈ A ⟹ (λy. f (x, y)) abs_multipliable_on B x"
and "(λx. ∑⇩∞y∈B x. norm (f (x, y) - 1)) summable_on A"
shows "f abs_multipliable_on Sigma A B"
using assms by (simp add: abs_multipliable_on_Sigma_iff)
corollary multipliable_on_SigmaI:
fixes f :: "'a × 'b ⇒ 'c :: {banach, real_normed_field}"
assumes "⋀x. x ∈ A ⟹ (λy. f (x, y)) abs_multipliable_on B x"
and "(λx. ∑⇩∞y∈B x. norm (f (x, y) - 1)) summable_on A"
shows "f multipliable_on Sigma A B"
using abs_multipliable_on_SigmaI[OF assms]
by (blast intro: strongly_multipliable_imp_multipliable
abs_multipliable_on_imp_strongly_multipliable_on)
corollary abs_multipliable_on_UnionI:
fixes f :: "'b ⇒ 'c :: {banach, real_normed_algebra_1}"
assumes f: "⋀x. x ∈ A ⟹ f abs_multipliable_on B x"
and sum: "(λx. ∑⇩∞y∈B x. norm (f y - 1)) summable_on A"
and disj: "disjoint_family_on B A"
shows "f abs_multipliable_on (⋃x∈A. B x)"
proof -
have "(f ∘ snd) abs_multipliable_on Sigma A B"
using f sum by (intro abs_multipliable_on_SigmaI) auto
also have "?this ⟷ f abs_multipliable_on (snd ` Sigma A B)"
unfolding abs_multipliable_on_def o_def using disj
by (subst multipliable_on_reindex[where h = snd, unfolded o_def];
force simp: disjoint_family_on_def inj_on_def)
also have "snd ` Sigma A B = (⋃x∈A. B x)"
by force
finally show ?thesis .
qed
corollary multipliable_on_UnionI:
fixes f :: "'b ⇒ 'c :: {banach, real_normed_field}"
assumes "⋀x. x ∈ A ⟹ f abs_multipliable_on B x"
and "(λx. ∑⇩∞y∈B x. norm (f y - 1)) summable_on A"
and "disjoint_family_on B A"
shows "f multipliable_on (⋃x∈A. B x)"
using abs_multipliable_on_UnionI[OF assms]
by (blast intro: strongly_multipliable_imp_multipliable
abs_multipliable_on_imp_strongly_multipliable_on)
lemma multipliable_on_SigmaD:
fixes f :: "'a × 'b ⇒ 'c :: real_normed_field"
assumes sum1: "f multipliable_on (Sigma A B)"
assumes sum2: "⋀x. x ∈ A ⟹ (λy. f (x, y)) multipliable_on (B x)"
shows "(λx. infprod (λy. f (x, y)) (B x)) multipliable_on A"
using assms unfolding multipliable_on_def
by (smt (verit, del_insts) assms has_setprod_Sigma has_setprod_cong has_setprod_infprod)
lemma multipliable_on_UnionD:
fixes f :: "'a ⇒ 'c :: real_normed_field"
assumes sum1: "f multipliable_on (⋃x∈A. B x)"
assumes sum2: "⋀x. x ∈ A ⟹ f multipliable_on (B x)"
assumes disj: "disjoint_family_on B A"
shows "(λx. infprod f (B x)) multipliable_on A"
proof -
have "(⋃x∈A. B x) = snd ` Sigma A B"
by (force simp: Sigma_def)
with sum1 have "f multipliable_on (snd ` Sigma A B)"
by simp
also have "?this ⟷ (f ∘ snd) multipliable_on (Sigma A B)"
using disj by (intro multipliable_on_reindex inj_onI) (force simp: disjoint_family_on_def)
finally show "(λx. infprod f (B x)) multipliable_on A"
using multipliable_on_SigmaD[of "f ∘ snd" A B] sum2 by simp
qed
text ‹
❙‹NOTE.› The next lemma is about sums, not products, and belongs in
\<^theory>‹HOL-Analysis.Infinite_Sum›. It is the Weierstrass ‹M›-test for ∗‹unordered› sums in its
uniform form: a family dominated by a summable \<^term>‹M› converges uniformly on \<^term>‹B› along
\<^term>‹finite_subsets_at_top A›. It is proved here because that is where it was needed.
›
lemma uniform_limit_infsum_M_test:
fixes h :: "'k ⇒ 'a ⇒ real"
assumes le: "⋀k y. k ∈ A ⟹ y ∈ B ⟹ h k y ≤ M k"
and nn: "⋀k y. k ∈ A ⟹ y ∈ B ⟹ 0 ≤ h k y"
and M: "M summable_on A"
shows "uniform_limit B (λX y. ∑k∈X. h k y) (λy. ∑⇩∞k∈A. h k y) (finite_subsets_at_top A)"
proof (cases "B = {}")
case True
thus ?thesis
by simp
next
case False
then obtain y0 where y0: "y0 ∈ B" by blast
have Mnn: "0 ≤ M k" if "k ∈ A" for k
using nn[OF that y0] le[OF that y0] by linarith
have summ: "(λk. h k y) summable_on A" if "y ∈ B" for y
using M by (rule summable_on_comparison_test) (use le nn that in auto)
have summ_sub: "(λk. h k y) summable_on A'" if "y ∈ B" "A' ⊆ A" for y A'
using summ[OF that(1)] that(2) by (rule summable_on_subset_banach)
have M_sub: "M summable_on A'" if "A' ⊆ A" for A'
using M that by (rule summable_on_subset_banach)
have split: "(∑⇩∞k∈A. h k y) = (∑k∈X. h k y) + (∑⇩∞k∈A-X. h k y)"
if "y ∈ B" "finite X" "X ⊆ A" for y X
proof -
have "A = X ∪ (A - X)"
using that by auto
hence "(∑⇩∞k∈A. h k y) = (∑⇩∞k∈X ∪ (A - X). h k y)"
by simp
also have "… = (∑⇩∞k∈X. h k y) + (∑⇩∞k∈A-X. h k y)"
using that by (intro infsum_Un_disjoint summ_sub) auto
finally show ?thesis
using that by simp
qed
have splitM: "(∑⇩∞k∈A. M k) = (∑k∈X. M k) + (∑⇩∞k∈A-X. M k)"
if "finite X" "X ⊆ A" for X
proof -
have "A = X ∪ (A - X)"
using that by auto
hence "(∑⇩∞k∈A. M k) = (∑⇩∞k∈X ∪ (A - X). M k)"
by simp
also have "… = (∑⇩∞k∈X. M k) + (∑⇩∞k∈A-X. M k)"
using that by (intro infsum_Un_disjoint M_sub) auto
finally show ?thesis
using that by simp
qed
show ?thesis
unfolding uniform_limit_iff
proof (intro allI impI)
fix ε :: real assume ε: "ε > 0"
obtain S where S: "finite S" "S ⊆ A" and Sclose: "dist (∑k∈S. M k) (∑⇩∞k∈A. M k) ≤ ε/2"
using infsum_finite_approximation[OF M, of "ε/2"] ε by auto
have tailM: "(∑⇩∞k∈A-S. M k) ≤ ε/2"
using Sclose splitM[OF S] by (simp add: dist_real_def)
show "∀⇩F X in finite_subsets_at_top A. ∀y∈B. dist (∑k∈X. h k y) (∑⇩∞k∈A. h k y) < ε"
unfolding eventually_finite_subsets_at_top
proof (intro exI[of _ S] conjI allI impI S)
fix X assume X: "finite X ∧ S ⊆ X ∧ X ⊆ A"
hence X': "finite X" "S ⊆ X" "X ⊆ A" by auto
show "∀y∈B. dist (∑k∈X. h k y) (∑⇩∞k∈A. h k y) < ε"
proof
fix y assume y: "y ∈ B"
have nonneg: "0 ≤ (∑⇩∞k∈A-X. h k y)"
using nn y by (intro infsum_nonneg) auto
have "(∑⇩∞k∈A-X. h k y) ≤ (∑⇩∞k∈A-X. M k)"
using y X' le by (intro infsum_mono summ_sub M_sub) auto
also have "… ≤ (∑⇩∞k∈A-S. M k)"
using X' Mnn by (intro infsum_mono2 M_sub) auto
also have "… ≤ ε/2"
by (rule tailM)
finally have "(∑⇩∞k∈A-X. h k y) ≤ ε/2" .
moreover have "dist (∑k∈X. h k y) (∑⇩∞k∈A. h k y) = (∑⇩∞k∈A-X. h k y)"
using split[OF y X'(1,3)] nonneg by (simp add: dist_real_def)
ultimately show "dist (∑k∈X. h k y) (∑⇩∞k∈A. h k y) < ε"
using ε by simp
qed
qed
qed
qed
text ‹
The workhorse for products. Earlier versions of this lemma assumed \<^term>‹continuous_on B (f n)›
for every \<^term>‹n› together with \<^term>‹compact B›; those served only to bound the limit
\<^term>‹L› of the partial sums on \<^term>‹B›, so that bound is now the hypothesis and \<^term>‹B› may be
any set. The usable form is the ‹M›-test ‹uniform_limit_infprod_M_test› below, which discharges
the uniform-convergence hypothesis as well.
›
lemma uniform_limit_prodinf:
fixes f :: "'k ⇒ 'a :: topological_space ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach, semidom, topological_semigroup_mult, t2_space}"
assumes conv_sum: "uniform_limit B (λX y. ∑x∈X. norm (f x y)) L (finite_subsets_at_top A)"
assumes bdd: "⋀y. y ∈ B ⟹ L y ≤ C"
shows "uniform_limit B (λX y. ∏x∈X. 1 + f x y) (λy. ∏⇩∞x∈A. 1 + f x y) (finite_subsets_at_top A)"
unfolding uniform_limit_iff
proof (intro allI impI)
fix ε :: real assume ε: "ε > 0"
have summ_y: "(λn. norm (f n y)) summable_on A" if "y ∈ B" for y
proof -
from conv_sum that have "((λX. ∑x∈X. norm (f x y)) ⤏ L y) (finite_subsets_at_top A)"
by (intro tendsto_uniform_limitI)
thus ?thesis
unfolding summable_on_def has_sum_def by blast
qed
have mult_y: "(λx. 1 + f x y) multipliable_on A" if "y ∈ B" for y
by (simp add: abs_multipliable_multipliable abs_multipliable_on_iff_summable_on summ_y that)
have prod_tendsto: "(prod (λx. 1 + f x y) ⤏ infprod (λx. 1 + f x y) A) (finite_subsets_at_top A)"
if "y ∈ B" for y
using mult_y[OF that] by (rule infprod_tendsto)
define r where "r = ln (1 + ε / exp (C+1))"
have r_pos: "r > 0"
unfolding r_def using ε by (intro ln_gt_zero) (auto intro: add_pos_pos)
have exp_r: "exp r = 1 + ε / exp (C+1)"
unfolding r_def using ε by (subst exp_ln) (auto intro: add_pos_pos)
have "∀⇩F X in finite_subsets_at_top A. ∀y∈B. dist (∑x∈X. norm (f x y)) (L y) < min 1 (r/4)"
proof -
have "min 1 (r/4) > 0" using r_pos by auto
with conv_sum show ?thesis unfolding uniform_limit_iff by blast
qed
then obtain X0 where X0: "finite X0" "X0 ⊆ A" and
X0_prop: "⋀X. ⟦finite X; X0 ⊆ X; X ⊆ A⟧ ⟹ ∀y∈B. dist (∑x∈X. norm (f x y)) (L y) < min 1 (r/4)"
by (auto simp: eventually_finite_subsets_at_top)
show "∀⇩F X in finite_subsets_at_top A. ∀y∈B. dist (∏x∈X. 1 + f x y) (∏⇩∞x∈A. 1 + f x y) < ε"
unfolding eventually_finite_subsets_at_top
proof (intro exI conjI allI impI)
show "finite X0" by (rule X0(1))
show "X0 ⊆ A" by (rule X0(2))
fix X assume X_props: "finite X ∧ X0 ⊆ X ∧ X ⊆ A"
then have X_fin: "finite X" and X0_X: "X0 ⊆ X" and X_sub: "X ⊆ A" by auto
show "∀y∈B. dist (∏x∈X. 1 + f x y) (∏⇩∞x∈A. 1 + f x y) < ε"
proof
fix y assume y: "y ∈ B"
define g where "g = (λx. 1 + f x y)"
have limg: "(prod g ⤏ infprod g A) (finite_subsets_at_top A)"
using prod_tendsto[OF y] unfolding g_def .
have dX: "dist (∑x∈X. norm (f x y)) (L y) < min 1 (r/4)"
using X0_prop[OF X_fin X0_X X_sub] y by blast
have sumX_le: "(∑x∈X. norm (f x y)) ≤ L y + 1"
using dX unfolding dist_real_def by linarith
have normgX: "norm (prod g X) ≤ exp (L y + 1)"
proof -
have pe: "norm (g x) ≤ 1 + norm (f x y)" for x
unfolding g_def using norm_triangle_ineq[of 1 "f x y"] by simp
have "norm (prod g X) = (∏x∈X. norm (g x))"
by (simp add: prod_norm)
also have "… ≤ (∏x∈X. 1 + norm (f x y))"
by (intro prod_mono conjI) (use pe in auto)
also have "… ≤ exp (∑x∈X. norm (f x y))"
by (intro prod_le_exp_sum) auto
also have "… ≤ exp (L y + 1)"
using sumX_le by simp
finally show ?thesis .
qed
have step_bound: "dist (prod g X) (prod g X2) ≤ exp (L y + 1) * (exp (∑x∈X2 - X. norm (f x y)) - 1)"
if X2: "finite X2" "X ⊆ X2" "X2 ⊆ A" for X2
proof -
define D where "D = X2 - X"
have Dfin: "finite D" and Ddisj: "X ∩ D = {}" and X2eq: "X2 = X ∪ D"
using X2 X_fin unfolding D_def by auto
have normD: "norm (prod g D - 1) ≤ exp (∑x∈D. norm (f x y)) - 1"
proof -
have "norm (prod g D - 1) ≤ (∏x∈D. 1 + norm (f x y)) - 1"
unfolding g_def using norm_prod_minus1_le_prod_minus1[of "λx. f x y" D] by simp
also have "(∏x∈D. 1 + norm (f x y)) ≤ exp (∑x∈D. norm (f x y))"
by (intro prod_le_exp_sum) auto
finally show ?thesis by simp
qed
have "prod g X2 = prod g X * prod g D"
unfolding X2eq using X_fin Dfin Ddisj by (simp add: prod.union_disjoint)
hence "prod g X2 - prod g X = prod g X * (prod g D - 1)"
by (simp add: algebra_simps)
hence "dist (prod g X) (prod g X2) = norm (prod g X) * norm (prod g D - 1)"
by (simp add: dist_norm norm_mult norm_minus_commute)
also have "… ≤ exp (L y + 1) * (exp (∑x∈D. norm (f x y)) - 1)"
by (intro mult_mono normgX normD) auto
finally show ?thesis unfolding D_def .
qed
have tail_bound: "(∑x∈X2 - X. norm (f x y)) ≤ r/2"
if X2: "finite X2" "X ⊆ X2" "X2 ⊆ A" for X2
proof -
have "(∑x∈X2. norm (f x y)) = (∑x∈X. norm (f x y)) + (∑x∈X2 - X. norm (f x y))"
using X2 X_fin by (subst sum.subset_diff[of X X2]) auto
moreover have "dist (∑x∈X2. norm (f x y)) (L y) < min 1 (r/4)"
using X0_prop[OF X2(1) _ X2(3)] X0_X X2(2) y by blast
ultimately show ?thesis using dX unfolding dist_real_def by linarith
qed
have dist_le_C: "dist (prod g X) (prod g X2) ≤ exp (L y + 1) * (exp (r/2) - 1)"
if X2: "finite X2" "X ⊆ X2" "X2 ⊆ A" for X2
using step_bound tail_bound that
by (smt (verit, best) exp_ge_zero exp_mono mult_left_mono)
have "infprod g A ∈ cball (prod g X) (exp (L y + 1) * (exp (r/2) - 1))"
proof (rule Lim_in_closed_set[OF closed_cball _ _ limg])
show "∀⇩F X2 in finite_subsets_at_top A. prod g X2 ∈ cball (prod g X) (exp (L y + 1) * (exp (r/2) - 1))"
unfolding eventually_finite_subsets_at_top
using X_props dist_le_C by auto
qed auto
hence lim_le_C: "dist (prod g X) (infprod g A) ≤ exp (L y + 1) * (exp (r/2) - 1)"
by (simp add: dist_commute mem_cball)
have "exp (L y + 1) * (exp (r/2) - 1) < ε"
proof -
have "exp (L y + 1) * (exp (r/2) - 1) ≤ exp (C + 1) * (exp (r/2) - 1)"
using r_pos bdd[OF y] by (intro mult_right_mono) auto
also have "… < exp (C + 1) * (exp r - 1)"
using r_pos by (intro mult_strict_left_mono) auto
also have "… = ε"
using exp_r by (simp add: field_simps)
finally show ?thesis .
qed
with lim_le_C have "dist (prod g X) (infprod g A) < ε" by linarith
thus "dist (∏x∈X. 1 + f x y) (∏⇩∞x∈A. 1 + f x y) < ε"
unfolding g_def by simp
qed
qed
qed
lemma uniform_limit_prodinf':
fixes f :: "'k ⇒ 'a :: topological_space ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach, semidom, topological_semigroup_mult, t2_space}"
assumes conv_sum: "uniform_limit B (λX y. ∑x∈X. norm (f x y - 1)) L (finite_subsets_at_top A)"
assumes bdd: "⋀y. y ∈ B ⟹ L y ≤ C"
shows "uniform_limit B (λX y. ∏x∈X. f x y) (λy. ∏⇩∞x∈A. f x y) (finite_subsets_at_top A)"
proof -
have "uniform_limit B (λX y. ∏x∈X. 1 + (f x y - 1)) (λy. ∏⇩∞x∈A. 1 + (f x y - 1)) (finite_subsets_at_top A)"
by (rule uniform_limit_prodinf[where L = L and C = C]) (use assms in auto)
then show ?thesis
by simp
qed
text ‹
❙‹The Weierstrass ‹M›-test for unordered products›, and the form to use in practice: a
dominating summable \<^term>‹M› is all one has to produce. No continuity, no compactness, and no
uniform-convergence hypothesis -- ‹uniform_limit_infsum_M_test› supplies the latter and the
bound \<^term>‹∑⇩∞k∈A. M k› the former. This is the shape in which Weierstrass products arise: on
a compact set one bounds \<^term>‹norm (f k z - 1)› by a summable sequence independent of \<^term>‹z›.
Feeding it to ‹logderiv_infprod_uniform_limit› gives the logarithmic derivative as a uniformly
convergent sum.
›
corollary uniform_limit_infprod_M_test:
fixes f :: "'k ⇒ 'a :: topological_space ⇒ 'b :: {real_normed_div_algebra, comm_ring_1, banach, semidom, topological_semigroup_mult, t2_space}"
assumes le: "⋀k y. k ∈ A ⟹ y ∈ B ⟹ norm (f k y - 1) ≤ M k"
and M: "M summable_on A"
shows "uniform_limit B (λX y. ∏k∈X. f k y) (λy. ∏⇩∞k∈A. f k y) (finite_subsets_at_top A)"
proof (rule uniform_limit_prodinf'[where L = "λy. ∑⇩∞k∈A. norm (f k y - 1)"
and C = "∑⇩∞k∈A. M k"])
show "uniform_limit B (λX y. ∑k∈X. norm (f k y - 1))
(λy. ∑⇩∞k∈A. norm (f k y - 1)) (finite_subsets_at_top A)"
proof (rule uniform_limit_infsum_M_test[where h = "λk y. norm (f k y - 1)" and M = M])
show "⋀k y. k ∈ A ⟹ y ∈ B ⟹ norm (f k y - 1) ≤ M k"
using le by blast
show "⋀k y. k ∈ A ⟹ y ∈ B ⟹ 0 ≤ norm (f k y - 1)"
by simp
show "M summable_on A"
by (rule M)
qed
show "(∑⇩∞k∈A. norm (f k y - 1)) ≤ (∑⇩∞k∈A. M k)" if y: "y ∈ B" for y
proof (intro M infsum_mono)
show "(λk. norm (f k y - 1)) summable_on A"
using M le summable_on_comparison_test y by fastforce
show "⋀k. k ∈ A ⟹ norm (f k y - 1) ≤ M k"
using le y by blast
qed
qed
text ‹
The bridge to the sequential theory. A uniform limit along
\<^term>‹finite_subsets_at_top (UNIV :: nat set)› specialises to a uniform limit over the initial
segments. For the logarithmic derivative of a
Weierstrass product the detour is no longer needed: ‹uniform_limit_prodinf'› feeds
‹logderiv_infprod_uniform_limit› above directly, both being stated along
\<^term>‹finite_subsets_at_top A›.
›
corollary uniform_limit_prod_lessThan:
fixes f :: "nat ⇒ 'a ⇒ 'b :: {metric_space, comm_monoid_mult}"
assumes "uniform_limit B (λX y. ∏x∈X. f x y) P (finite_subsets_at_top UNIV)"
shows "uniform_limit B (λn y. ∏k<n. f k y) P sequentially"
using assms filterlim_lessThan_at_top by (rule filterlim_compose)
subsection ‹Real numbers›
text ‹Most lemmas in the general property section already apply to real numbers.
A few ones that are specific to reals are given here.›
lemma strongly_multipliable_on_iff_abs_multipliable_on_real:
fixes f :: ‹'a ⇒ real›
shows ‹f strongly_multipliable_on A ⟷ f abs_multipliable_on A›
proof
assume *: "f strongly_multipliable_on A"
then obtain B where B: "B ⊆ A" "finite B" "⋀x. x ∈ A-B ⟹ f x ∈ {0<..}"
using strongly_multipliable_on_imp_nhds_1[OF *, of "{0<..}"] by auto
have "f strongly_multipliable_on (A - B)"
by (rule strongly_multipliable_on_Diff_finite) fact+
moreover from B(3) have "f x ≠ 0" if "x ∈ A - B" for x
using that by force
ultimately obtain P where P: "(f has_setprod P) (A - B)" "P ≠ 0"
by (subst (asm) strongly_multipliable_on_nonzero_iff) auto
from P have "((λx. ln (f x)) has_sum ln P) (A - B)"
by (intro has_prod_imp_sums_ln_real)
hence "(λx. ln (f x)) summable_on (A - B)"
using has_sum_imp_summable by blast
hence "(λx. ln (f x)) abs_summable_on (A - B)"
by (subst (asm) summable_on_iff_abs_summable_on_real)
hence "(λx. exp (ln (f x))) abs_multipliable_on (A - B)"
by (intro abs_multipliable_on_exp)
also have "?this ⟷ f abs_multipliable_on (A - B)"
by (intro abs_multipliable_on_cong) (use B in auto)
finally have "f abs_multipliable_on (A - B ∪ B)"
by (intro abs_multipliable_on_Un_disjoint) (use B in auto)
also have "A - B ∪ B = A"
using B by auto
finally show "f abs_multipliable_on A" .
qed (use abs_multipliable_on_imp_strongly_multipliable_on in blast)
subsection ‹Complex numbers›
text ‹
A criterion that is useful when one controls the finite ∗‹partial sums› rather than the
individual summands: if all of them are bounded, the family is absolutely summable. Splitting
a finite subset according to the sign of ‹g› turns a bound on \<^term>‹¦sum g D¦› into a bound
on \<^term>‹sum (λx. ¦g x¦) D›, and then ‹nonneg_bdd_above_summable_on› applies.
›
lemma sum_abs_le_of_bdd_partial_sums:
fixes g :: "'a ⇒ real"
assumes bdd: "⋀E. finite E ⟹ E ⊆ A ⟹ ¦sum g E¦ ≤ C"
assumes D: "finite D" "D ⊆ A"
shows "(∑x∈D. ¦g x¦) ≤ 2 * C"
proof -
define P where "P = {x ∈ D. g x ≥ 0}"
have PD: "P ⊆ D" and Pfin: "finite P"
using D by (auto simp: P_def)
have e1: "(∑x∈P. ¦g x¦) = sum g P"
by (intro sum.cong refl) (auto simp: P_def)
have "(∑x∈D-P. ¦g x¦) = (∑x∈D-P. - g x)"
by (intro sum.cong refl) (auto simp: P_def)
then have e2: "(∑x∈D-P. ¦g x¦) = - sum g (D - P)"
by (simp add: sum_negf)
have DPA: "D - P ⊆ A" and PA: "P ⊆ A"
using D(2) PD by auto
have f1: "finite (D - P)"
using D(1) by simp
have b1: "- sum g (D - P) ≤ C"
using bdd[OF f1 DPA] by (simp add: abs_le_iff)
have b2: "sum g P ≤ C"
using bdd[OF Pfin PA] by (simp add: abs_le_iff)
have "(∑x∈D. ¦g x¦) = (∑x∈D-P. ¦g x¦) + (∑x∈P. ¦g x¦)"
using PD D(1) by (rule sum.subset_diff)
also have "… = - sum g (D - P) + sum g P"
by (simp add: e1 e2)
also have "… ≤ 2 * C"
using b1 b2 by linarith
finally show ?thesis .
qed
lemma abs_summable_on_real_of_bdd_partial_sums:
fixes g :: "'a ⇒ real"
assumes bdd: "⋀D. finite D ⟹ D ⊆ A ⟹ ¦sum g D¦ ≤ C"
shows "g abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on)
show "⋀x. x ∈ A ⟹ 0 ≤ norm (g x)"
by simp
show "bdd_above (sum (λx. norm (g x)) ` {D. D ⊆ A ∧ finite D})"
using sum_abs_le_of_bdd_partial_sums[OF bdd]
by fastforce
qed
lemma abs_summable_on_of_bdd_partial_sums:
fixes g :: "'a ⇒ complex"
assumes bdd: "⋀D. finite D ⟹ D ⊆ A ⟹ norm (sum g D) ≤ C"
shows "g abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on)
show "⋀x. x ∈ A ⟹ 0 ≤ norm (g x)"
by simp
show "bdd_above (sum (λx. norm (g x)) ` {D. D ⊆ A ∧ finite D})"
proof (rule bdd_aboveI2)
fix D assume "D ∈ {D. D ⊆ A ∧ finite D}"
then have D: "finite D" "D ⊆ A" by auto
have re: "¦sum (λx. Re (g x)) E¦ ≤ C" if "finite E" "E ⊆ A" for E
using bdd[OF that] abs_Re_le_cmod[of "sum g E"] by simp
have im: "¦sum (λx. Im (g x)) E¦ ≤ C" if "finite E" "E ⊆ A" for E
using bdd[OF that] abs_Im_le_cmod[of "sum g E"] by simp
have "(∑x∈D. norm (g x)) ≤ (∑x∈D. ¦Re (g x)¦ + ¦Im (g x)¦)"
by (intro sum_mono cmod_le)
also have "… = (∑x∈D. ¦Re (g x)¦) + (∑x∈D. ¦Im (g x)¦)"
by (rule sum.distrib)
also have "… ≤ 2 * C + 2 * C"
using sum_abs_le_of_bdd_partial_sums[OF re D] sum_abs_le_of_bdd_partial_sums[OF im D]
by simp
finally show "(∑x∈D. norm (g x)) ≤ 4 * C"
by simp
qed
qed
text ‹
❙‹The logarithm of an unordered product.› There is no unconditional complex analogue of
‹has_prod_imp_sums_ln_real›: ‹((λx. Ln (f x)) has_sum Ln P) A› already fails on a two-element
index set. Take \<^term>‹A = {1, 2 :: nat}› and \<^term>‹f = (λ_. -1 :: complex)›; then
\<^term>‹P = (1 :: complex)› is non-zero with \<^term>‹Ln P = 0›, whereas
\<^term>‹Ln (-1 :: complex) = 𝗂 * pi› and the sum is \<^term>‹2 * 𝗂 * pi›. Factors far from ‹1› wrap the
branch.
What is true is the statement under a hypothesis that rules the wrapping out, and every product
with a non-zero value satisfies that hypothesis once a finite set of factors is removed. The
first lemma isolates the additivity of ‹Ln›, which was previously buried in the proof of
‹strongly_multipliable_on_iff_abs_multipliable_on_complex› below.
›
lemma Ln_prod_of_prods_near_1:
fixes f :: "'a ⇒ complex"
assumes near: "⋀E. finite E ⟹ E ⊆ S ⟹ norm (prod f E - 1) < 1/2"
and D: "finite D" "D ⊆ S"
shows "Ln (prod f D) = (∑x∈D. Ln (f x))"
proof -
have Repos: "Re (prod f E) > 0" if E: "finite E" "E ⊆ S" for E
proof -
have "¦Re (prod f E - 1)¦ ≤ norm (prod f E - 1)"
by (rule abs_Re_le_cmod)
with near[OF E] show ?thesis
by simp
qed
have prod_nz: "prod f E ≠ 0" if "finite E" "E ⊆ S" for E
using Repos[OF that] by auto
have nzS: "f x ≠ 0" if "x ∈ S" for x
using prod_nz[of "{x}"] that by simp
have ImLn: "¦Im (Ln (prod f E))¦ < pi/2" if "finite E" "E ⊆ S" for E
using Repos[OF that] by (rule Re_Ln_pos_lt_imp)
have Ln_prod: "Ln (prod f E) = (∑x∈E. Ln (f x))" if "finite E" "E ⊆ S" for E
using that
proof (induction E rule: finite_induct)
case empty
show ?case by simp
next
case (insert a E)
from insert.prems have aS: "a ∈ S" and ES: "E ⊆ S" by auto
have IH: "Ln (prod f E) = (∑x∈E. Ln (f x))"
using insert.IH ES by blast
have b1: "- (pi/2) < Im (Ln (f a))" "Im (Ln (f a)) < pi/2"
using ImLn[of "{a}"] aS by (auto simp: abs_less_iff)
have b2: "- (pi/2) < Im (Ln (prod f E))" "Im (Ln (prod f E)) < pi/2"
using ImLn[of E] insert.hyps(1) ES by (auto simp: abs_less_iff)
have "Ln (prod f (insert a E)) = Ln (f a * prod f E)"
using insert.hyps by simp
also have "… = Ln (f a) + Ln (prod f E)"
proof (rule Ln_times_simple)
show "f a ≠ 0" using aS by (rule nzS)
show "prod f E ≠ 0" using insert.hyps(1) ES by (rule prod_nz)
show "- pi < Im (Ln (f a)) + Im (Ln (prod f E))"
using b1 b2 by linarith
show "Im (Ln (f a)) + Im (Ln (prod f E)) ≤ pi"
using b1 b2 by linarith
qed
also have "… = (∑x∈insert a E. Ln (f x))"
using insert.hyps IH by simp
finally show ?case .
qed
show ?thesis
using D by (rule Ln_prod)
qed
text ‹
With additivity available, the logarithm of the product is the sum of the logarithms: the partial
sums are literally \<^term>‹Ln (prod f X)›, and the limit is off the branch cut because the closed
ball \<^term>‹cball (1::complex) (1/2)› is, so ‹tendsto_Ln› applies.
›
lemma has_sum_Ln_of_prods_near_1:
fixes f :: "'a ⇒ complex"
assumes P: "(f has_setprod P) A"
and near: "⋀D. finite D ⟹ D ⊆ A ⟹ norm (prod f D - 1) < 1/2"
shows "((λx. Ln (f x)) has_sum Ln P) A"
proof -
have lim: "(prod f ⤏ P) (finite_subsets_at_top A)"
using P by (simp add: has_setprod_def)
have "P ∈ cball 1 (1/2)"
proof (rule Lim_in_closed_set[OF closed_cball _ _ lim])
show "∀⇩F X in finite_subsets_at_top A. prod f X ∈ cball 1 (1/2)"
proof (intro eventually_finite_subsets_at_top_weakI)
fix X assume X: "finite X" "X ⊆ A"
have "norm (prod f X - 1) < 1/2"
by (rule near[OF X])
thus "prod f X ∈ cball 1 (1/2)"
by (simp add: dist_norm norm_minus_commute)
qed
qed auto
hence "norm (P - 1) ≤ 1/2"
by (simp add: dist_norm norm_minus_commute)
hence ReP: "Re P > 0"
using abs_Re_le_cmod[of "P - 1"] by simp
hence "P ∉ ℝ⇩≤⇩0"
by (auto simp: complex_nonpos_Reals_iff)
have "((λX. Ln (prod f X)) ⤏ Ln P) (finite_subsets_at_top A)"
by (rule tendsto_Ln[OF lim]) fact
also have "?this ⟷ (sum (λx. Ln (f x)) ⤏ Ln P) (finite_subsets_at_top A)"
proof (intro filterlim_cong)
have "∀⇩F X in finite_subsets_at_top A. X ⊆ A ∧ finite X"
by (rule eventually_finite_subsets_at_top_weakI) auto
thus "∀⇩F X in finite_subsets_at_top A. Ln (prod f X) = (∑x∈X. Ln (f x))"
by eventually_elim (use Ln_prod_of_prods_near_1[OF near] in blast)
qed auto
finally show ?thesis
unfolding has_sum_def .
qed
text ‹
The general form: for a product with a non-zero value the logarithms are summable, and sum to the
logarithm of the product, after removing finitely many factors. As the counterexample above
shows, the finite exceptional set cannot be dispensed with.
›
corollary has_sum_Ln_of_has_setprod_complex:
fixes f :: "'a ⇒ complex"
assumes P: "(f has_setprod P) A" and nz: "P ≠ 0"
shows "∃F. finite F ∧ F ⊆ A ∧
((λx. Ln (f x)) has_sum Ln (∏⇩∞x∈A-F. f x)) (A - F)"
proof -
have lim: "(prod f ⤏ P) (finite_subsets_at_top A)"
using P by (simp add: has_setprod_def)
have half: "(1/2::real) > 0"
by simp
obtain F where F: "finite F" "F ⊆ A"
and near: "⋀D. finite D ⟹ D ⊆ A - F ⟹ dist (prod f D) 1 < 1/2"
using has_setprod_prods_near_1[OF lim nz half] by blast
obtain Q where Q: "(f has_setprod Q) (A - F)" "Q ≠ 0"
using has_setprod_subset_nonzero[OF P nz Diff_subset] by blast
have Qeq: "(∏⇩∞x∈A-F. f x) = Q"
by (rule infprodI[OF Q(1)])
have sum: "((λx. Ln (f x)) has_sum Ln Q) (A - F)"
by (rule has_sum_Ln_of_prods_near_1[OF Q(1)]) (use near in ‹simp add: dist_norm›)
show ?thesis
using F Qeq sum by blast
qed
text ‹
The complex analogue of ‹strongly_multipliable_on_iff_abs_multipliable_on_real›. The
difficulty anticipated in the original note -- that \<^term>‹∑x. Ln (f x)› might cross branch
cuts, with an ill-defined winding count for an unordered index set -- does not in fact arise.
A non-zero product forces every finite subproduct outside a suitable finite set to lie within
‹1/2› of ‹1›, and ‹Ln_prod_of_prods_near_1› above turns that into exact additivity of ‹Ln›. The
resulting partial sums of \<^term>‹Ln ∘ f› are then bounded by ‹norm_Ln_le›, which gives absolute
summability and hence absolute multipliability.
›
lemma strongly_multipliable_on_iff_abs_multipliable_on_complex:
fixes f :: ‹'a ⇒ complex›
shows ‹f strongly_multipliable_on A ⟷ f abs_multipliable_on A›
proof
assume *: "f strongly_multipliable_on A"
define A0 where "A0 = {x ∈ A. f x ≠ 0}"
from * obtain P where P: "finite {x∈A. f x = 0}" "(f has_setprod P) A0" "P ≠ 0"
unfolding strongly_multipliable_on_def A0_def by blast
have limA0: "(prod f ⤏ P) (finite_subsets_at_top A0)"
using P(2) by (simp add: has_setprod_def)
have half: "(1/2::real) > 0"
by simp
obtain F where F: "finite F" "F ⊆ A0"
and near: "⋀D. finite D ⟹ D ⊆ A0 - F ⟹ dist (prod f D) 1 < 1/2"
using has_setprod_prods_near_1[OF limA0 P(3) half] by blast
define S where "S = A0 - F"
have SA: "S ⊆ A"
by (auto simp: S_def A0_def)
have nzS: "f x ≠ 0" if "x ∈ S" for x
using that by (auto simp: S_def A0_def)
have near': "norm (prod f D - 1) < 1/2" if "finite D" "D ⊆ S" for D
using near[of D] that by (simp add: S_def dist_norm)
have Ln_prod: "Ln (prod f D) = (∑x∈D. Ln (f x))" if "finite D" "D ⊆ S" for D
by (rule Ln_prod_of_prods_near_1[OF near' that])
have bdd: "norm (∑x∈D. Ln (f x)) ≤ 1" if D: "finite D" "D ⊆ S" for D
proof -
have eq: "(∑x∈D. Ln (f x)) = Ln (1 + (prod f D - 1))"
using Ln_prod[OF D] by simp
have "norm (Ln (1 + (prod f D - 1))) ≤ 2 * norm (prod f D - 1)"
by (rule norm_Ln_le) (use near'[OF D] in simp)
also have "… ≤ 1"
using near'[OF D] by simp
finally show ?thesis
using eq by simp
qed
have "(λx. Ln (f x)) abs_summable_on S"
by (rule abs_summable_on_of_bdd_partial_sums[where C = 1]) (use bdd in auto)
hence "(λx. exp (Ln (f x))) abs_multipliable_on S"
by (intro abs_multipliable_on_exp)
also have "?this ⟷ f abs_multipliable_on S"
by (intro abs_multipliable_on_cong) (use nzS in auto)
finally have S: "f abs_multipliable_on S" .
have "A - S ⊆ {x∈A. f x = 0} ∪ F"
by (auto simp: S_def A0_def)
hence finAS: "finite (A - S)"
using P(1) F(1) by (auto elim: finite_subset)
have "f abs_multipliable_on (S ∪ (A - S))"
using S abs_multipliable_on_finite[OF finAS] by (intro abs_multipliable_on_Un_disjoint) auto
also have "S ∪ (A - S) = A"
using SA by auto
finally show "f abs_multipliable_on A" .
qed (use abs_multipliable_on_imp_strongly_multipliable_on in blast)
text ‹
A striking consequence, for real and for complex families: an unordered product whose value is
non-zero converges ∗‹absolutely›. So for these types there is no distinction between
unconditional and absolute convergence of products once the value ‹0› is excluded -- the exact
analogue of the corresponding fact for sums.
›
corollary multipliable_on_imp_abs_multipliable_on_complex:
fixes f :: "'a ⇒ complex"
assumes mult: "f multipliable_on A" and nz: "infprod f A ≠ 0"
shows "f abs_multipliable_on A"
proof -
have P: "(f has_setprod infprod f A) A"
using mult by (rule has_setprod_infprod)
have nzf: "f x ≠ 0" if "x ∈ A" for x
using nz that by (meson infprodI zero_imp_has_setprod_0)
have empty: "{x ∈ A. f x = 0} = {}"
using nzf by blast
have all: "{x ∈ A. f x ≠ 0} = A"
using nzf by blast
have "f strongly_multipliable_on A"
using P nz nzf strongly_multipliable_on_nonzero_iff by blast
thus ?thesis
by (simp add: strongly_multipliable_on_iff_abs_multipliable_on_complex)
qed
corollary multipliable_on_imp_abs_multipliable_on_real:
fixes f :: "'a ⇒ real"
assumes mult: "f multipliable_on A" and nz: "infprod f A ≠ 0"
shows "f abs_multipliable_on A"
proof -
have P: "(f has_setprod infprod f A) A"
using mult by (rule has_setprod_infprod)
have nzf: "f x ≠ 0" if "x ∈ A" for x
using nz that by (meson infprodI zero_imp_has_setprod_0)
have empty: "{x ∈ A. f x = 0} = {}"
using nzf by blast
have all: "{x ∈ A. f x ≠ 0} = A"
using nzf by blast
have "f strongly_multipliable_on A"
using P nz nzf strongly_multipliable_on_nonzero_iff by blast
thus ?thesis
by (simp add: strongly_multipliable_on_iff_abs_multipliable_on_real)
qed
lemma has_setprod_cnj_iff[simp]:
fixes f :: ‹'a ⇒ complex›
shows ‹((λx. cnj (f x)) has_setprod cnj a) M ⟷ (f has_setprod a) M›
using lim_cnj by (fastforce simp add: has_setprod_def)
lemma multipliable_on_cnj_iff[simp]:
"(λi. cnj (f i)) multipliable_on A ⟷ f multipliable_on A"
by (metis complex_cnj_cnj multipliable_on_def has_setprod_cnj_iff)
lemma infprod_cnj[simp]: ‹infprod (λx. cnj (f x)) M = cnj (infprod f M)›
by (metis complex_cnj_one has_setprod_cnj_iff has_setprod_infprod infprodI
infprod_not_exists multipliable_on_cnj_iff)
lemma has_setprod_Re:
assumes "(f has_setprod a) M" and real: "⋀x. x ∈ M ⟹ f x ∈ ℝ"
shows "((λx. Re (f x)) has_setprod Re a) M"
proof -
have eq: "∀⇩F X in finite_subsets_at_top M. prod (λx. Re (f x)) X = Re (prod f X)"
by (simp add: Re_prod_Reals eventually_finite_subsets_at_top_weakI real subsetD)
from assms(1) have "((λX. Re (prod f X)) ⤏ Re a) (finite_subsets_at_top M)"
by (simp add: has_setprodD tendsto_Re)
then show ?thesis
using eq unfolding has_setprod_def by (simp add: filterlim_cong)
qed
lemma infprod_Re:
assumes "f multipliable_on M" and "⋀x. x ∈ M ⟹ f x ∈ ℝ"
shows "infprod (λx. Re (f x)) M = Re (infprod f M)"
by (simp add: assms has_setprod_Re infprodI)
lemma multipliable_on_Re:
assumes "f multipliable_on M" and "⋀x. x ∈ M ⟹ f x ∈ ℝ"
shows "(λx. Re (f x)) multipliable_on M"
by (metis assms has_setprod_Re multipliable_on_def)
lemma has_setprod_Im:
assumes "(f has_setprod a) M" and real: "⋀x. x ∈ M ⟹ f x ∈ ℝ" and "M ≠ {}"
shows "((λx. Im (f x)) has_setprod Im a) M"
proof -
from ‹M ≠ {}› obtain m where "m ∈ M" by blast
have eq: "∀⇩F X in finite_subsets_at_top M. prod (λx. Im (f x)) X = Im (prod f X)"
unfolding eventually_finite_subsets_at_top
proof (intro exI conjI allI impI)
show "finite {m}" "{m} ⊆ M" using ‹m ∈ M› by auto
next
fix X assume "finite X ∧ {m} ⊆ X ∧ X ⊆ M"
then have "finite X" "X ⊆ M" "X ≠ {}" by auto
have "Im (f x) = 0" if "x ∈ X" for x
using real ‹X ⊆ M› that by (auto simp: complex_is_Real_iff subset_iff)
then have "prod (λx. Im (f x)) X = prod (λx. (0::real)) X"
by (intro prod.cong) auto
also have "… = 0"
using ‹finite X› ‹X ≠ {}› by (intro prod_zero) auto
finally have lhs: "prod (λx. Im (f x)) X = 0" .
have "prod f X ∈ ℝ"
using real ‹X ⊆ M› by (intro prod_in_Reals) (auto simp: subset_iff)
then have "Im (prod f X) = 0"
by (simp add: complex_is_Real_iff)
with lhs show "prod (λx. Im (f x)) X = Im (prod f X)" by simp
qed
from assms(1) have "(prod f ⤏ a) (finite_subsets_at_top M)"
by (simp add: has_setprod_def)
then have "((λX. Im (prod f X)) ⤏ Im a) (finite_subsets_at_top M)"
by (rule tendsto_Im)
then show ?thesis
unfolding has_setprod_def using eq tendsto_cong by fastforce
qed
lemma infprod_Im:
assumes "f multipliable_on M" and "⋀x. x ∈ M ⟹ f x ∈ ℝ" and "M ≠ {}"
shows "infprod (λx. Im (f x)) M = Im (infprod f M)"
by (simp add: assms has_setprod_Im infprodI)
lemma multipliable_on_Im:
assumes "f multipliable_on M" and "⋀x. x ∈ M ⟹ f x ∈ ℝ" and "M ≠ {}"
shows "(λx. Im (f x)) multipliable_on M"
by (metis assms has_setprod_Im multipliable_on_def)
end