Theory Misc_Tensor_Product

section ‹‹Misc_Tensor_Product› -- Miscelleanous results missing from other theories›

theory Misc_Tensor_Product
  imports "HOL-Analysis.Elementary_Topology" "HOL-Analysis.Abstract_Topology"
    "HOL-Analysis.Abstract_Limits" "HOL-Analysis.Function_Topology" "HOL-Cardinals.Cardinals"
    "HOL-Analysis.Infinite_Sum" "HOL-Analysis.Harmonic_Numbers" Containers.Containers_Auxiliary
    Complex_Bounded_Operators.Extra_General
    Complex_Bounded_Operators.Extra_Vector_Spaces
    Complex_Bounded_Operators.Extra_Ordered_Fields
begin

unbundle lattice_syntax

lemma local_defE: "(⋀x. x=y ⟹ P) ⟹ P" by metis
    ― ‹A helper lemma to introduce a local ``definition`` in the current goal when backwards reasoning.
        ‹apply (rule local_defE[where x=‹stuff›])› will insert \<^term>‹x=stuff› as a premise.
        This can be useful before using ‹apply transfer› because it will introduce some 
        additional knowledge about the properties of \<^term>‹x› into the transferred goal.›

lemma inv_prod_swap[simp]: ‹inv prod.swap = prod.swap›
  by (simp add: inv_unique_comp)

lemma filterlim_parametric[transfer_rule]: 
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique S›
  shows ‹((R ===> S) ===> rel_filter S ===> rel_filter R ===> (=)) filterlim filterlim›
  using filtermap_parametric[transfer_rule] le_filter_parametric[transfer_rule] apply fail?
  unfolding filterlim_def
  by transfer_prover


definition rel_topology :: ‹('a ⇒ 'b ⇒ bool) ⇒ ('a topology ⇒ 'b topology ⇒ bool)› where
  ‹rel_topology R S T ⟷ (rel_fun (rel_set R) (=)) (openin S) (openin T)
 ∧ (∀U. openin S U ⟶ Domainp (rel_set R) U) ∧ (∀U. openin T U ⟶ Rangep (rel_set R) U)›

lemma rel_topology_eq[relator_eq]: ‹rel_topology (=) = (=)›
  unfolding rel_topology_def using openin_inject
  by (auto simp: rel_fun_eq rel_set_eq fun_eq_iff)

lemma Rangep_conversep[simp]: ‹Rangep (R¯¯) = Domainp R›
  by blast

lemma Domainp_conversep[simp]: ‹Domainp (R¯¯) = Rangep R›
  by blast

lemma conversep_rel_fun:
  includes lifting_syntax
  shows ‹(T ===> U)¯¯ = (T¯¯) ===> (U¯¯)›
  by (auto simp: rel_fun_def)

lemma rel_topology_conversep[simp]: ‹rel_topology (R¯¯) = ((rel_topology R)¯¯)›
  by (auto simp add: rel_topology_def[abs_def] simp flip: conversep_rel_fun[where U=‹(=)›, simplified])

lemma openin_parametric[transfer_rule]:
  includes lifting_syntax
  shows ‹(rel_topology R ===> rel_set R ===> (=)) openin openin›
  by (auto simp add: rel_fun_def rel_topology_def)

lemma topspace_parametric [transfer_rule]:
  includes lifting_syntax
  shows ‹(rel_topology R ===> rel_set R) topspace topspace›
proof -
  have *: ‹∃y∈topspace T'. R x y› if ‹rel_topology R T T'› ‹x ∈ topspace T› for x T T' and R :: ‹'q ⇒ 'r ⇒ bool›
  proof -
    from that obtain U where ‹openin T U› and ‹x ∈ U›
      unfolding topspace_def
      by auto
    from ‹openin T U›
    have ‹Domainp (rel_set R) U›
      using ‹rel_topology R T T'› rel_topology_def by blast
    then obtain V where [transfer_rule]: ‹rel_set R U V›
      by blast
    with ‹x ∈ U› obtain y where ‹R x y› and ‹y ∈ V›
      by (meson rel_set_def)
    from ‹rel_set R U V› ‹rel_topology R T T'› ‹openin T U›
    have ‹openin T' V›
      by (simp add: rel_topology_def rel_fun_def)
    with ‹y ∈ V› have ‹y ∈ topspace T'›
      using openin_subset by auto
    with ‹R x y› show ‹∃y∈topspace T'. R x y›
      by auto
  qed

  show ?thesis
    using *[where ?R.1=R]
    using *[where ?R.1=‹R¯¯›]
    by (auto intro!: rel_setI)
qed

lemma [transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_total S›
  assumes [transfer_rule]: ‹bi_unique S›
  assumes [transfer_rule]: ‹bi_total R›
  assumes [transfer_rule]: ‹bi_unique R›
  shows ‹(rel_topology R ===> rel_topology S ===> (R ===> S) ===> (=)) continuous_map continuous_map›
  unfolding continuous_map_def Pi_def
  by transfer_prover


lemma limitin_closedin:
  assumes ‹limitin T f c F›
  assumes ‹range f ⊆ S›
  assumes ‹closedin T S›
  assumes ‹¬ trivial_limit F›
  shows ‹c ∈ S›
proof -
  from assms have ‹T closure_of S = S›
    by (simp add: closure_of_eq)
  moreover have ‹c ∈ T closure_of S›
    using assms(1) _ assms(4) apply (rule limitin_closure_of)
    using range_subsetD[OF assms(2)] by auto
  ultimately show ?thesis
    by simp
qed


lemma closure_nhds_principal: ‹a ∈ closure A ⟷ inf (nhds a) (principal A) ≠ bot›
proof (rule iffI)
  show ‹inf (nhds a) (principal A) ≠ bot› if ‹a ∈ closure A›
  proof (cases ‹a ∈ A›)
    case True
    thus ?thesis
      unfolding filter_eq_iff eventually_inf eventually_principal eventually_nhds by force
  next
    case False
    have "at a within A ≠ bot"
      using False that by (subst at_within_eq_bot_iff) auto
    also have "at a within A = inf (nhds a) (principal A)"
      using False by (simp add: at_within_def)
    finally show ?thesis .
  qed
  show ‹a ∈ closure A› if ‹inf (nhds a) (principal A) ≠ bot›
    by (metis Diff_empty Diff_insert0 at_within_def closure_subset not_in_closure_trivial_limitI subsetD that)
qed


lemma limit_in_closure:
  assumes lim: ‹(f ⤏ x) F›
  assumes nt: ‹F ≠ bot›
  assumes inA: ‹∀⇩F x in F. f x ∈ A›
  shows ‹x ∈ closure A›
proof (rule Lim_in_closed_set[of _ _ F])
  show "∀⇩F x in F. f x ∈ closure A"
    using inA by eventually_elim (use closure_subset in blast)
qed (use assms in auto)

lemma filterlim_nhdsin_iff_limitin:
  ‹l ∈ topspace T ∧ filterlim f (nhdsin T l) F ⟷ limitin T f l F›
  unfolding limitin_def
proof safe
  fix U assume *: "l ∈ topspace T" "filterlim f (nhdsin T l) F" "openin T U" "l ∈ U"
  hence "eventually (λy. y ∈ U) (nhdsin T l)"
    unfolding eventually_nhdsin by blast
  thus "eventually (λx. f x ∈ U) F"
    using *(2) eventually_compose_filterlim by blast
next
  assume *: "l ∈ topspace T" "∀U. openin T U ∧ l ∈ U ⟶ (∀⇩F x in F. f x ∈ U)"
  show "filterlim f (nhdsin T l) F"
    unfolding filterlim_def le_filter_def eventually_filtermap
  proof safe
    fix P :: "'a ⇒ bool"
    assume "eventually P (nhdsin T l)"
    then obtain U where U: "openin T U" "l ∈ U" "∀x∈U. P x"
      using *(1) unfolding eventually_nhdsin by blast
    with * have "eventually (λx. f x ∈ U) F"
      by blast
    thus "eventually (λx. P (f x)) F"
      by eventually_elim (use U in blast)
  qed
qed

lemma pullback_topology_bi_cont: 
  fixes g :: ‹'a ⇒ ('b ⇒ 'c::topological_space)›
    and f :: ‹'a ⇒ 'a ⇒ 'a› and f' :: ‹'c ⇒ 'c ⇒ 'c›
  assumes gf_f'g: ‹⋀a b i. g (f a b) i = f' (g a i) (g b i)›
  assumes f'_cont: ‹⋀a' b'. (case_prod f' ⤏ f' a' b') (nhds a' ×⇩F nhds b')›
  defines ‹T ≡ pullback_topology UNIV g euclidean›
  shows ‹LIM (x,y) nhdsin T a ×⇩F nhdsin T b. f x y :> nhdsin T (f a b)›
proof -
  have topspace[simp]: ‹topspace T = UNIV›
    unfolding T_def topspace_pullback_topology by simp
  have openin: ‹openin T U ⟷ (∃V. open V ∧ U = g -` V)› for U
    by (simp add: assms openin_pullback_topology)

  have 1: ‹nhdsin T a = filtercomap g (nhds (g a))›
    for a :: 'a
    by (auto simp add: filter_eq_iff eventually_filtercomap eventually_nhds eventually_nhdsin openin)

  have ‹((g ∘ case_prod f) ⤏ g (f a b)) (nhdsin T a ×⇩F nhdsin T b)›
  proof (unfold tendsto_def, intro allI impI)
    fix S assume ‹open S› and gfS: ‹g (f a b) ∈ S›
    obtain U where gf_PiE: ‹g (f a b) ∈ Pi⇩E UNIV U› and openU: ‹∀i. openin euclidean (U i)›
      and finiteD: ‹finite {i. U i ≠ topspace euclidean}› and US: ‹Pi⇩E UNIV U ⊆ S›
      using product_topology_open_contains_basis[OF ‹open S›[unfolded open_fun_def] gfS]
      by auto

    define D where ‹D = {i. U i ≠ UNIV}›
    with finiteD have ‹finite D›
      by auto

    from openU have openU: ‹open (U i)› for i
      by auto

    have *: ‹f' (g a i) (g b i) ∈ U i› for i
      by (metis PiE_mem gf_PiE iso_tuple_UNIV_I gf_f'g)

    have ‹∀⇩F x in nhds (g a i) ×⇩F nhds (g b i). case_prod f' x ∈ U i› for i
      using tendsto_def[THEN iffD1, rule_format, OF f'_cont openU *, of i] by -

    then obtain Pa Pb where ‹eventually (Pa i) (nhds (g a i))› and ‹eventually (Pb i) (nhds (g b i))›
      and PaPb_plus: ‹(∀x y. Pa i x ⟶ Pb i y ⟶ f' x y ∈ U i)› for i
      unfolding eventually_prod_filter by (metis prod.simps(2))

    from ‹⋀i. eventually (Pa i) (nhds (g a i))›
    obtain Ua where ‹open (Ua i)› and a_Ua: ‹g a i ∈ Ua i› and Ua_Pa: ‹Ua i ⊆ Collect (Pa i)› for i
      unfolding eventually_nhds
      apply atomize_elim
      by (metis mem_Collect_eq subsetI)
    from ‹⋀i. eventually (Pb i) (nhds (g b i))›
    obtain Ub where ‹open (Ub i)› and b_Ub: ‹g b i ∈ Ub i› and Ub_Pb: ‹Ub i ⊆ Collect (Pb i)› for i
      unfolding eventually_nhds
      apply atomize_elim
      by (metis mem_Collect_eq subsetI)
    have UaUb_plus: ‹x ∈ Ua i ⟹ y ∈ Ub i ⟹ f' x y ∈ U i› for i x y
      by (metis PaPb_plus Ua_Pa Ub_Pb mem_Collect_eq subsetD)

    define Ua' where ‹Ua' i = (if i∈D then Ua i else UNIV)› for i
    define Ub' where ‹Ub' i = (if i∈D then Ub i else UNIV)› for i

    have Ua'_UNIV: ‹U i = UNIV ⟹ Ua' i = UNIV› for i
      by (simp add: D_def Ua'_def)
    have Ub'_UNIV: ‹U i = UNIV ⟹ Ub' i = UNIV› for i
      by (simp add: D_def Ub'_def)
    have [simp]: ‹open (Ua' i)› for i
      by (simp add: Ua'_def ‹open (Ua _)›)
    have [simp]: ‹open (Ub' i)› for i
      by (simp add: Ub'_def ‹open (Ub _)›)
    have a_Ua': ‹g a i ∈ Ua' i› for i
      by (simp add: Ua'_def a_Ua)
    have b_Ub': ‹g b i ∈ Ub' i› for i
      by (simp add: Ub'_def b_Ub)
    have UaUb'_plus: ‹a' ∈ Ua' i ⟹ b' ∈ Ub' i ⟹ f' a' b' ∈ U i› for i a' b'
      apply (cases ‹i ∈ D›)
      using UaUb_plus by (auto simp add: Ua'_def  Ub'_def D_def)

    define Ua'' where ‹Ua'' = Pi UNIV Ua'›
    define Ub'' where ‹Ub'' = Pi UNIV Ub'›

    have ‹open Ua''›
      using finiteD Ua'_UNIV
      by (auto simp add: open_fun_def Ua''_def PiE_UNIV_domain
            openin_product_topology_alt D_def intro!: exI[where x=‹Ua'›] intro: rev_finite_subset)
    have ‹open Ub''›
      using finiteD Ub'_UNIV
      by (auto simp add: open_fun_def Ub''_def PiE_UNIV_domain
            openin_product_topology_alt D_def intro!: exI[where x=‹Ub'›] intro: rev_finite_subset)
    have a_Ua'': ‹g a ∈ Ua''›
      by (simp add: Ua''_def a_Ua')
    have b_Ub'': ‹g b ∈ Ub''›
      by (simp add: Ub''_def b_Ub')
    have UaUb''_plus: ‹a' ∈ Ua'' ⟹ b' ∈ Ub'' ⟹ f' (a' i) (b' i) ∈ U i› for i a' b'
      using UaUb'_plus by (force simp add: Ua''_def  Ub''_def)

    define Ua''' where ‹Ua''' = g -` Ua''›
    define Ub''' where ‹Ub''' = g -` Ub''›
    have ‹openin T Ua'''›
      using ‹open Ua''› by (auto simp: openin Ua'''_def)
    have ‹openin T Ub'''›
      using ‹open Ub''› by (auto simp: openin Ub'''_def)
    have a_Ua'': ‹a ∈ Ua'''›
      by (simp add: Ua'''_def a_Ua'')
    have b_Ub'': ‹b ∈ Ub'''›
      by (simp add: Ub'''_def b_Ub'')
    have UaUb'''_plus: ‹a ∈ Ua''' ⟹ b ∈ Ub''' ⟹ f' (g a i) (g b i) ∈ U i› for i a b
      by (simp add: Ua'''_def UaUb''_plus Ub'''_def)

    define Pa' where ‹Pa' a ⟷ a ∈ Ua'''› for a
    define Pb' where ‹Pb' b ⟷ b ∈ Ub'''› for b

    have Pa'_nhd: ‹eventually Pa' (nhdsin T a)›
      using ‹openin T Ua'''›
      by (auto simp add: Pa'_def eventually_nhdsin intro!: exI[of _ ‹Ua'''›] a_Ua'')
    have Pb'_nhd: ‹eventually Pb' (nhdsin T b)›
      using ‹openin T Ub'''›
      by (auto simp add: Pb'_def eventually_nhdsin intro!: exI[of _ ‹Ub'''›] b_Ub'')
    have Pa'Pb'_plus: ‹(g ∘ case_prod f) (a, b) ∈ S› if ‹Pa' a› ‹Pb' b› for a b
      using that UaUb'''_plus US
      by (auto simp add: Pa'_def Pb'_def PiE_UNIV_domain Pi_iff gf_f'g)

    show ‹∀⇩F x in nhdsin T a ×⇩F nhdsin T b. (g ∘ case_prod f) x ∈ S›
      using Pa'_nhd Pb'_nhd Pa'Pb'_plus
      unfolding eventually_prod_filter
      apply -
      apply (rule exI[of _ Pa'])
      apply (rule exI[of _ Pb'])
      by simp
  qed
  then show ?thesis
    unfolding 1 filterlim_filtercomap_iff by -
qed

definition ‹has_sum_in T f A x ⟷ limitin T (sum f) x (finite_subsets_at_top A)›


lemma has_sum_in_finite:
  assumes "finite F"
  assumes ‹sum f F ∈ topspace T›
  shows "has_sum_in T f F (sum f F)"
  using assms
  by (simp add: finite_subsets_at_top_finite has_sum_in_def limitin_def eventually_principal)


definition ‹summable_on_in T f A ⟷ (∃x. has_sum_in T f A x)›

definition ‹infsum_in T f A = (let L = Collect (has_sum_in T f A) in if card L = 1 then the_elem L else 0)›
(* The reason why we return 0 also in the case that there are several solutions is to make sure infsum_in is parametric.
(See lemma 'infsum_in_parametric' below. *)

lemma hausdorff_OFCLASS_t2_space: ‹OFCLASS('a::topological_space, t2_space_class)› if ‹Hausdorff_space (euclidean :: 'a topology)›
proof intro_classes
  fix a b :: 'a
  assume ‹a ≠ b›
  from that
  show ‹∃U V. open U ∧ open V ∧ a ∈ U ∧ b ∈ V ∧ U ∩ V = {}›
    unfolding Hausdorff_space_def disjnt_def
    using ‹a ≠ b› by auto
qed

lemma hausdorffI: 
  assumes ‹⋀x y. x ∈ topspace T ⟹ y ∈ topspace T ⟹ x ≠ y ⟹ ∃U V. openin T U ∧ openin T V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}›
  shows ‹Hausdorff_space T›
  using assms by (auto simp: Hausdorff_space_def disjnt_def)

lemma hausdorff_euclidean[simp]: ‹Hausdorff_space (euclidean :: _::t2_space topology)›
  apply (rule hausdorffI)
  by (metis (mono_tags, lifting) hausdorff open_openin)

lemma has_sum_in_unique:
  assumes ‹Hausdorff_space T›
  assumes ‹has_sum_in T f A l›
  assumes ‹has_sum_in T f A l'›
  shows ‹l = l'›
  using assms(2,3)[unfolded has_sum_in_def] _ assms(1)
  apply (rule limitin_Hausdorff_unique)
  by simp

lemma infsum_in_def':
  assumes ‹Hausdorff_space T›
  shows ‹infsum_in T f A = (if summable_on_in T f A then (THE s. has_sum_in T f A s) else 0)›
proof (cases ‹Collect (has_sum_in T f A) = {}›)
  case True
  then show ?thesis using True
    by (auto simp: infsum_in_def summable_on_in_def Let_def card_1_singleton_iff)
next
  case False
  then have ‹summable_on_in T f A›
    by (metis (no_types, lifting) empty_Collect_eq summable_on_in_def)
  from False ‹Hausdorff_space T›
  have ‹card (Collect (has_sum_in T f A)) = 1›
    by (metis (mono_tags, opaque_lifting) has_sum_in_unique is_singletonI' is_singleton_altdef mem_Collect_eq)
  then show ?thesis
    using ‹summable_on_in T f A›
    by (smt (verit, best) assms card_1_singletonE has_sum_in_unique infsum_in_def mem_Collect_eq singletonI the_elem_eq the_equality)
qed

lemma has_sum_in_infsum_in: 
  assumes ‹Hausdorff_space T› and summable: ‹summable_on_in T f A›
  shows ‹has_sum_in T f A (infsum_in T f A)›
  apply (simp add: infsum_in_def'[OF ‹Hausdorff_space T›] summable)
  apply (rule theI'[of ‹has_sum_in T f A›])
  using has_sum_in_unique[OF ‹Hausdorff_space T›, of f A] summable
  by (meson summable_on_in_def)


lemma infsum_in_finite:
  assumes "finite F"
  assumes ‹Hausdorff_space T›
  assumes ‹sum f F ∈ topspace T›
  shows "infsum_in T f F = sum f F"
  using has_sum_in_finite[OF assms(1,3)]
  using assms(2) has_sum_in_infsum_in has_sum_in_unique summable_on_in_def by blast

lemma nhdsin_mono:
  assumes [simp]: ‹⋀x. openin T' x ⟹ openin T x›
  assumes [simp]: ‹topspace T = topspace T'›
  shows ‹nhdsin T a ≤ nhdsin T' a›
  unfolding nhdsin_def 
  by (auto intro!: INF_superset_mono)


lemma has_sum_in_cong: 
  assumes "⋀x. x∈A ⟹ f x = g x"
  shows "has_sum_in T f A x ⟷ has_sum_in T g A x"
proof -
  have ‹(∀⇩F x in finite_subsets_at_top A. sum f x ∈ U) ⟷ (∀⇩F x in finite_subsets_at_top A. sum g x ∈ U)› for U
    apply (rule eventually_subst)
    apply (subst eventually_finite_subsets_at_top)
    by (metis (mono_tags, lifting) assms empty_subsetI finite.emptyI subset_eq sum.cong)
  then show ?thesis
    by (simp add: has_sum_in_def limitin_def)
qed

lemma infsum_in_eqI':
  fixes f g :: ‹'a ⇒ 'b::comm_monoid_add›
  assumes ‹⋀x. has_sum_in T f A x ⟷ has_sum_in T g B x›
  shows ‹infsum_in T f A = infsum_in T g B›
  by (simp add: infsum_in_def assms[abs_def] summable_on_in_def)

lemma infsum_in_cong:
  assumes "⋀x. x∈A ⟹ f x = g x"
  shows "infsum_in T f A = infsum_in T g A"
  using assms infsum_in_eqI' has_sum_in_cong by blast

lemma limitin_cong: "limitin T f c F ⟷ limitin T g c F" if "eventually (λx. f x = g x) F"
  by (smt (verit, best) eventually_elim2 limitin_transform_eventually that)

lemma has_sum_in_reindex:
  assumes ‹inj_on h A›
  shows ‹has_sum_in T g (h ` A) x ⟷ has_sum_in T (g ∘ h) A x›
proof -
  have ‹has_sum_in T g (h ` A) x ⟷ limitin T (sum g) x (finite_subsets_at_top (h ` A))›
    by (simp add: has_sum_in_def)
  also have ‹… ⟷ limitin T (λF. sum g (h ` F)) x (finite_subsets_at_top A)›
    apply (subst filtermap_image_finite_subsets_at_top[symmetric])
    by (simp_all add: assms eventually_filtermap limitin_def)
  also have ‹… ⟷ limitin T (sum (g ∘ h)) x (finite_subsets_at_top A)›
    apply (rule limitin_cong)
    apply (rule eventually_finite_subsets_at_top_weakI)
    apply (rule sum.reindex)
    using assms inj_on_subset by blast
  also have ‹… ⟷ has_sum_in T (g ∘ h) A x›
    by (simp add: has_sum_in_def)
  finally show ?thesis .
qed

lemma summable_on_in_reindex:
  assumes ‹inj_on h A›
  shows ‹summable_on_in T g (h ` A) ⟷ summable_on_in T (g ∘ h) A›
  by (simp add: assms summable_on_in_def has_sum_in_reindex)

lemma infsum_in_reindex:
  assumes ‹inj_on h A›
  shows ‹infsum_in T g (h ` A) = infsum_in T (g ∘ h) A›
  by (metis Collect_cong assms has_sum_in_reindex infsum_in_def)

lemma has_sum_in_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "has_sum_in T (λx. f (g x)) A s ⟷ has_sum_in T f B s"
proof -
  have ‹has_sum_in T (λx. f (g x)) A s ⟷ has_sum_in T f (g ` A) s›
    by (metis (mono_tags, lifting) assms bij_betw_imp_inj_on has_sum_in_cong has_sum_in_reindex o_def)
  also have ‹… = has_sum_in T f B s›
    using assms bij_betw_imp_surj_on by blast
  finally show ?thesis .
qed


lemma has_sum_euclidean_iff: ‹has_sum_in euclidean f A s ⟷ (f has_sum s) A›
  by (simp add: has_sum_def has_sum_in_def)

lemma summable_on_euclidean_eq: ‹summable_on_in euclidean f A ⟷ f summable_on A›
  by (auto simp add: infsum_def infsum_in_def has_sum_euclidean_iff[abs_def] has_sum_def
      t2_space_class.Lim_def summable_on_def summable_on_in_def)

lemma infsum_euclidean_eq: ‹infsum_in euclidean f A = infsum f A›
  by (auto simp add: infsum_def infsum_in_def' summable_on_euclidean_eq
      has_sum_euclidean_iff[abs_def] has_sum_def t2_space_class.Lim_def)

lemma infsum_in_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "infsum_in T (λx. f (g x)) A = infsum_in T f B"
proof -
  have ‹infsum_in T (λx. f (g x)) A = infsum_in T f (g ` A)›
    by (metis (mono_tags, lifting) assms bij_betw_imp_inj_on infsum_in_cong infsum_in_reindex o_def)
  also have ‹… = infsum_in T f B›
    using assms bij_betw_imp_surj_on by blast
  finally show ?thesis .
qed

lemma limitin_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique S›
  shows ‹(rel_topology S ===> (R ===> S) ===> S ===> rel_filter R ===> (⟷)) limitin limitin›
proof (intro rel_funI, rename_tac T T' f f' l l' F F')
  fix T T' f f' l l' F F'
  assume [transfer_rule]: ‹rel_topology S T T'›
  assume [transfer_rule]: ‹(R ===> S) f f'›
  assume [transfer_rule]: ‹S l l'›
  assume [transfer_rule]: ‹rel_filter R F F'›

  have topspace: ‹l ∈ topspace T ⟷ l' ∈ topspace T'›
    by transfer_prover

  have open1: ‹∀⇩F x in F. f x ∈ U›
    if ‹openin T U› and ‹l ∈ U› and lhs: ‹(∀V. openin T' V ∧ l' ∈ V ⟶ (∀⇩F x in F'. f' x ∈ V))›
    for U
  proof -
    from ‹rel_topology S T T'› ‹openin T U›
    obtain V where ‹openin T' V› and [transfer_rule]: ‹rel_set S U V›
      by (smt (verit, best) Domainp.cases rel_fun_def rel_topology_def)
    with ‹S l l'› have ‹l' ∈ V›
      by (metis (no_types, lifting) assms bi_uniqueDr rel_setD1 that(2))
    with lhs ‹openin T' V›
    have ‹∀⇩F x in F'. f' x ∈ V›
      by auto
    then show ‹∀⇩F x in F. f x ∈ U›
      by transfer simp
  qed

  have open2: ‹∀⇩F x in F'. f' x ∈ V›
    if ‹openin T' V› and ‹l' ∈ V› and lhs: ‹(∀U. openin T U ∧ l ∈ U ⟶ (∀⇩F x in F. f x ∈ U))›
    for V
  proof -
    from ‹rel_topology S T T'› ‹openin T' V›
    obtain U where ‹openin T U› and [transfer_rule]: ‹rel_set S U V›
      by (auto simp: rel_topology_def rel_fun_def)
    with ‹S l l'› have ‹l ∈ U›
      by (metis (full_types) assms bi_unique_def rel_setD2 that(2))
    with lhs ‹openin T U›
    have ‹∀⇩F x in F. f x ∈ U›
      by auto
    then show ‹∀⇩F x in F'. f' x ∈ V›
      by transfer simp
  qed

  from topspace open1 open2
  show ‹limitin T f l F = limitin T' f' l' F'›
    unfolding limitin_def by auto
qed

lemma finite_subsets_at_top_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique R›
  shows ‹(rel_set R ===> rel_filter (rel_set R)) finite_subsets_at_top finite_subsets_at_top›
proof (intro rel_funI)
  fix A B assume ‹rel_set R A B›
  from ‹bi_unique R› obtain f where Rf: ‹R x (f x)› if ‹x ∈ A› for x
    by (metis (no_types, opaque_lifting) ‹rel_set R A B› rel_setD1)
  have ‹inj_on f A›
    by (metis (no_types, lifting) Rf assms bi_unique_def inj_onI)
  have ‹B = f ` A›
    by (metis (mono_tags, lifting) Rf ‹rel_set R A B› assms bi_uniqueDr bi_unique_rel_set_lemma image_cong)

  have RfX: ‹rel_set R X (f ` X)› if ‹X ⊆ A› for X
    apply (rule rel_setI)
    subgoal
      by (metis (no_types, lifting) Rf ‹inj_on f A› in_mono inj_on_image_mem_iff that)
    subgoal
      by (metis (no_types, lifting) Rf imageE subsetD that)
    done

  have Piff: ‹(∃X. finite X ∧ X ⊆ A ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ A ⟶ P (f ` Y))) ⟷
              (∃X. finite X ∧ X ⊆ B ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ B ⟶ P Y))› for P
  proof (rule iffI)
    assume ‹∃X. finite X ∧ X ⊆ A ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ A ⟶ P (f ` Y))›
    then obtain X where ‹finite X› and ‹X ⊆ A› and XP: ‹finite Y ⟹ X ⊆ Y ⟹ Y ⊆ A ⟹ P (f ` Y)› for Y
      by auto
    define X' where ‹X' = f ` X›
    have ‹finite X'›
      by (metis X'_def ‹finite X› finite_imageI)
    have ‹X' ⊆ B›
      by (smt (verit, best) Rf X'_def ‹X ⊆ A› ‹rel_set R A B› assms bi_uniqueDr image_subset_iff rel_setD1 subsetD)
    have ‹P Y'› if ‹finite Y'› and ‹X' ⊆ Y'› and ‹Y' ⊆ B› for Y'
    proof -
      define Y where ‹Y = (f -` Y') ∩ A›
      have ‹finite Y›
        by (metis Y_def ‹inj_on f A› finite_vimage_IntI that(1))
      moreover have ‹X ⊆ Y›
        by (metis (no_types, lifting) X'_def Y_def ‹X ⊆ A› image_subset_iff_subset_vimage le_inf_iff that(2))
      moreover have ‹Y ⊆ A›
        by (metis (no_types, lifting) Y_def inf_le2)
      ultimately have ‹P (f ` Y)›
        by (rule XP)
      then show ‹P Y'›
        by (metis (no_types, lifting) Int_greatest Y_def ‹B = f ` A› dual_order.refl image_subset_iff_subset_vimage inf_le1 subset_antisym subset_image_iff that(3))
    qed
    then show ‹∃X. finite X ∧ X ⊆ B ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ B ⟶ P Y)›
      by (metis (no_types, opaque_lifting) ‹X' ⊆ B› ‹finite X'›)
  next
    assume ‹∃X. finite X ∧ X ⊆ B ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ B ⟶ P Y)›
    then obtain X where ‹finite X› and ‹X ⊆ B› and XP: ‹finite Y ⟹ X ⊆ Y ⟹ Y ⊆ B ⟹ P Y› for Y
      by auto
    define X' where ‹X' = (f -` X) ∩ A›
    have ‹finite X'›
      by (simp add: X'_def ‹finite X› ‹inj_on f A› finite_vimage_IntI)
    have ‹X' ⊆ A›
      by (simp add: X'_def)
    have ‹P (f ` Y')› if ‹finite Y'› and ‹X' ⊆ Y'› and ‹Y' ⊆ A› for Y'
    proof -
      define Y where ‹Y = f ` Y'›
      have ‹finite Y›
        by (metis Y_def finite_imageI that(1))
      moreover have ‹X ⊆ Y›
        using X'_def Y_def ‹B = f ` A› ‹X ⊆ B› that(2) by blast
      moreover have ‹Y ⊆ B›
        by (metis Y_def ‹B = f ` A› image_mono that(3))
      ultimately have ‹P Y›
        by (rule XP)
      then show ‹P (f ` Y')›
        by (smt (z3) Y_def ‹B = f ` A› imageE imageI subset_antisym subset_iff that(3) vimage_eq)
    qed
    then show ‹∃X. finite X ∧ X ⊆ A ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ A ⟶ P (f ` Y))›
      by (metis ‹X' ⊆ A› ‹finite X'›)
  qed

  define Z where ‹Z = filtermap (λM. (M, f`M)) (finite_subsets_at_top A)›
  have ‹∀⇩F (x, y) in Z. rel_set R x y›
    by (auto intro!: eventually_finite_subsets_at_top_weakI simp add: Z_def eventually_filtermap RfX)
  moreover have ‹map_filter_on {(x, y). rel_set R x y} fst Z = finite_subsets_at_top A›
    apply (rule filter_eq_iff[THEN iffD2])
    apply (subst eventually_map_filter_on)
    subgoal
      by (auto intro!: eventually_finite_subsets_at_top_weakI simp add: Z_def eventually_filtermap RfX)[1]
    subgoal
      by (auto simp add: Z_def eventually_filtermap eventually_finite_subsets_at_top RfX)
    done
  moreover have ‹map_filter_on {(x, y). rel_set R x y} snd Z = finite_subsets_at_top B›
    apply (rule filter_eq_iff[THEN iffD2])
    apply (subst eventually_map_filter_on)
    subgoal
      by (auto intro!: eventually_finite_subsets_at_top_weakI simp add: Z_def eventually_filtermap RfX)[1]
    subgoal
      by (simp add: Z_def eventually_filtermap eventually_finite_subsets_at_top RfX Piff)
    done
  ultimately show ‹rel_filter (rel_set R) (finite_subsets_at_top A) (finite_subsets_at_top B)›
    by (rule rel_filter.intros[where Z=Z])
qed

lemma sum_parametric'[transfer_rule]:
  includes lifting_syntax
  fixes R :: ‹'a ⇒ 'b ⇒ bool› and S :: ‹'c::comm_monoid_add ⇒ 'd::comm_monoid_add ⇒ bool›
  assumes [transfer_rule]: ‹bi_unique R›
  assumes [transfer_rule]: ‹(S ===> S ===> S) (+) (+)›
  assumes [transfer_rule]: ‹S 0 0›
  shows ‹((R ===> S) ===> rel_set R ===> S) sum sum›
proof (intro rel_funI)
  fix A B f g assume ‹rel_set R A B› and ‹(R ===> S) f g›
  from ‹bi_unique R› obtain p where Rf: ‹R x (p x)› if ‹x ∈ A› for x
    by (metis (no_types, opaque_lifting) ‹rel_set R A B› rel_setD1)
  have ‹inj_on p A›
    by (metis (no_types, lifting) Rf ‹bi_unique R› bi_unique_def inj_onI)
  have ‹B = p ` A›
    by (metis (mono_tags, lifting) Rf ‹rel_set R A B› ‹bi_unique R› bi_uniqueDr bi_unique_rel_set_lemma image_cong)

  define A_copy where ‹A_copy = A›

  have *: ‹S (f x + sum f F) (g (p x) + sum g (p ` F))›
    if [transfer_rule]: ‹S (sum f F) (sum g (p ` F))› and [simp]: ‹x ∈ A› for x F
    by (metis (no_types, opaque_lifting) Rf ‹(R ===> S) f g› assms(2) rel_fun_def that(1) that(2))
  have ind_step: ‹S (sum f (insert x F)) (sum g (p ` insert x F))› 
    if ‹S (sum f F) (sum g (p ` F))› ‹x ∈ A› ‹x ∉ F› ‹finite F› ‹F ⊆ A› for x F
  proof -
    have "sum g (p ` insert x F) = g (p x) + sum g (p ` F)"
      unfolding image_insert using that
      by (subst sum.insert) (use inj_onD[OF ‹inj_on p A›, of x] in ‹auto›)
    thus ?thesis
      using that * by simp
  qed

  have ‹S (∑x∈A. f x) (∑x∈p ` A. g x)› if ‹A ⊆ A_copy›
    using that
   apply (induction A rule:infinite_finite_induct)
    unfolding A_copy_def
    subgoal
      by (metis (no_types, lifting) ‹inj_on p A› assms(3) finite_image_iff inj_on_subset sum.infinite)
    using ‹S 0 0› ind_step by auto
  hence ‹S (∑x∈A. f x) (∑x∈p ` A. g x)›
    by (simp add: A_copy_def)
  also have ‹… = (∑x∈B. g x)›
    by (metis (full_types) ‹B = p ` A›)
  finally show ‹S (∑x∈A. f x) (∑x∈B. g x)›
    by -
qed


lemma has_sum_in_parametric[transfer_rule]:
  includes lifting_syntax
  fixes R :: ‹'a ⇒ 'b ⇒ bool› and S :: ‹'c::comm_monoid_add ⇒ 'd::comm_monoid_add ⇒ bool›
  assumes [transfer_rule]: ‹bi_unique R›
  assumes [transfer_rule]: ‹bi_unique S›
  assumes [transfer_rule]: ‹(S ===> S ===> S) (+) (+)›
  assumes [transfer_rule]: ‹S 0 0›
  shows ‹(rel_topology S ===> (R ===> S) ===> (rel_set R) ===> S ===> (=)) has_sum_in has_sum_in›
proof -
  note sum_parametric'[transfer_rule]
  show ?thesis
    unfolding has_sum_in_def
    by transfer_prover
qed

lemma has_sum_in_topspace: ‹has_sum_in T f A s ⟹ s ∈ topspace T›
  by (metis has_sum_in_def limitin_def)

lemma summable_on_in_parametric[transfer_rule]: 
  includes lifting_syntax
  fixes R :: ‹'a ⇒ 'b ⇒ bool›
  assumes [transfer_rule]: ‹bi_unique R›
  assumes [transfer_rule]: ‹bi_unique S›
  assumes [transfer_rule]: ‹(S ===> S ===> S) (+) (+)›
  assumes [transfer_rule]: ‹S 0 0›
  shows ‹(rel_topology S ===> (R ===> S) ===> (rel_set R) ===> (=)) summable_on_in summable_on_in›
proof (intro rel_funI)
  fix T T' assume [transfer_rule]: ‹rel_topology S T T'›
  fix f f' assume [transfer_rule]: ‹(R ===> S) f f'›
  fix A A' assume [transfer_rule]: ‹rel_set R A A'›

  define ExT ExT' where ‹ExT P ⟷ (∃x∈Collect (Domainp S). P x)› and ‹ExT' P' ⟷ (∃x∈Collect (Rangep S). P' x)› for P P'
  have [transfer_rule]: ‹((S ===> (⟷)) ===> (⟷)) ExT ExT'›
    by (smt (z3) Domainp_iff ExT'_def ExT_def RangePI Rangep.cases mem_Collect_eq rel_fun_def)
  from ‹rel_topology S T T'› have top1: ‹topspace T ⊆ Collect (Domainp S)›
    unfolding rel_topology_def
    by (metis (no_types, lifting) Domainp_set mem_Collect_eq openin_topspace subsetI)
  from ‹rel_topology S T T'› have top2: ‹topspace T' ⊆ Collect (Rangep S)›
    unfolding rel_topology_def
    by (metis (no_types, lifting) RangePI Rangep.cases mem_Collect_eq openin_topspace rel_setD2 subsetI)

  have ‹ExT (has_sum_in T f A) = ExT' (has_sum_in T' f' A')›
    by transfer_prover
  with top1 top2 show ‹summable_on_in T f A ⟷ summable_on_in T' f' A'›
    by (metis ExT'_def ExT_def has_sum_in_topspace in_mono summable_on_in_def)
qed

lemma not_summable_infsum_in_0: ‹¬ summable_on_in T f A ⟹ infsum_in T f A = 0›
  by (smt (verit, del_insts) Collect_empty_eq card_eq_0_iff infsum_in_def summable_on_in_def zero_neq_one)

lemma infsum_in_parametric[transfer_rule]: 
  includes lifting_syntax
  fixes R :: ‹'a ⇒ 'b ⇒ bool›
  assumes [transfer_rule]: ‹bi_unique R›
  assumes [transfer_rule]: ‹bi_unique S›
  assumes [transfer_rule]: ‹(S ===> S ===> S) (+) (+)›
  assumes [transfer_rule]: ‹S 0 0›
  shows ‹(rel_topology S ===> (R ===> S) ===> (rel_set R) ===> S) infsum_in infsum_in›
proof (intro rel_funI)
  fix T T' assume [transfer_rule]: ‹rel_topology S T T'›
  fix f f' assume [transfer_rule]: ‹(R ===> S) f f'›
  fix A A' assume [transfer_rule]: ‹rel_set R A A'›
  have S_has_sum: ‹(S ===> (=)) (has_sum_in T f A) (has_sum_in T' f' A')›
    by transfer_prover

  have sum_iff: ‹summable_on_in T f A ⟷ summable_on_in T' f' A'›
    by transfer_prover

  define L L' where ‹L = Collect (has_sum_in T f A)› and ‹L' = Collect (has_sum_in T' f' A')›

  have LT: ‹L ⊆ topspace T›
    by (metis (mono_tags, lifting) Ball_Collect L_def has_sum_in_topspace subset_iff)
  have TS: ‹topspace T ⊆ Collect (Domainp S)›
    by (metis (no_types, lifting) Ball_Collect Domainp_set ‹rel_topology S T T'› openin_topspace rel_topology_def)
  have LT': ‹L' ⊆ topspace T'›
    by (metis Ball_Collect L'_def has_sum_in_topspace subset_eq)
  have T'S: ‹topspace T' ⊆ Collect (Rangep S)›
    by (metis (mono_tags, opaque_lifting) Ball_Collect RangePI ‹rel_topology S T T'› rel_fun_def rel_setD2 topspace_parametric)
  have Sss': ‹S s s' ⟹ has_sum_in T f A s ⟷ has_sum_in T' f' A' s'› for s s'
    using S_has_sum
    by (metis (mono_tags, lifting) rel_funE)

  have ‹rel_set S L L'›
    by (smt (verit) Domainp.cases L'_def L_def Rangep.cases ‹L ⊆ topspace T› ‹L' ⊆ topspace T'› ‹⋀s' s. S s s' ⟹ has_sum_in T f A s = has_sum_in T' f' A' s'› ‹topspace T ⊆ Collect (Domainp S)› ‹topspace T' ⊆ Collect (Rangep S)› in_mono mem_Collect_eq rel_setI)

  have cardLL': ‹card L = 1 ⟷ card L' = 1›
    by (metis (no_types, lifting) ‹rel_set S L L'› assms(2) bi_unique_rel_set_lemma card_image)

  have ‹S (infsum_in T f A) (infsum_in T' f' A')› if ‹card L ≠ 1›
    using that cardLL' by (simp add: infsum_in_def L'_def L_def Let_def that ‹S 0 0› flip: sum_iff)

  moreover have ‹S (infsum_in T f A) (infsum_in T' f' A')› if [simp]: ‹card L = 1›
  proof -
    have [simp]: ‹card L' = 1›
      using that cardLL' by simp
    have ‹S (the_elem L) (the_elem L')›
      using ‹rel_set S L L'›
      by (metis (no_types, opaque_lifting) ‹card L' = 1› is_singleton_altdef is_singleton_the_elem rel_setD1 singleton_iff that)
    then show ?thesis
      by (simp add: infsum_in_def flip: L'_def L_def)
  qed

  ultimately show ‹S (infsum_in T f A) (infsum_in T' f' A')›
    by auto
qed

lemma infsum_parametric[transfer_rule]: 
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique R›
  shows ‹((R ===> (=)) ===> (rel_set R) ===> (=)) infsum infsum›
  unfolding infsum_euclidean_eq[symmetric]
  by transfer_prover

lemma summable_on_transfer[transfer_rule]: 
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique R›
  shows ‹((R ===> (=)) ===> (rel_set R) ===> (=)) Infinite_Sum.summable_on Infinite_Sum.summable_on›
  unfolding summable_on_euclidean_eq[symmetric]
  by transfer_prover

lemma abs_gbinomial: ‹abs (a gchoose n) = (-1)^(n - nat (ceiling a)) * (a gchoose n)›
proof -
  have ‹(∏i=0..<n. abs (a - of_nat i)) = (- 1) ^ (n - nat (ceiling a)) * (∏i=0..<n. a - of_nat i)›
  proof (induction n)
    case 0
    then show ?case
      by simp
  next
    case (Suc n)
    consider (geq) ‹of_int n ≥ a› | (lt) ‹of_int n < a›
      by fastforce
    then show ?case
    proof cases
      case geq
      from geq have ‹abs (a - of_int n) = - (a - of_int n)›
        by simp
      moreover from geq have ‹(Suc n - nat (ceiling a)) = (n - nat (ceiling a)) + 1›
        by (metis Suc_diff_le Suc_eq_plus1 ceiling_le nat_le_iff)
      ultimately show ?thesis
        apply (simp add: Suc)
        by (metis (no_types, lifting) ‹¦a - of_int (int n)¦ = - (a - of_int (int n))› mult.assoc mult_minus_right of_int_of_nat_eq)
    next
      case lt
      from lt have ‹abs (a - of_int n) = (a - of_int n)›
        by simp
      moreover from lt have ‹(Suc n - nat (ceiling a)) = (n - nat (ceiling a))›
        by (smt (verit, ccfv_threshold) Suc_leI cancel_comm_monoid_add_class.diff_cancel diff_commute diff_diff_cancel diff_le_self less_ceiling_iff linorder_not_le order_less_le zless_nat_eq_int_zless)
      ultimately show ?thesis
        by (simp add: Suc)
    qed
  qed
  then show ?thesis
    by (simp add: gbinomial_prod_rev abs_prod)
qed

lemma gbinomial_sum_lower_abs: 
  fixes a :: ‹'a::{floor_ceiling}›
  defines ‹a' ≡ nat (ceiling a)›
  assumes ‹of_nat m ≥ a-1›
  shows "(∑k≤m. abs (a gchoose k)) = 
                 (-1)^a' * ((-1) ^ m * (a - 1 gchoose m)) 
               - (-1)^a' * of_bool (a'>0) * ((-1) ^ (a'-1) * (a-1 gchoose (a'-1)))
               + (∑k<a'. abs (a gchoose k))"
proof -
  from assms
  have ‹a' ≤ Suc m›
    using ceiling_mono by force

  have ‹(∑k≤m. abs (a gchoose k)) = (∑k=a'..m. abs (a gchoose k)) + (∑k<a'. abs (a gchoose k))›
    apply (subst asm_rl[of ‹{..m} = {a'..m} ∪ {..<a'}›])
    using ‹a' ≤ Suc m› apply auto[1]
    apply (subst sum.union_disjoint)
    by auto
  also have ‹… = (∑k=a'..m. (-1)^(k-a') * (a gchoose k)) + (∑k<a'. abs (a gchoose k))›
    apply (rule arg_cong[where f=‹λx. x + _›])
    apply (rule sum.cong[OF refl])
    apply (subst abs_gbinomial)
    using a'_def by blast
  also have ‹… = (∑k=a'..m. (-1)^k * (-1)^a' * (a gchoose k)) + (∑k<a'. abs (a gchoose k))›
    apply (rule arg_cong[where f=‹λx. x + _›])
    apply (rule sum.cong[OF refl])
    by (simp add: power_diff_conv_inverse)
  also have ‹… = (-1)^a' * (∑k=a'..m. (a gchoose k) * (-1)^k) + (∑k<a'. abs (a gchoose k))›
    by (auto intro: sum.cong simp: sum_distrib_left)
  also have ‹… = (-1)^a' * (∑k≤m. (a gchoose k) * (-1)^k) - (-1)^a' * (∑k<a'. (a gchoose k) * (-1)^k) + (∑k<a'. abs (a gchoose k))›
    apply (subst asm_rl[of ‹{..m} = {..<a'} ∪ {a'..m}›])
    using ‹a' ≤ Suc m› apply auto[1]
    apply (subst sum.union_disjoint)
    by (auto simp: distrib_left)
  also have ‹… = (-1)^a' * ((- 1) ^ m * (a - 1 gchoose m)) - (-1)^a' * (∑k<a'. (a gchoose k) * (-1)^k) + (∑k<a'. abs (a gchoose k))›
    apply (subst gbinomial_sum_lower_neg)
    by simp
  also have ‹… = (-1)^a' * ((-1) ^ m * (a - 1 gchoose m)) - (-1)^a' 
               * of_bool (a'>0) * ((-1) ^ (a'-1) * (a-1 gchoose (a'-1)))
               + (∑k<a'. abs (a gchoose k))›
    apply (cases ‹a' = 0›)
    subgoal
      by simp
    subgoal
      by (subst asm_rl[of ‹{..<a'} = {..a'-1}›]) (auto simp: gbinomial_sum_lower_neg)
    done
  finally show ?thesis
    by -
qed

lemma abs_gbinomial_leq1:
  fixes a :: ‹'a :: {linordered_field}›
  assumes ‹abs a ≤ 1›
  shows ‹abs (a gchoose b) ≤ 1›
proof -
  have *: ‹-1 ≤ a› ‹a ≤ 1›
    using abs_le_D2 assms minus_le_iff abs_le_iff assms by auto
  have ‹abs (a gchoose b) = abs ((∏i = 0..<b. a - of_nat i) / fact b)›
    by (simp add: gbinomial_prod_rev)
  also have ‹… = abs ((∏i=0..<b. a - of_nat i)) / fact b›
    apply (subst abs_divide)
    by simp
  also have ‹… = (∏i=0..<b. abs (a - of_nat i)) / fact b›
    apply (subst abs_prod) by simp
  also have ‹… ≤ (∏i=0..<b. of_nat (Suc i)) / fact b›
  proof (intro divide_right_mono prod_mono conjI)
    fix i assume "i ∈ {0..<b}"
    have "¦a - of_nat i¦ ≤ ¦a¦ + ¦of_nat i¦"
      by linarith
    also have "¦a¦ ≤ 1"
      by fact
    finally show "¦a - of_nat i¦ ≤ of_nat (Suc i)"
      by simp
  qed auto
  also have ‹… = fact b / fact b›
    by (subst (2) fact_prod_Suc) auto
  also have ‹… = 1›
    by simp
  finally show ?thesis
    by -
qed

lemma gbinomial_summable_abs:
  fixes a :: real
  assumes ‹a ≥ 0› and ‹a ≤ 1›
  shows ‹summable (λn. abs (a gchoose n))›
proof -
  define a' where ‹a' = nat (ceiling a)›
  have a': ‹a' = 0 ∨ a' = 1›
    by (metis One_nat_def a'_def assms(2) ceiling_le_one less_one nat_1 nat_mono order_le_less)
  have aux1: ‹abs x ≤ x' ⟹ abs y ≤ y' ⟹ abs z ≤ z' ⟹ x - y + z ≤ x' + y' + z'› for x y z x' y' z' :: real
    by auto
  have ‹(∑i≤n. ¦a gchoose i¦) = (- 1) ^ a' * ((- 1) ^ n * (a - 1 gchoose n)) -
    (- 1) ^ a' * of_bool (0 < a') * ((- 1) ^ (a' - 1) * (a - 1 gchoose (a' - 1))) +
    (∑k<a'. ¦a gchoose k¦)› for n
    unfolding a'_def  by (rule gbinomial_sum_lower_abs) (use assms in auto)
  also have ‹…n ≤ 1 + 1 + 1› for n
    by (rule aux1) (use a' in ‹auto simp add: abs_mult abs_gbinomial_leq1 assms›)
  also have ‹… = 3›
    by simp
  finally show ?thesis
    by (meson abs_ge_zero bounded_imp_summable)
qed

lemma summable_tendsto_times_n:
  fixes f :: ‹nat ⇒ real›
  assumes pos: ‹⋀n. f n ≥ 0›
  assumes dec: ‹decseq (λn. (n+M) * f (n + M))›
  assumes sum: ‹summable f›
  shows ‹(λn. n * f n) ⇢ 0›
proof (rule ccontr)
  assume lim_not_0: ‹¬ (λn. n * f n) ⇢ 0›
  obtain B where ‹(λn. (n+M) * f (n+M)) ⇢ B› and nfB': ‹(n+M) * f (n+M) ≥ B› for n
    apply (rule decseq_convergent[where B=0, OF dec])
    using pos that by auto
  then have lim_B: ‹(λn. n * f n) ⇢ B›
    by - (rule LIMSEQ_offset)
  have ‹B ≥ 0›
    apply (subgoal_tac ‹⋀n. n * f n ≥ 0›)
    using Lim_bounded2 lim_B apply blast
    by (simp add: pos)
  moreover have ‹B ≠ 0›
    using lim_B lim_not_0 by blast
  ultimately have ‹B > 0›
    by linarith

  have ge: ‹f n ≥ B / n› if ‹n ≥ M› for n
    using nfB'[of ‹n-M›] that ‹B > 0›  by (auto simp: divide_simps mult_ac)

  have ‹summable (λn. B / n)›
    by (rule summable_comparison_test'[where N=M]) (use sum ‹B > 0› ge in auto)

  moreover have ‹¬ summable (λn. B / n)›
  proof (rule ccontr)
    define C where ‹C = (∑n. 1 / real n)›
    assume ‹¬ ¬ summable (λn. B / real n)›
    then have ‹summable (λn. inverse B * (B / real n))›
      using summable_mult by blast
    then have ‹summable (λn. 1 / real n)›
      using ‹B ≠ 0› by auto
    then have ‹(∑n=1..m. 1 / real n) ≤ C› for m
      unfolding C_def by (rule sum_le_suminf) auto
    then have ‹harm m ≤ C› for m
      by (simp add: harm_def inverse_eq_divide)
    then have ‹harm (nat (ceiling (exp C))) ≤ C›
      by -
    then have ‹ln (real (nat (ceiling (exp C))) + 1) ≤ C›
      by (smt (verit, best) ln_le_harm)
    then show False
      by (smt (z3) exp_ln ln_ge_iff of_nat_0_le_iff real_nat_ceiling_ge)
  qed

  ultimately show False
    by simp
qed
  


lemma gbinomial_tendsto_0:
  fixes a :: real
  assumes ‹a > -1›
  shows ‹(λn. (a gchoose n)) ⇢ 0›
proof -
  have thesis1: ‹(λn. (a gchoose n)) ⇢ 0› if ‹a ≥ 0› for a :: real
  proof -
    define m where ‹m = nat (floor a)›
    have m: ‹a ≥ real m› ‹a ≤ real m + 1›
      by (simp_all add: m_def that)
    show ?thesis
    proof (insert m, induction m arbitrary: a)
      case 0
      then have *: ‹a ≥ 0› ‹a ≤ 1›
        using assms by auto
      show ?case
        using gbinomial_summable_abs[OF *]
        using summable_LIMSEQ_zero tendsto_rabs_zero_iff by blast
    next
      case (Suc m)
      have 1: ‹(λn. (a-1 gchoose n)) ⇢ 0›
        by (rule Suc.IH) (use Suc.prems in auto)
      then have ‹(λn. (a-1 gchoose Suc n)) ⇢ 0›
        using filterlim_sequentially_Suc by blast
      with 1 have ‹(λn. (a-1 gchoose n) + (a-1 gchoose Suc n)) ⇢ 0›
        by (simp add: tendsto_add_zero)
      then have ‹(λn. (a gchoose Suc n)) ⇢ 0›
        using gbinomial_Suc_Suc[of ‹a-1›] by simp
      then show ?case
        using filterlim_sequentially_Suc by blast
    qed
  qed

  have thesis2: ‹(λn. (a gchoose n)) ⇢ 0› if ‹a > -1› ‹a ≤ 0›
  proof -
    have decseq: ‹decseq (λn. abs (a gchoose n))›
    proof (rule decseq_SucI)
      fix n
      have ‹¦a gchoose Suc n¦ = ¦a gchoose n¦ * (¦a - real n¦ / (1 + n))›
        unfolding gbinomial_prod_rev by (simp add: abs_mult) 
      also have ‹… ≤ ¦a gchoose n¦›
        apply (rule mult_left_le)
        using assms that(2) by auto
      finally show ‹¦a gchoose Suc n¦ ≤ ¦a gchoose n¦›
        by -
    qed
    have abs_a1: ‹abs (a+1) = a+1›
      using assms by auto

    have ‹0 ≤ ¦a + 1 gchoose n¦› for n
      by simp
    moreover have ‹decseq (λn. (n+1) * abs (a+1 gchoose (n+1)))›
      using decseq apply (simp add: gbinomial_rec abs_mult)
      by (smt (verit, best) decseq_def mult.commute mult_left_mono)
    moreover have ‹summable (λn. abs (a+1 gchoose n))›
      apply (rule gbinomial_summable_abs)
      using that by auto
    ultimately have ‹(λn. n * abs (a+1 gchoose n)) ⇢ 0›
      by (rule summable_tendsto_times_n)
    then have ‹(λn. Suc n * abs (a+1 gchoose Suc n)) ⇢ 0›
      by (rule_tac LIMSEQ_ignore_initial_segment[where k=1 and a=0, simplified])
    then have ‹(λn. abs (Suc n * (a+1 gchoose Suc n))) ⇢ 0›
      by (simp add: abs_mult)
    then have ‹(λn. (a+1) * abs (a gchoose n)) ⇢ 0›
      apply (subst (asm) gbinomial_absorption)
      by (simp add: abs_mult abs_a1)
    then have ‹(λn. abs (a gchoose n)) ⇢ 0›
      using that(1) by force
    then show ‹(λn. (a gchoose n)) ⇢ 0›
      by (rule tendsto_rabs_zero_cancel)
  qed

  from thesis1 thesis2 assms show ?thesis
    using linorder_linear by blast
qed


(* lemma gbinomial_minus1[simp]: ‹(-1 gchoose n) = (case n of 0 ⇒ 1 | _ ⇒ -1)›
  apply (cases n)
   apply auto
  unfolding gbinomial_prod_rev
  apply auto
  by auto *)

lemma gbinomial_abs_sum:
  fixes a :: real
  assumes ‹a > 0› and ‹a ≤ 1›
  shows ‹(λn. abs (a gchoose n)) sums 2›
proof -
  define a' where ‹a' = nat (ceiling a)›
  have ‹a' = 1›
    using a'_def assms(1) assms(2) by linarith
  have lim: ‹(λn. (a - 1 gchoose n)) ⇢ 0›
    by (simp add: assms(1) gbinomial_tendsto_0)
  have ‹(∑k≤n. abs (a gchoose k)) = (- 1) ^ a' * ((- 1) ^ n * (a - 1 gchoose n)) -
    (- 1) ^ a' * of_bool (0 < a') * ((- 1) ^ (a'-1) * (a - 1 gchoose (a' - 1))) +
    (∑k<a'. ¦a gchoose k¦)› for n
    unfolding a'_def
    apply (rule gbinomial_sum_lower_abs)
    using assms(2) by linarith
  also have ‹…n = 2 - (- 1) ^ n * (a - 1 gchoose n)› for n
    using assms
    by (auto simp add: ‹a' = 1›)
  finally have ‹(∑k≤n. abs (a gchoose k)) = 2 - (- 1) ^ n * (a - 1 gchoose n)› for n
    by -
  moreover have ‹(λn. 2 - (- 1) ^ n * (a - 1 gchoose n)) ⇢ 2›
  proof -
    have ‹(λn. ((-1) ^ n * (a-1 gchoose n))) ⇢ 0›
      by (rule tendsto_rabs_zero_cancel) (use lim in ‹simp add: abs_mult tendsto_rabs_zero_iff›)
    then have ‹(λn. 2 - (- 1) ^ n * (a - 1 gchoose n)) ⇢ 2 - 0›
      by (rule tendsto_diff[rotated]) simp
    then show ?thesis
      by simp
  qed
  ultimately have ‹(λn. ∑k≤n. abs (a gchoose k)) ⇢ 2›
    by auto
  then show ?thesis
    using sums_def_le by blast
qed

lemma sums_has_sum:
  fixes s :: ‹'a :: banach›
  assumes sums: ‹f sums s›
  assumes abs_sum: ‹summable (λn. norm (f n))›
  shows ‹(f has_sum s) UNIV›
proof (rule has_sumI_metric)
  fix e :: real assume ‹0 < e›
  define e' where ‹e' = e/2›
  then have ‹e' > 0›
    using ‹0 < e› half_gt_zero by blast
  from suminf_exist_split[where r=e', OF ‹0<e'› abs_sum]
  obtain N where ‹norm (∑i. norm (f (i + N))) < e'›
    by auto
  then have N: ‹(∑i. norm (f (i + N))) < e'›
    by auto
  then have N': ‹norm (∑i. f (i + N)) < e'›
    apply (rule dual_order.strict_trans2)
    by (auto intro!: summable_norm summable_iff_shift[THEN iffD2] abs_sum)

  define X where ‹X = {..<N}›
  then have ‹finite X›
    by auto
  moreover have ‹dist (sum f Y) s < e› if ‹finite Y› and ‹X ⊆ Y› for Y
  proof -
    have ‹dist (sum f Y) s = norm (s - sum f {..<N} - sum f (Y-{..<N}))›
      by (metis X_def diff_diff_eq2 dist_norm norm_minus_commute sum.subset_diff that(1) that(2))
    also have ‹… ≤ norm (s - sum f {..<N}) + norm (sum f (Y-{..<N}))›
      using norm_triangle_ineq4 by blast
    also have ‹… = norm (∑i. f (i + N)) + norm (sum f (Y-{..<N}))›
      apply (subst suminf_minus_initial_segment)
      using sums sums_summable apply blast
      using sums sums_unique by blast
    also have ‹… < e' + norm (sum f (Y-{..<N}))›
      using N' by simp
    also have ‹… ≤ e' + norm (∑i∈Y-{..<N}. norm (f i))›
      apply (rule add_left_mono)
      by (smt (verit, best) real_norm_def sum_norm_le)
    also have ‹… ≤ e' + (∑i∈Y-{..<N}. norm (f i))›
      apply (rule add_left_mono)
      by (simp add: sum_nonneg)
    also have "(∑i∈Y-{..<N}. norm (f i)) = (∑i|i+N∈Y. norm (f (i + N)))"
      by (rule sum.reindex_bij_witness[of _ "λi. i + N" "λi. i - N"]) auto
    also have ‹e' + … ≤ e' + (∑i. norm (f (i + N)))›
      by (auto intro!: add_left_mono sum_le_suminf summable_iff_shift[THEN iffD2] abs_sum finite_inverse_image ‹finite Y›)
    also have ‹… ≤ e' + e'›
      using N by simp
    also have ‹… = e›
      by (simp add: e'_def)
    finally show ?thesis
      by -
  qed
  ultimately show ‹∃X. finite X ∧ X ⊆ UNIV ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ UNIV ⟶ dist (sum f Y) s < e)›
    by auto
qed

lemma sums_has_sum_pos:
  fixes s :: real
  assumes ‹f sums s›
  assumes ‹⋀n. f n ≥ 0›
  shows ‹(f has_sum s) UNIV›
  apply (rule sums_has_sum)
  apply (simp add: assms(1))
  using assms(1) assms(2) summable_def by auto

lemma gbinomial_abs_has_sum:
  fixes a :: real
  assumes ‹a > 0› and ‹a ≤ 1›
  shows ‹((λn. abs (a gchoose n)) has_sum 2) UNIV›
  apply (rule sums_has_sum_pos)
   apply (rule gbinomial_abs_sum)
  using assms by auto

lemma gbinomial_abs_has_sum_1:
  fixes a :: real
  assumes ‹a > 0› and ‹a ≤ 1›
  shows ‹((λn. abs (a gchoose n)) has_sum 1) (UNIV-{0})›
proof -
  have ‹((λn. abs (a gchoose n)) has_sum 2-(∑n∈{0}. abs (a gchoose n))) (UNIV-{0})›
    apply (rule has_sum_Diff)
      apply (rule gbinomial_abs_has_sum)
    using assms apply auto[2]
     apply (rule has_sum_finite)
    by auto
  then show ?thesis
    by simp
qed

lemma gbinomial_abs_summable:
  fixes a :: real
  assumes ‹a > 0› and ‹a ≤ 1›
  shows ‹(λn. (a gchoose n)) abs_summable_on UNIV›
  using assms by (auto intro!: has_sum_imp_summable gbinomial_abs_has_sum)

lemma gbinomial_abs_summable_1:
  fixes a :: real
  assumes ‹a > 0› and ‹a ≤ 1›
  shows ‹(λn. (a gchoose n)) abs_summable_on UNIV-{0}›
  using assms by (auto intro!: has_sum_imp_summable gbinomial_abs_has_sum_1)

lemma has_sum_singleton[simp]: ‹(f has_sum y) {x} ⟷ f x = y› for y :: ‹'a :: {comm_monoid_add, t2_space}›
  using has_sum_finite[of ‹{x}›] infsumI[of f "{x}" y] by auto


lemma has_sum_sums: ‹f sums s› if ‹(f has_sum s) UNIV›
proof -
  have ‹(λn. sum f {..<n}) ⇢ s›
  proof (unfold tendsto_def, intro allI impI)
    fix S assume ‹open S› and ‹s ∈ S›
    with ‹(f has_sum s) UNIV›
    have ‹∀⇩F F in finite_subsets_at_top UNIV. sum f F ∈ S›
      using has_sum_def tendsto_def by blast
    then
    show ‹∀⇩F x in sequentially. sum f {..<x} ∈ S›
      using eventually_compose_filterlim filterlim_lessThan_at_top by blast
  qed
  then show ?thesis
    by (simp add: sums_def)
qed

lemma The_eqI1:
  assumes ‹⋀x y. F x ⟹ F y ⟹ x = y›
  assumes ‹∃z. F z›
  assumes ‹⋀x. F x ⟹ P x = Q x›
  shows ‹P (The F) = Q (The F)›
  by (metis assms(1) assms(2) assms(3) theI)

lemma summable_on_uminus[intro!]: 
  fixes f :: ‹'a ⇒ 'b :: real_normed_vector› (* Can probably be shown for a much wider type class. *)
  assumes ‹f summable_on A›
  shows ‹(λi. - f i) summable_on A›
  apply (subst asm_rl[of ‹(λi. - f i) = (λi. (-1) *⇩R f i)›])
   apply simp
  using assms by (rule summable_on_scaleR_right)

lemma summable_on_diff:
  fixes f g :: "'a ⇒ 'b::real_normed_vector"  (* Can probably be shown for a much wider type class. *)
  assumes ‹f summable_on A›
  assumes ‹g summable_on A›
  shows ‹(λx. f x - g x) summable_on A›
  using summable_on_add[where f=f and g=‹λx. - g x›] summable_on_uminus[where f=g]
  using assms by auto


lemma gbinomial_1: ‹(1 gchoose n) = of_bool (n≤1)›
proof -
  consider (0) ‹n=0› | (1) ‹n=1› | (bigger) m where ‹n=Suc (Suc m)›
    by (metis One_nat_def not0_implies_Suc)
  then show ?thesis
  proof cases
    case 0
    then show ?thesis
      by simp
  next
    case 1
    then show ?thesis
      by simp
  next
    case bigger
    then show ?thesis
      using gbinomial_rec[where a=0 and k=‹Suc m›]
      by simp
  qed
qed



lemma gbinomial_a_Suc_n:
  ‹(a gchoose Suc n) = (a gchoose n) * (a-n) / Suc n›
  by (simp add: gbinomial_prod_rev)

lemma has_sum_in_0[simp]:
  assumes ‹0 ∈ topspace T›
  assumes ‹⋀x. x∈A ⟹ f x = 0›
  shows ‹has_sum_in T f A 0›
proof -
  have ‹has_sum_in T (λ_. 0) A 0›
    using assms
    by (simp add: has_sum_in_def sum.neutral_const[abs_def])
  then show ?thesis
    apply (rule has_sum_in_cong[THEN iffD2, rotated])
    using assms by simp
qed

lemma summable_on_in_cong:
  assumes "⋀x. x∈A ⟹ f x = g x"
  shows "summable_on_in T f A ⟷ summable_on_in T g A"
  by (simp add: summable_on_in_def has_sum_in_cong[OF assms])

lemma infsum_in_0:
  assumes ‹Hausdorff_space T› and ‹0 ∈ topspace T›
  assumes ‹⋀x. x∈M ⟹ f x = 0›
  shows ‹infsum_in T f M = 0›
proof -
  have ‹has_sum_in T f M 0›
    using assms
    by (auto intro!: has_sum_in_0 Hausdorff_imp_t1_space)
  then show ?thesis
    by (meson assms(1) has_sum_in_infsum_in has_sum_in_unique not_summable_infsum_in_0)
qed

lemma summable_on_in_finite:
  fixes f :: ‹'a ⇒ 'b::{comm_monoid_add,topological_space}›
  assumes "finite F"
  assumes ‹sum f F ∈ topspace T›
  shows "summable_on_in T f F"
  using assms summable_on_in_def has_sum_in_finite by blast

lemma has_sum_diff:
  fixes f g :: "'a ⇒ 'b::{topological_ab_group_add}"
  assumes ‹(f has_sum a) A›
  assumes ‹(g has_sum b) A›
  shows ‹((λx. f x - g x) has_sum (a - b)) A›
  by (auto intro!: has_sum_add has_sum_uminus[THEN iffD2] assms simp add: simp flip: add_uminus_conv_diff)

lemma has_sum_of_real:
  fixes f :: "'a ⇒ real"
  assumes ‹(f has_sum a) A›
  shows ‹((λx. of_real (f x)) has_sum (of_real a :: 'b::{real_algebra_1,real_normed_vector})) A›
  apply (rule has_sum_comm_additive[unfolded o_def, where f=of_real])
  by (auto intro!: additive.intro assms tendsto_of_real)

lemma summable_on_cdivide:
  fixes f :: "'a ⇒ 'b :: {t2_space, topological_semigroup_mult, division_ring}"
  assumes ‹f summable_on A›
  shows "(λx. f x / c) summable_on A"
  apply (subst division_ring_class.divide_inverse)
  using assms summable_on_cmult_left by blast

lemma has_sum_in_weaker_topology:
  assumes ‹continuous_map T U (λf. f)›
  assumes ‹has_sum_in T f A l›
  shows ‹has_sum_in U f A l›
  using continuous_map_limit[OF assms(1)]
  using assms(2)
  by (auto simp: has_sum_in_def o_def)

lemma summable_on_in_weaker_topology:
  assumes ‹continuous_map T U (λf. f)›
  assumes ‹summable_on_in T f A›
  shows ‹summable_on_in U f A›
  by (meson assms(1,2) has_sum_in_weaker_topology summable_on_in_def)

lemma norm_abs[simp]: ‹norm (abs x) = norm x› for x :: ‹'a :: {idom_abs_sgn, real_normed_div_algebra}›
proof -
  have ‹norm x = norm (sgn x * abs x)›
    by (simp add: sgn_mult_abs)
  also have ‹… = norm ¦x¦›
    by (simp add: norm_mult norm_sgn)
  finally show ?thesis
    by simp
qed

(* Strengthening of  *) thm abs_summable_product (* with narrower typeclass *)
lemma abs_summable_product:
  fixes x :: "'a ⇒ 'b::real_normed_div_algebra"
  assumes x2_sum: "(λi. (x i)⇧2) abs_summable_on A"
    and y2_sum: "(λi. (y i)⇧2) abs_summable_on A"
  shows "(λi. x i * y i) abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on)
  show ‹0 ≤ norm (x i * y i)› for i
    by simp
  show ‹bdd_above (sum (λi. norm (x i * y i)) ` {F. F ⊆ A ∧ finite F})›
  proof (rule bdd_aboveI2, rename_tac F)
    fix F assume ‹F ∈ {F. F ⊆ A ∧ finite F}›
    then have "finite F" and "F ⊆ A"
      by auto

    have "norm (x i * y i) ≤ norm (x i * x i) + norm (y i * y i)" for i
      unfolding norm_mult
      by (smt mult_left_mono mult_nonneg_nonneg mult_right_mono norm_ge_zero)
    hence "(∑i∈F. norm (x i * y i)) ≤ (∑i∈F. norm ((x i)⇧2) + norm ((y i)⇧2))"
      using [[simp_trace]]
      by (simp add: power2_eq_square sum_mono)
    also have "… = (∑i∈F. norm ((x i)⇧2)) + (∑i∈F. norm ((y i)⇧2))"
      by (simp add: sum.distrib)
    also have "… ≤ (∑⇩∞i∈A. norm ((x i)⇧2)) + (∑⇩∞i∈A. norm ((y i)⇧2))"
      using x2_sum y2_sum ‹finite F› ‹F ⊆ A› by (auto intro!: finite_sum_le_infsum add_mono)
    finally show ‹(∑xa∈F. norm (x xa * y xa)) ≤ (∑⇩∞i∈A. norm ((x i)⇧2)) + (∑⇩∞i∈A. norm ((y i)⇧2))›
      by simp
  qed
qed

lemma Cauchy_Schwarz_ineq_infsum:
  fixes x :: "'a ⇒ 'b::{real_normed_div_algebra}"
  assumes x2_sum: "(λi. (x i)⇧2) abs_summable_on A"
    and y2_sum: "(λi. (y i)⇧2) abs_summable_on A"
  shows ‹(∑⇩∞i∈A. norm (x i * y i)) ≤ sqrt (∑⇩∞i∈A. (norm (x i))⇧2) * sqrt (∑⇩∞i∈A. (norm (y i))⇧2)›
proof -
  (* have ‹(norm (∑⇩∞i∈A. x i * y i)) ≤ (∑⇩∞i∈A. norm (x i * y i))›
    by (simp add: Misc_Tensor_Product.abs_summable_product assms(2) norm_infsum_bound x2_sum)
  also *) have ‹(∑⇩∞i∈A. norm (x i * y i)) ≤ sqrt (∑⇩∞i∈A. (norm (x i))⇧2) * sqrt (∑⇩∞i∈A. (norm (y i))⇧2)›
  proof (rule infsum_le_finite_sums)
    show ‹(λi. x i * y i) abs_summable_on A›
      using Misc_Tensor_Product.abs_summable_product x2_sum y2_sum by blast
    fix F assume ‹finite F› and ‹F ⊆ A›


    have sum1: ‹(λi. (norm (x i))⇧2) summable_on A›
      by (metis (mono_tags, lifting) norm_power summable_on_cong x2_sum)
    have sum2: ‹(λi. (norm (y i))⇧2) summable_on A›
      by (metis (no_types, lifting) norm_power summable_on_cong y2_sum)

    have ‹(∑i∈F. norm (x i * y i))⇧2 = (∑i∈F. norm (x i) * norm (y i))⇧2›
      by (simp add: norm_mult)
    also have ‹… ≤ (∑i∈F. (norm (x i))⇧2) * (∑i∈F. (norm (y i))⇧2)›
      using Cauchy_Schwarz_ineq_sum by fastforce
    also have ‹… ≤ (∑⇩∞i∈A. (norm (x i))⇧2) * (∑i∈F. (norm (y i))⇧2)›
      using sum1 ‹finite F› ‹F ⊆ A› 
      by (auto intro!: mult_right_mono finite_sum_le_infsum sum_nonneg)
    also have ‹… ≤ (∑⇩∞i∈A. (norm (x i))⇧2) * (∑⇩∞i∈A. (norm (y i))⇧2)›
      using sum2 ‹finite F› ‹F ⊆ A› 
      by (auto intro!: mult_left_mono finite_sum_le_infsum infsum_nonneg)
    also have ‹… = (sqrt (∑⇩∞i∈A. (norm (x i))⇧2) * sqrt (∑⇩∞i∈A. (norm (y i))⇧2))⇧2›
      by (smt (verit, best) calculation real_sqrt_mult real_sqrt_pow2 zero_le_power2)
  finally show ‹(∑i∈F. norm (x i * y i)) ≤ sqrt (∑⇩∞i∈A. (norm (x i))⇧2) * sqrt (∑⇩∞i∈A. (norm (y i))⇧2)›
    apply (rule power2_le_imp_le)
    by (auto intro!: mult_nonneg_nonneg infsum_nonneg)
  qed
  then show ?thesis
    by -
qed

lemma continuous_map_pullback_both:
  assumes cont: ‹continuous_map T1 T2 g'›
  assumes g'g: ‹⋀x. f1 x ∈ topspace T1 ⟹ x ∈ A1 ⟹ g' (f1 x) = f2 (g x)›
  assumes top1: ‹f1 -` topspace T1 ∩ A1 ⊆ g -` A2›
  shows ‹continuous_map (pullback_topology A1 f1 T1) (pullback_topology A2 f2 T2) g›
proof -
  from cont
  have ‹continuous_map (pullback_topology A1 f1 T1) T2 (g' ∘ f1)›
    by (rule continuous_map_pullback)
  then have ‹continuous_map (pullback_topology A1 f1 T1) T2 (f2 ∘ g)›
    apply (rule continuous_map_eq)
    by (simp add: g'g topspace_pullback_topology)
  then show ?thesis
    apply (rule continuous_map_pullback')
    by (simp add: top1 topspace_pullback_topology)
qed

lemma onorm_case_prod_plus_leq: ‹onorm (case_prod plus :: _ ⇒ 'a::real_normed_vector) ≤ sqrt 2›
  apply (rule onorm_bound)
  using norm_plus_leq_norm_prod by auto

lemma bounded_linear_case_prod_plus[simp]: ‹bounded_linear (case_prod plus)›
  apply (rule bounded_linear_intro[where K=‹sqrt 2›])
  by (auto simp add: scaleR_right_distrib norm_plus_leq_norm_prod mult.commute)

lemma pullback_topology_twice:
  assumes ‹(f -` B) ∩ A = C›
  shows ‹pullback_topology A f (pullback_topology B g T) = pullback_topology C (g o f) T›
proof -
  have aux: ‹S = A ⟷ S = B› if ‹A = B› for A B S :: 'z
    using that by simp
  have *: ‹(∃V. (openin T U ∧ V = g -` U ∩ B) ∧ S = f -` V ∩ A) = (openin T U ∧ S = (g ∘ f) -` U ∩ C)› for S U
    apply (cases ‹openin T U›)
    using assms
    by (auto intro!: aux simp: vimage_comp)
  then have *: ‹(∃V. (∃U. openin T U ∧ V = g -` U ∩ B) ∧ S = f -` V ∩ A) = (∃U. openin T U ∧ S = (g ∘ f) -` U ∩ C)› for S
    by metis
  show ?thesis
    by (auto intro!: * simp: topology_eq openin_pullback_topology)
qed

lemma pullback_topology_homeo_cong:
  assumes ‹homeomorphic_map T S g›
  assumes ‹range f ⊆ topspace T›
  shows ‹pullback_topology A f T = pullback_topology A (g o f) S›
proof -
  have ‹∃Us. openin S Us ∧ f -` Ut ∩ A = (g ∘ f) -` Us ∩ A› if ‹openin T Ut› for Ut
    apply (rule exI[of _ ‹g ` Ut›])
    using assms that apply auto
    using homeomorphic_map_openness_eq apply blast
    by (smt (verit, best) homeomorphic_map_maps homeomorphic_maps_map openin_subset rangeI subsetD)
  moreover have ‹∃Ut. openin T Ut ∧ (g ∘ f) -` Us ∩ A = f -` Ut ∩ A› if ‹openin S Us› for Us
    apply (rule exI[of _ ‹(g -` Us) ∩ topspace T›])
    using assms that apply auto
    by (meson continuous_map_open homeomorphic_imp_continuous_map)
  ultimately show ?thesis
    by (auto simp: topology_eq openin_pullback_topology)
qed

definition ‹opensets_in T = Collect (openin T)›
  ― ‹This behaves more nicely with the @{method transfer}-method (and friends) than \<^const>‹openin›.
      So when rewriting a subgoal, using, e.g., \<^term>‹∃U∈opensets T. xxx› instead of \<^term>‹∃U. openin T U ⟶ xxx› can make @{method transfer} work better. ›

lemma opensets_in_parametric[transfer_rule]:
  includes lifting_syntax
  assumes ‹bi_unique R›
  shows ‹(rel_topology R ===> rel_set (rel_set R)) opensets_in opensets_in›
proof (intro rel_funI rel_setI)
  fix S T
  assume rel_topo: ‹rel_topology R S T›
  fix U
  assume ‹U ∈ opensets_in S›
  then show ‹∃V ∈ opensets_in T. rel_set R U V›
    by (smt (verit, del_insts) Domainp.cases mem_Collect_eq opensets_in_def rel_fun_def rel_topo rel_topology_def)
next
  fix S T assume rel_topo: ‹rel_topology R S T›
  fix U assume ‹U ∈ opensets_in T›
  then show ‹∃V ∈ opensets_in S. rel_set R V U›
    by (smt (verit) RangepE mem_Collect_eq opensets_in_def rel_fun_def rel_topo rel_topology_def)
qed

lemma hausdorff_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique R›
  shows ‹(rel_topology R ===> (⟷)) Hausdorff_space Hausdorff_space›
proof -
  have Hausdorff_space_def': ‹Hausdorff_space T ⟷ (∀x∈topspace T. ∀y∈topspace T. x ≠ y ⟶ (∃U ∈ opensets_in T. ∃V ∈ opensets_in T. x ∈ U ∧ y ∈ V ∧ U ∩ V = {}))›
    for T :: ‹'z topology›
    unfolding opensets_in_def Hausdorff_space_def disjnt_def Bex_def by auto
  show ?thesis
    unfolding Hausdorff_space_def'
    by transfer_prover
qed

lemma sum_cmod_pos: 
  assumes ‹⋀x. x∈A ⟹ f x ≥ 0›
  shows ‹(∑x∈A. cmod (f x)) = cmod (∑x∈A. f x)›
  by (metis (mono_tags, lifting) Re_sum assms cmod_Re sum.cong sum_nonneg)

lemma min_power_distrib_left: ‹(min x y) ^ n = min (x ^ n) (y ^ n)› if ‹x ≥ 0› and ‹y ≥ 0› for x y :: ‹_ :: linordered_semidom›
  by (metis linorder_le_cases min.absorb_iff2 min.order_iff power_mono that(1) that(2))

lemma abs_summable_times: 
  fixes f :: ‹'a ⇒ 'c::{real_normed_algebra}› and g :: ‹'b ⇒ 'c›
  assumes sum_f: ‹f abs_summable_on A›
  assumes sum_g: ‹g abs_summable_on B›
  shows ‹(λ(i,j). f i * g j) abs_summable_on A × B›
proof -
  have a1: ‹(λj. norm (f i) * norm (g j)) abs_summable_on B› if ‹i ∈ A› for i
    using sum_g by (simp add: summable_on_cmult_right)
  then have a2: ‹(λj. f i * g j) abs_summable_on B› if ‹i ∈ A› for i
    apply (rule abs_summable_on_comparison_test)
     apply (fact that)
    by (simp add: norm_mult_ineq)
  from sum_f
  have ‹(λx. ∑⇩∞y∈B. norm (f x) * norm (g y)) abs_summable_on A›
    by (auto simp add: infsum_cmult_right' infsum_nonneg intro!: summable_on_cmult_left)
  then have b1: ‹(λx. ∑⇩∞y∈B. norm (f x * g y)) abs_summable_on A›
    apply (rule abs_summable_on_comparison_test)
    using a1 a2 by (simp_all add: norm_mult_ineq infsum_mono infsum_nonneg)
  from a2 b1 show ?thesis
    by (intro abs_summable_on_Sigma_iff[THEN iffD2]) auto
qed


definition ‹the_default def S = (if card S = 1 then (THE x. x ∈ S) else def)›

lemma card1I:
  assumes "a ∈ A"
  assumes "⋀x. x ∈ A ⟹ x = a"
  shows ‹card A = 1›
  by (metis One_nat_def assms(1) assms(2) card_eq_Suc_0_ex1)

lemma the_default_CollectI:
  assumes "P a"
    and "⋀x. P x ⟹ x = a"
  shows "P (the_default d (Collect P))"
proof -
  have card: ‹card (Collect P) = 1›
    apply (rule card1I)
    using assms by auto
  from assms have ‹P (THE x. P x)›
    by (rule theI)
  then show ?thesis
    by (simp add: the_default_def card)
qed


lemma the_default_singleton[simp]: ‹the_default def {x} = x›
  unfolding the_default_def by auto

lemma the_default_empty[simp]: ‹the_default def {} = def›
  unfolding the_default_def by auto

lemma the_default_The: ‹the_default z S = (THE x. x ∈ S)› if ‹card S = 1›
  by (simp add: that the_default_def)

lemma the_default_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(T ===> rel_set T ===> T) the_default the_default›
proof (intro rel_funI, rename_tac def def' S S')
  fix def def' assume [transfer_rule]: ‹T def def'›
  fix S S' assume [transfer_rule]: ‹rel_set T S S'›
  have card_eq: ‹card S = card S'›
    by transfer_prover
  show ‹T (the_default def S) (the_default def' S')›
  proof (cases ‹card S = 1›)
    case True
    define theS theS' where [no_atp]: ‹theS = (THE x. x ∈ S)› and [no_atp]: ‹theS' = (THE x. x ∈ S')›
    from True have cardS': ‹card S' = 1›
      by (simp add: card_eq)
    have ‹theS ∈ S›
      unfolding theS_def
      by (rule theI') (use True in ‹simp add: card_eq_Suc_0_ex1›)
    moreover have ‹theS' ∈ S'›
      unfolding theS'_def
      by (rule theI') (use cardS' in ‹simp add: card_eq_Suc_0_ex1›)
    ultimately have ‹T theS theS'›
      using ‹rel_set T S S'› True cardS'
      by (auto simp: rel_set_def card_1_singleton_iff)
    then show ?thesis
      by (simp add: True cardS' the_default_def theS_def theS'_def)
  next
    case False
    then have cardS': ‹card S' ≠ 1›
      by (simp add: card_eq)
    show ?thesis
      using False cardS' ‹T def def'›
      by (auto simp add: the_default_def)
  qed
qed

definition ‹rel_pred T P Q = rel_set T (Collect P) (Collect Q)›

lemma Collect_parametric[transfer_rule]:
  includes lifting_syntax
  shows ‹(rel_pred T ===> rel_set T) Collect Collect›
  by (auto simp: rel_pred_def)

lemma fold_graph_finite:
― ‹Exists as @{thm [source] comp_fun_commute_on.fold_graph_finite}, but the
    \<^locale>‹comp_fun_commute_on›-assumption is not needed.›
  assumes "fold_graph f z A y"
  shows "finite A"
  using assms by induct simp_all

lemma fold_graph_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule, simp]: ‹bi_unique T›
  shows ‹((T ===> U ===> U) ===> U ===> rel_set T ===> rel_pred U)
          fold_graph fold_graph›
proof (intro rel_funI, rename_tac f f' z z' A A')
  fix f f' assume [transfer_rule, simp]: ‹(T ===> U ===> U) f f'›
  fix z z' assume [transfer_rule, simp]: ‹U z z'›
  fix A A' assume [transfer_rule, simp]: ‹rel_set T A A'›
  have one_direction: ‹∃y'. fold_graph f' z' A' y' ∧ U y y'› if ‹fold_graph f z A y› 
    and [transfer_rule]: ‹U z z'› ‹(T ===> U ===> U) f f'› ‹rel_set T A A'› ‹bi_unique T›
    for f f' z z' A A' y and U :: ‹'c1 ⇒ 'd1 ⇒ bool› and T :: ‹'a1 ⇒ 'b1 ⇒ bool›
    using ‹fold_graph f z A y›  ‹rel_set T A A'›
  proof (induction arbitrary: A')
    case emptyI
    then show ?case
      by (metis ‹U z z'› empty_iff equals0I fold_graph.intros(1) rel_setD2)
  next
    case (insertI x A y)
    from insertI have foldA: ‹fold_graph f z A y› and T_xA[transfer_rule]: ‹rel_set T (insert x A) A'› and xA: ‹x ∉ A›
      by simp_all
    define DT RT where ‹DT = Collect (Domainp T)› and ‹RT = Collect (Rangep T)›
    from T_xA have ‹x ∈ DT›
      by (metis DT_def DomainPI insertCI mem_Collect_eq rel_set_def)
    then obtain x' where [transfer_rule]: ‹T x x'›
      unfolding DT_def by blast
    have ‹x' ∈ A'›
      apply transfer by simp
    define A'' where ‹A'' = A' - {x'}›
    then have A'_def: ‹A' = insert x' A''›
      using ‹x' ∈ A'› by fastforce
    have ‹x' ∉ A''›
      unfolding A''_def by simp
    have [transfer_rule]: ‹rel_set T A A''›
      apply (subst asm_rl[of ‹A = (insert x A) - {x}›])
      using insertI.hyps apply blast
      unfolding A''_def
      by transfer_prover
    from insertI.IH[OF this]
    obtain y'' where foldA'': ‹fold_graph f' z' A'' y''› and [transfer_rule]: ‹U y y''›
      by auto
    define y' where ‹y' = f' x' y''›
    have ‹fold_graph f' z' A' y'›
      unfolding A'_def y'_def
      using ‹x' ∉ A''› foldA''
      by (rule fold_graph.intros)
    moreover have ‹U (f x y) y'›
      unfolding y'_def by transfer_prover
    ultimately show ?case
      by auto
  qed

  show ‹rel_pred U (fold_graph f z A) (fold_graph f' z' A')›
    unfolding rel_pred_def rel_set_def bex_simps
    apply safe
    subgoal
      by (rule one_direction[of f z A _ U z' T f']) auto
    subgoal
      by (rule one_direction[of f' z' A' _ ‹U¯¯› z ‹T¯¯› f, simplified])
         (auto simp flip: conversep_rel_fun)
    done
qed

lemma Domainp_rel_filter:
  assumes ‹Domainp r = S›
  shows ‹Domainp (rel_filter r) F ⟷ (F ≤ principal (Collect S))›
proof (intro iffI, elim Domainp.cases, hypsubst)
  fix G 
  assume ‹rel_filter r F G›
  then obtain Z where rZ: ‹∀⇩F (x, y) in Z. r x y›
    and ZF: "map_filter_on {(x, y). r x y} fst Z = F" 
    and "map_filter_on {(x, y). r x y} snd Z = G"
    using rel_filter.simps by blast
  show ‹F ≤ principal (Collect S)›
    using rZ 
    by (auto simp flip: ZF assms intro!: filter_leI  elim!: eventually_mono
             simp: eventually_principal eventually_map_filter_on case_prod_unfold DomainPI)
next
  assume asm: ‹F ≤ principal (Collect S)›
  define Z where ‹Z = inf (filtercomap fst F) (principal {(x, y). r x y})›
  have rZ: ‹∀⇩F (x, y) in Z. r x y›
    by (simp add: Z_def eventually_inf_principal)
  moreover 
  have ‹(∀⇩F x in Z. P (fst x) ∧ (case x of (x, xa) ⇒ r x xa)) = eventually P F› for P
    using asm apply (auto simp add: le_principal Z_def eventually_inf_principal eventually_filtercomap)
    by (smt (verit, del_insts) DomainpE assms eventually_elim2)
  then have ‹map_filter_on {(x, y). r x y} fst Z = F›
    by (simp add: filter_eq_iff eventually_map_filter_on rZ)
  ultimately show ‹Domainp (rel_filter r) F›
    by (auto simp: Domainp_iff intro!: exI rel_filter.intros)
qed


lemma map_filter_on_cong:
  assumes [simp]: ‹∀⇩F x in F. x ∈ D›
  assumes ‹⋀x. x ∈ D ⟹ f x = g x›
  shows ‹map_filter_on D f F = map_filter_on D g F›
  apply (rule filter_eq_iff[THEN iffD2, rule_format])
  apply (simp add: eventually_map_filter_on)
  apply (rule eventually_subst)
  apply (rule always_eventually)
  using assms(2) by auto 


lemma filtermap_cong: 
  assumes ‹∀⇩F x in F. f x = g x›
  shows ‹filtermap f F = filtermap g F›
  apply (rule filter_eq_iff[THEN iffD2, rule_format])
  apply (simp add: eventually_filtermap)
  by (smt (verit, del_insts) assms eventually_elim2)

lemma filtermap_INF_eq: 
  assumes inj_f: ‹inj_on f X›
  assumes B_nonempty: ‹B ≠ {}›
  assumes F_bounded: ‹⋀b. b∈B ⟹ F b ≤ principal X›
  shows ‹filtermap f (⨅ (F ` B)) = (⨅b∈B. filtermap f (F b))›
proof (rule antisym)
  show ‹filtermap f (⨅ (F ` B)) ≤ (⨅b∈B. filtermap f (F b))›
    by (rule filtermap_INF)
  define f1 where ‹f1 = inv_into X f›
  have f1f: ‹x ∈ X ⟹ f1 (f x) = x› for x
    by (simp add: inj_f f1_def)
  have ff1: ‹x ∈ f ` X ⟹ x = f (f1 x)› for x
    by (simp add: f1_def f_inv_into_f)

  have ‹filtermap f (F b) ≤ principal (f ` X)› if ‹b ∈ B› for b
    by (metis F_bounded filtermap_mono filtermap_principal that)
  then have ‹(⨅b∈B. filtermap f (F b)) ≤ (⨅b∈B. principal (f ` X))›
    by (simp add: INF_greatest INF_lower2) 
  also have ‹… = principal (f ` X)›
    by (simp add: B_nonempty)
  finally have ‹∀⇩F x in ⨅b∈B. filtermap f (F b). x ∈ f ` X›
    using B_nonempty le_principal by auto
  then have *: ‹∀⇩F x in ⨅b∈B. filtermap f (F b). x = f (f1 x)›
    apply (rule eventually_mono)
    by (simp add: ff1)

  have ‹∀⇩F x in F b. x ∈ X› if ‹b ∈ B› for b
    using F_bounded le_principal that by blast
  then have **: ‹∀⇩F x in F b. f1 (f x) = x› if ‹b ∈ B› for b
    apply (rule eventually_mono)
    using that by (simp_all add: f1f)

  have ‹(⨅b∈B. filtermap f (F b)) = filtermap f (filtermap f1 (⨅b∈B. filtermap f (F b)))›
    apply (simp add: filtermap_filtermap)
    using * by (rule filtermap_cong[where f=id, simplified])
  also have ‹… ≤ filtermap f (⨅b∈B. filtermap f1 (filtermap f (F b)))›
    apply (rule filtermap_mono)
    by (rule filtermap_INF)
  also have ‹… = filtermap f (⨅b∈B. F b)›
    apply (rule arg_cong[where f=‹filtermap _›])
    apply (rule INF_cong, rule refl)
    unfolding filtermap_filtermap
    using ** by (rule filtermap_cong[where g=id, simplified])
  finally show ‹(⨅b∈B. filtermap f (F b)) ≤ filtermap f (⨅ (F ` B))›
    by -
qed

lemma filtermap_inf_eq:
  assumes ‹inj_on f X›
  assumes ‹F1 ≤ principal X›
  assumes ‹F2 ≤ principal X›
  shows ‹filtermap f (F1 ⊓ F2) = filtermap f F1 ⊓ filtermap f F2›
proof -
  have ‹filtermap f (F1 ⊓ F2) = filtermap f (INF F∈{F1,F2}. F)›
    by simp
  also have ‹… = (INF F∈{F1,F2}. filtermap f F)›
    apply (rule filtermap_INF_eq[where X=X])
    using assms by auto
  also have ‹… = filtermap f F1 ⊓ filtermap f F2›
    by simp
  finally show ?thesis
    by -
qed


definition ‹transfer_bounded_filter_Inf B M = Inf M ⊓ principal B›

lemma Inf_transfer_bounded_filter_Inf: ‹Inf M = transfer_bounded_filter_Inf UNIV M›
  by (metis inf_top.right_neutral top_eq_principal_UNIV transfer_bounded_filter_Inf_def)

lemma Inf_bounded_transfer_bounded_filter_Inf:
  assumes ‹⋀F. F ∈ M ⟹ F ≤ principal B›
  assumes ‹M ≠ {}›
  shows ‹Inf M = transfer_bounded_filter_Inf B M›
  by (simp add: Inf_less_eq assms(1) assms(2) inf_absorb1 transfer_bounded_filter_Inf_def)


lemma transfer_bounded_filter_Inf_parametric[transfer_rule]:
  includes lifting_syntax
  fixes r :: ‹'rep ⇒ 'abs ⇒ bool›
  assumes [transfer_rule]: ‹bi_unique r›
  shows ‹(rel_set r ===> rel_set (rel_filter r) ===> rel_filter r)
     transfer_bounded_filter_Inf transfer_bounded_filter_Inf›
proof (intro rel_funI, unfold transfer_bounded_filter_Inf_def)
  fix BF BG assume BFBG[transfer_rule]: ‹rel_set r BF BG›
  fix Fs Gs assume FsGs[transfer_rule]: ‹rel_set (rel_filter r) Fs Gs›
  define D R where ‹D = Collect (Domainp r)› and ‹R = Collect (Rangep r)›
  
  have ‹rel_set r D R›
     by (smt (verit) D_def Domainp_iff R_def RangePI Rangep.cases mem_Collect_eq rel_setI)
  with ‹bi_unique r›
  obtain f where ‹R = f ` D› and [simp]: ‹inj_on f D› and rf0: ‹x∈D ⟹ r x (f x)› for x
    using bi_unique_rel_set_lemma
    by metis
  have rf: ‹r x y ⟷ x ∈ D ∧ f x = y› for x y
    apply (auto simp: rf0)
    using D_def apply auto[1]
    using D_def assms bi_uniqueDr rf0 by fastforce

  from BFBG
  have ‹BF ⊆ D›
     by (metis rel_setD1 rf subsetI)

  have G: ‹G = filtermap f F› if ‹rel_filter r F G› for F G
    using that proof cases
    case (1 Z)
    then have Z[simp]: ‹∀⇩F (x, y) in Z. r x y›
      by -
    then have ‹filtermap f F = filtermap f (map_filter_on {(x, y). r x y} fst Z)›
      using 1 by simp
    also have ‹… = map_filter_on {(x, y). r x y} (f ∘ fst) Z›
      unfolding map_filter_on_UNIV[symmetric]
      apply (subst map_filter_on_comp)
      using Z by simp_all
    also have ‹… = G›
      apply (simp add: o_def rf)
      apply (subst map_filter_on_cong[where g=snd])
      using Z apply (rule eventually_mono)
      using 1 by (auto simp: rf)
    finally show ?thesis
      by simp
  qed

  have rf_filter: ‹rel_filter r F G ⟷ F ≤ principal D ∧ filtermap f F = G› for F G
    apply (intro iffI conjI)
      apply (metis D_def DomainPI Domainp_rel_filter)
    using G apply simp
    by (metis D_def Domainp_iff Domainp_rel_filter G)

  have FD: ‹F ≤ principal D› if ‹F ∈ Fs› for F
    by (meson FsGs rel_setD1 rf_filter that)

  from BFBG
  have [simp]: ‹BG = f ` BF›
    by (auto simp: rel_set_def rf)

  from FsGs
  have [simp]: ‹Gs = filtermap f ` Fs›
    using G apply (auto simp: rel_set_def rf)
    by fastforce

  show ‹rel_filter r (⨅ Fs ⊓ principal BF) (⨅ Gs ⊓ principal BG)›
  proof (cases ‹Fs = {}›)
    case True
    then have ‹Gs = {}›
      by transfer
    have ‹rel_filter r (principal BF) (principal BG)›
      by transfer_prover
    with True ‹Gs = {}› show ?thesis
      by simp
  next
    case False
    note False[simp]
    then have [simp]: ‹Gs ≠ {}›
      by transfer
    have ‹rel_filter r (⨅ Fs ⊓ principal BF) (filtermap f (⨅ Fs ⊓ principal BF))›
      apply (rule rf_filter[THEN iffD2])
      by (simp add: ‹BF ⊆ D› le_infI2)
    then show ?thesis
      using FD ‹BF ⊆ D›
      by (simp add: Inf_less_eq 
          flip: filtermap_inf_eq[where X=D] filtermap_INF_eq[where X=D] flip: filtermap_principal)
  qed
qed


definition ‹transfer_inf_principal F M = F ⊓ principal M›

lemma transfer_inf_principal_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(rel_filter T ===> rel_set T ===> rel_filter T) transfer_inf_principal transfer_inf_principal›
proof -
  have *: ‹transfer_inf_principal F M = transfer_bounded_filter_Inf M {F}› for F :: ‹'z filter› and M
    by (simp add: transfer_inf_principal_def[abs_def] transfer_bounded_filter_Inf_def)
  show ?thesis
    unfolding * 
    apply transfer_prover_start
    apply transfer_step+
    by transfer_prover
qed


lemma continuous_map_is_continuous_at_point:
  assumes ‹continuous_map T U f›
  shows ‹filterlim f (nhdsin U (f l)) (atin T l)›
  by (metis assms atin_degenerate bot.extremum continuous_map_atin filterlim_iff_le_filtercomap filterlim_nhdsin_iff_limitin)

lemma set_compr_2_image_collect: ‹{f x y |x y. P x y} = case_prod f ` Collect (case_prod P)›
  by fast

lemma closure_image_closure: ‹continuous_on (closure S) f ⟹ closure (f ` closure S) = closure (f ` S)›
  by (smt (verit) closed_closure closure_closure closure_mono closure_subset image_closure_subset image_mono set_eq_subset)


lemma has_sum_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "((λx. f (g x)) has_sum l) A ⟷ (f has_sum l) B"
proof -
  have ‹((λx. f (g x)) has_sum l) A ⟷ (f has_sum l) (g ` A)›
    apply (rule has_sum_reindex[symmetric, unfolded o_def])
    using assms bij_betw_imp_inj_on by blast
  also have ‹… ⟷ (f has_sum l) B›
    using assms bij_betw_imp_surj_on by blast
  finally show ?thesis .
qed

lemma enum_inj:
  assumes "i < CARD('a)" and "j < CARD('a)"
  shows "(Enum.enum ! i :: 'a::enum) = Enum.enum ! j ⟷ i = j"
  using inj_on_nth[OF enum_distinct, where I=‹{..<CARD('a)}›]
  using assms by (auto dest: inj_onD simp flip: card_UNIV_length_enum)

lemma closedin_vimage:
  assumes ‹closedin U S›
  assumes ‹continuous_map T U f›
  shows ‹closedin T (topspace T ∩ (f -` S))›
  by (meson assms(1) assms(2) continuous_map_closedin_preimage_eq)

lemma join_forall: ‹(∀x. P x) ∧ (∀x. Q x) ⟷ (∀x. P x ∧ Q x)›
  by auto

lemma closedin_if_converge_inside:
  fixes A :: ‹'a set›
  assumes AT: ‹A ⊆ topspace T›
  assumes xA: ‹⋀(F::'a filter) f x. F ≠ ⊥ ⟹ limitin T f x F ⟹ range f ⊆ A ⟹ x ∈ A›
  shows ‹closedin T A›
proof (cases ‹A = {}›)
  case True
  then show ?thesis by simp
next
  case False
  then obtain a where ‹a ∈ A›
    by auto
  define Ac where ‹Ac = topspace T - A›
  have ‹∃U. openin T U ∧ x ∈ U ∧ U ⊆ Ac› if ‹x ∈ Ac› for x
  proof (rule ccontr)
    assume ‹∄U. openin T U ∧ x ∈ U ∧ U ⊆ Ac›
    then have UA: ‹U ∩ A ≠ {}› if ‹openin T U›and ‹x ∈ U› for U
      by (metis Ac_def Diff_mono Diff_triv openin_subset subset_refl that)
    have [simp]: ‹x ∈ topspace T›
      using that by (simp add: Ac_def)

    define F where ‹F = nhdsin T x ⊓ principal A›
    have ‹F ≠ ⊥›
      apply (subst filter_eq_iff)
      apply (auto intro!: exI[of _ ‹λ_. False›] simp: F_def eventually_inf eventually_principal
          eventually_nhdsin)
      by (meson UA disjoint_iff)

    define f where ‹f y = (if y∈A then y else a)› for y
    with ‹a ∈ A› have ‹range f ⊆ A›
      by force

    have ‹∀⇩F y in F. f y ∈ U› if ‹openin T U› and ‹x ∈ U› for U
    proof -
      have ‹eventually (λx. x ∈ U) (nhdsin T x)›
        using eventually_nhdsin that by fastforce
      moreover have ‹∃R. (∀x∈A. R x) ∧ (∀x. x ∈ U ⟶ R x ⟶ f x ∈ U)›
        apply (rule exI[of _ ‹λx. x ∈ A›])
        by (simp add: f_def)
      ultimately show ?thesis
        by (auto simp add: F_def eventually_inf eventually_principal)
    qed
    then have ‹limitin T f x F›
      unfolding limitin_def by simp
    with ‹F ≠ ⊥› ‹range f ⊆ A› xA
    have ‹x ∈ A›
      by simp
    with that show False
      by (simp add: Ac_def)
  qed
  then have ‹openin T Ac›
    apply (rule_tac openin_subopen[THEN iffD2])
    by simp
  then show ?thesis
    by (simp add: Ac_def AT closedin_def)
qed

lemma cmod_mono: ‹0 ≤ a ⟹ a ≤ b ⟹ cmod a ≤ cmod b›
  by (simp add: cmod_Re less_eq_complex_def)

lemma choice2: ‹∃f. (∀x. Q1 x (f x)) ∧ (∀x. Q2 x (f x))›
  if ‹∀x. ∃y. Q1 x y ∧ Q2 x y›
  by (meson that)

lemma choice3: ‹∃f. (∀x. Q1 x (f x)) ∧ (∀x. Q2 x (f x)) ∧ (∀x. Q3 x (f x))›
  if ‹∀x. ∃y. Q1 x y ∧ Q2 x y ∧ Q3 x y›
  by (meson that)

lemma choice4: ‹∃f. (∀x. Q1 x (f x)) ∧ (∀x. Q2 x (f x)) ∧ (∀x. Q3 x (f x)) ∧ (∀x. Q4 x (f x))›
  if ‹∀x. ∃y. Q1 x y ∧ Q2 x y ∧ Q3 x y ∧ Q4 x y›
  by (meson that)

lemma choice5: ‹∃f. (∀x. Q1 x (f x)) ∧ (∀x. Q2 x (f x)) ∧ (∀x. Q3 x (f x)) ∧ (∀x. Q4 x (f x)) ∧ (∀x. Q5 x (f x))›
  if ‹∀x. ∃y. Q1 x y ∧ Q2 x y ∧ Q3 x y ∧ Q4 x y ∧ Q5 x y›
  apply (simp only: flip: all_conj_distrib)
  using that by (rule choice)

lemma is_Sup_unique: ‹is_Sup X a ⟹ is_Sup X b ⟹ a=b›
  by (simp add: Orderings.order_eq_iff is_Sup_def)

lemma has_Sup_bdd_above: ‹has_Sup X ⟹ bdd_above X›
  by (metis bdd_above.unfold has_Sup_def is_Sup_def)

lemma is_Sup_has_Sup: ‹is_Sup X s ⟹ has_Sup X›
  using has_Sup_def by blast

class Sup_order = order + Sup + sup +
  assumes is_Sup_Sup: ‹has_Sup X ⟹ is_Sup X (Sup X)›
  assumes is_Sup_sup: ‹has_Sup {x,y} ⟹ is_Sup {x,y} (sup x y)›

lemma (in Sup_order) is_Sup_eq_Sup:
  assumes ‹is_Sup X s›
  shows ‹s = Sup X›
  by (meson assms local.dual_order.antisym local.has_Sup_def local.is_Sup_Sup local.is_Sup_def)

lemma is_Sup_cSup:
  fixes X :: ‹'a::conditionally_complete_lattice set›
  assumes ‹bdd_above X› and ‹X ≠ {}›
  shows ‹is_Sup X (Sup X)›
  using assms by (auto intro!: cSup_upper cSup_least simp: is_Sup_def)

lemma continuous_map_iff_preserves_convergence:
  assumes ‹⋀F a. a ∈ topspace T ⟹ limitin T id a F ⟹ limitin U f (f a) F›
  shows ‹continuous_map T U f›
  apply (rule continuous_map_atin[THEN iffD2], intro ballI)
  using assms
  by (simp add: limitin_continuous_map)


lemma SMT_choices:
  ― ‹Was included as SMT.choices in Isabelle and disappeared›
  "⋀Q. ∀x. ∃y ya. Q x y ya ⟹ ∃f fa. ∀x. Q x (f x) (fa x)"
  "⋀Q. ∀x. ∃y ya yb. Q x y ya yb ⟹ ∃f fa fb. ∀x. Q x (f x) (fa x) (fb x)"
  "⋀Q. ∀x. ∃y ya yb yc. Q x y ya yb yc ⟹ ∃f fa fb fc. ∀x. Q x (f x) (fa x) (fb x) (fc x)"
  "⋀Q. ∀x. ∃y ya yb yc yd. Q x y ya yb yc yd ⟹
     ∃f fa fb fc fd. ∀x. Q x (f x) (fa x) (fb x) (fc x) (fd x)"
  "⋀Q. ∀x. ∃y ya yb yc yd ye. Q x y ya yb yc yd ye ⟹
     ∃f fa fb fc fd fe. ∀x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)"
  "⋀Q. ∀x. ∃y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf ⟹
     ∃f fa fb fc fd fe ff. ∀x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)"
  "⋀Q. ∀x. ∃y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg ⟹
     ∃f fa fb fc fd fe ff fg. ∀x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)"
  by metis+


lemma closedin_pullback_topology:
  "closedin (pullback_topology A f T) S ⟷ (∃C. closedin T C ∧ S = f-`C ∩ A)"
proof (rule iffI)
  define TT PT where ‹TT = topspace T› and ‹PT = topspace (pullback_topology A f T)›
  assume closed: ‹closedin (pullback_topology A f T) S›
  then have ‹S ⊆ PT›
    using PT_def closedin_subset by blast
  from closed have ‹openin (pullback_topology A f T) (PT - S)›
    by (auto intro!: simp: closedin_def PT_def)
  then obtain U where ‹openin T U› and S_fUA: ‹PT - S = f -` U ∩ A›
    by (auto simp: openin_pullback_topology)
  define C where ‹C = TT - U›
  have ‹closedin T C›
    using C_def TT_def ‹openin T U› by blast
  moreover have ‹S = f -` C ∩ A›
    using S_fUA ‹S ⊆ PT›
    apply (simp only: C_def PT_def TT_def)
    by (metis Diff_Diff_Int Diff_Int_distrib2  inf.absorb_iff2 topspace_pullback_topology vimage_Diff)
  ultimately show ‹∃C. closedin T C ∧ S = f -` C ∩ A›
    by auto
next
  assume ‹∃U. closedin T U ∧ S = f -` U ∩ A›
  then show ‹closedin (pullback_topology A f T) S›
    apply (simp add: openin_pullback_topology closedin_def topspace_pullback_topology)
    by blast
qed


lemma regular_space_pullback[intro]:
  assumes ‹regular_space T›
  shows ‹regular_space (pullback_topology A f T)›
proof (unfold regular_space_def, intro allI impI)
  define TT PT where ‹TT = topspace T› and ‹PT = topspace (pullback_topology A f T)›
  fix S y
  assume asm: ‹closedin (pullback_topology A f T) S ∧ y ∈ PT - S›
  from asm obtain C where ‹closedin T C› and S_fCA: ‹S = f -` C ∩ A›
    by (auto simp: closedin_pullback_topology)
  from asm S_fCA
  have ‹f y ∈ TT - C›
    by (auto simp: PT_def TT_def topspace_pullback_topology)
  then obtain U' V' where ‹openin T U'› and ‹openin T V'› and ‹f y ∈ U'› and ‹C ⊆ V'› and ‹U' ∩ V' = {}›
    by (metis TT_def ‹closedin T C› assms regular_space_def disjnt_def)
  define U V where ‹U = f -` U' ∩ A› and ‹V = f -` V' ∩ A›
  have ‹openin (pullback_topology A f T) U›
    using U_def ‹openin T U'› openin_pullback_topology by blast
  moreover have ‹openin (pullback_topology A f T) V›
    using V_def ‹openin T V'› openin_pullback_topology by blast
  moreover have ‹y ∈ U›
    by (metis DiffD1 Int_iff PT_def U_def ‹f y ∈ U'› asm topspace_pullback_topology vimageI)
  moreover have ‹S ⊆ V›
    using S_fCA V_def ‹C ⊆ V'› by blast
  moreover have ‹disjnt U V›
    using U_def V_def ‹U' ∩ V' = {}› disjnt_def by blast

  ultimately show ‹∃U V. openin (pullback_topology A f T) U ∧ openin (pullback_topology A f T) V ∧ y ∈ U ∧ S ⊆ V ∧ disjnt U V›
    apply (rule_tac exI[of _ U], rule_tac exI[of _ V])
    by auto
qed

lemma t3_space_euclidean_regular[iff]: ‹regular_space (euclidean :: 'a::t3_space topology)›
  using t3_space
  apply (simp add: regular_space_def disjnt_def)
  by fast

definition increasing_filter :: ‹'a::order filter ⇒ bool› where
  ― ‹Definition suggested by \<^cite>‹"increasing-filters"››
  ‹increasing_filter F ⟷ (∀⇩F x in F. ∀⇩F y in F. y ≥ x)›

lemma increasing_filtermap:
  fixes F :: ‹'a::order filter› and f :: ‹'a ⇒ 'b::order› and X :: ‹'a set›
  assumes increasing: ‹increasing_filter F›
  assumes mono: ‹mono_on X f›
  assumes ev_X: ‹eventually (λx. x ∈ X) F›
  shows ‹increasing_filter (filtermap f F)›
proof -
  from increasing
  have incr: ‹∀⇩F x in F. ∀⇩F y in F. x ≤ y›
    apply (simp add: increasing_filter_def)
    by -
  have ‹∀⇩F x in F. ∀⇩F y in F. f x ≤ f y›
  proof (rule eventually_elim2[OF ev_X incr])
    fix x
    assume ‹x ∈ X›
    assume ‹∀⇩F y in F. x ≤ y›
    then show ‹∀⇩F y in F. f x ≤ f y›
    proof (rule eventually_elim2[OF ev_X])
      fix y assume ‹y ∈ X› and ‹x ≤ y›
      with ‹x ∈ X› show ‹f x ≤ f y›
        using mono by (simp add: mono_on_def)
    qed
  qed
  then show ‹increasing_filter (filtermap f F)›
    by (simp add: increasing_filter_def eventually_filtermap)
qed

lemma increasing_finite_subsets_at_top[simp]: ‹increasing_filter (finite_subsets_at_top X)›
  apply (simp add: increasing_filter_def eventually_finite_subsets_at_top)
  by force

lemma monotone_convergence:
  ― ‹Following \<^cite>‹"increasing-filters"››
  fixes f :: ‹'b ⇒ 'a::{order_topology, conditionally_complete_linorder}›
  assumes bounded: ‹∀⇩F x in F. f x ≤ B›
  assumes increasing: ‹increasing_filter (filtermap f F)›
  shows ‹∃l. (f ⤏ l) F›
proof (cases ‹F ≠ ⊥›)
  case True
  note [simp] = True
  define S l where ‹S x ⟷ (∀⇩F y in F. f y ≥ x) ∧ x ≤ B› 
    and ‹l = Sup (Collect S)› for x
  from bounded increasing
  have ev_S: ‹eventually S (filtermap f F)›
    by (auto intro!: eventually_conj simp: S_def[abs_def] increasing_filter_def eventually_filtermap)
  have bdd_S: ‹bdd_above (Collect S)›
    by (auto simp: S_def)
  have S_nonempty: ‹Collect S ≠ {}›
    using ev_S
    by (metis Collect_empty_eq_bot Set.empty_def True eventually_False filtermap_bot_iff)
  have ‹(f ⤏ l) F›
  proof (rule order_tendstoI; rename_tac x)
    fix x
    assume ‹x < l›
    then obtain s where ‹S s› and ‹x < s›
      using less_cSupD[OF S_nonempty] l_def
      by blast
    then 
    show ‹∀⇩F y in F. x < f y›
      using S_def basic_trans_rules(22) eventually_mono by force
  next
    fix x
    assume asm: ‹l < x›
    from ev_S
    show ‹∀⇩F y in F. f y < x›
      unfolding eventually_filtermap
      apply (rule eventually_mono)
      using asm
      by (metis bdd_S cSup_upper dual_order.strict_trans2 l_def mem_Collect_eq)
  qed
  then show ‹∃l. (f ⤏ l) F›
    by (auto intro!: exI[of _ l] simp: filterlim_def)
next
  case False
  then show ‹∃l. (f ⤏ l) F›
    by (auto intro!: exI)
qed


lemma monotone_convergence_complex:
  fixes f :: ‹'b ⇒ complex›
  assumes bounded: ‹∀⇩F x in F. f x ≤ B›
  assumes increasing: ‹increasing_filter (filtermap f F)›
  shows ‹∃l. (f ⤏ l) F›
proof -
  have inc_re: ‹increasing_filter (filtermap (λx. Re (f x)) F)›
    using increasing_filtermap[OF increasing, where f=Re and X=UNIV]
    by (simp add: less_eq_complex_def[abs_def] mono_def monotone_def filtermap_filtermap)
  from bounded have ‹∀⇩F x in F. Re (f x) ≤ Re B›
    using eventually_mono less_eq_complex_def by fastforce
  from monotone_convergence[OF this inc_re]
  obtain re where lim_re: ‹((λx. Re (f x)) ⤏ re) F›
    by auto
  from bounded have ‹∀⇩F x in F. Im (f x) = Im B›
    by (simp add: less_eq_complex_def[abs_def] eventually_mono)
  then have lim_im: ‹((λx. Im (f x)) ⤏ Im B) F›
    by (simp add: tendsto_eventually)
  from lim_re lim_im have ‹(f ⤏ Complex re (Im B)) F›
    by (simp add: tendsto_complex_iff)
  then show ?thesis
    by auto
qed

lemma compact_closed_subset:
  assumes ‹compact s›
  assumes ‹closed t›
  assumes ‹t ⊆ s›
  shows ‹compact t›
  by (metis assms(1) assms(2) assms(3) compact_Int_closed inf.absorb_iff2)

definition separable where ‹separable S ⟷ (∃B. countable B ∧ S ⊆ closure B)›

lemma compact_imp_separable: ‹separable S› if ‹compact S› for S :: ‹'a::metric_space set›
proof -
  from that
  obtain K where ‹finite (K n)› and K_cover_S: ‹S ⊆ (⋃k∈K n. ball k (1 / of_nat (n+1)))› for n :: nat
  proof (atomize_elim, intro choice2 allI)
    fix n
    have ‹S ⊆ (⋃k∈UNIV. ball k (1 / of_nat (n+1)))›
      apply (auto intro!: simp: )
      by (smt (verit, del_insts) dist_eq_0_iff linordered_field_class.divide_pos_pos of_nat_less_0_iff)
    then show ‹∃K. finite K ∧ S ⊆ (⋃k∈K. ball k (1 / real (n + 1)))›
      apply (simp add: compact_eq_Heine_Borel)
      by (meson Elementary_Metric_Spaces.open_ball compactE_image ‹compact S›)
  qed
  define B where ‹B = (⋃n. K n)›
  have ‹countable B›
    using B_def ‹finite (K _)› uncountable_infinite by blast
  have ‹S ⊆ closure B›
  proof (intro subsetI closure_approachable[THEN iffD2, rule_format])
    fix x assume ‹x ∈ S›
    fix e :: real assume ‹e > 0›
    define n :: nat where ‹n = nat (ceiling (1/e))›
    with ‹e > 0› have ne: ‹1 / real (n+1) ≤ e›
    proof -
      have ‹1 / real (n+1) ≤ 1 / ceiling (1/e)›
        by (simp add: ‹0 < e› linordered_field_class.frac_le n_def)
      also have ‹… ≤ 1 / (1/e)›
        by (smt (verit, del_insts) ‹0 < e› le_of_int_ceiling linordered_field_class.divide_pos_pos linordered_field_class.frac_le)
      also have ‹… = e›
        by simp
      finally show ?thesis
        by -
    qed
    have ‹S ⊆ (⋃k∈K n. ball k (1 / of_nat (n+1)))›
      using K_cover_S by presburger
    then obtain k where ‹k ∈ K n› and x_ball: ‹x ∈ ball k (1 / of_nat (n+1))›
      using ‹x ∈ S› by auto
    from ‹k ∈ K n› have ‹k ∈ B›
      using B_def by blast
    moreover from x_ball have ‹dist k x < e›
      by (smt (verit) ne mem_ball)
    ultimately show ‹∃k∈B. dist k x < e›
      by fast
  qed
  show ‹separable S›
    using ‹S ⊆ closure B› ‹countable B› separable_def by blast
qed

lemma infsum_single: 
  assumes "⋀j. j ≠ i ⟹ j∈A ⟹ f j = 0"
  shows "infsum f A = (if i∈A then f i else 0)"
  apply (subst infsum_cong_neutral[where T=‹A ∩ {i}› and g=f])
  using assms by auto

lemma suminf_eqI:
  fixes x :: ‹_::{comm_monoid_add,t2_space}›
  assumes ‹f sums x›
  shows ‹suminf f = x›
  using assms
  by (auto intro!: simp: sums_iff)

lemma suminf_If_finite_set:
  fixes f :: ‹_ ⇒ _::{comm_monoid_add,t2_space}›
  assumes ‹finite F›
  shows ‹(∑x∈F. f x) = (∑x. if x∈F then f x else 0)›
  by (auto intro!: suminf_eqI[symmetric] sums_If_finite_set simp: assms)



lemma tendsto_le_complex:
  fixes x y :: complex
  assumes F: "¬ trivial_limit F"
    and x: "(f ⤏ x) F"
    and y: "(g ⤏ y) F"
    and ev: "eventually (λx. g x ≤ f x) F"
  shows "y ≤ x"
proof (rule less_eq_complexI)
  note F
  moreover have ‹((λx. Re (f x)) ⤏ Re x) F›
    by (simp add: assms tendsto_Re)
  moreover have ‹((λx. Re (g x)) ⤏ Re y) F›
    by (simp add: assms tendsto_Re)
  moreover from ev have "eventually (λx. Re (g x) ≤ Re (f x)) F"
    apply (rule eventually_mono)
    by (simp add: less_eq_complex_def)
  ultimately show ‹Re y ≤ Re x›
    by (rule tendsto_le)
next
  note F
  moreover have ‹((λx. Im (g x)) ⤏ Im y) F›
    by (simp add: assms tendsto_Im)
  moreover 
  have ‹((λx. Im (g x)) ⤏ Im x) F›
  proof -
    have ‹((λx. Im (f x)) ⤏ Im x) F›
      by (simp add: assms tendsto_Im)
    moreover from ev have ‹∀⇩F x in F. Im (f x) = Im (g x)›
      apply (rule eventually_mono)
      by (simp add: less_eq_complex_def)
    ultimately show ?thesis
      by (rule Lim_transform_eventually)
  qed
  ultimately show ‹Im y = Im x›
    by (rule tendsto_unique)
qed

lemma bdd_above_mono2:
  assumes ‹bdd_above (g ` B)›
  assumes ‹A ⊆ B›
  assumes ‹⋀x. x ∈ A ⟹ f x ≤ g x›
  shows ‹bdd_above (f ` A)›
  by (smt (verit, del_insts) Set.basic_monos(7) assms(1) assms(2) assms(3) basic_trans_rules(23) bdd_above.I2 bdd_above.unfold imageI)


lemma infsum_product:
  fixes f :: ‹'a ⇒ 'c :: {topological_semigroup_mult,division_ring,banach}›
  assumes ‹(λ(x, y). f x * g y) summable_on X × Y›
  shows ‹(∑⇩∞x∈X. f x) * (∑⇩∞y∈Y. g y) = (∑⇩∞(x,y)∈X×Y. f x * g y)›
  using assms
  by (simp add: infsum_cmult_right' infsum_cmult_left' flip: infsum_Sigma'_banach)

lemma infsum_product':
  fixes f :: ‹'a ⇒ 'c :: {banach,times,real_normed_algebra}› and g :: ‹'b ⇒ 'c›
  assumes ‹f abs_summable_on X›
  assumes ‹g abs_summable_on Y›
  shows ‹(∑⇩∞x∈X. f x) * (∑⇩∞y∈Y. g y) = (∑⇩∞(x,y)∈X×Y. f x * g y)›
  using assms
  by (simp add: abs_summable_times infsum_cmult_right infsum_cmult_left abs_summable_summable flip: infsum_Sigma'_banach)

lemma infsum_bounded_linear_invertible:
  assumes ‹bounded_linear h›
  assumes ‹bounded_linear h'›
  assumes ‹h' o h = id›
  shows ‹infsum (λx. h (f x)) A = h (infsum f A)›
proof (cases ‹f summable_on A›)
  case True
  then show ?thesis
    using assms(1) infsum_bounded_linear by blast
next
  case False
  have ‹¬ (λx. h (f x)) summable_on A›
  proof (rule ccontr)
    assume ‹¬ ¬ (λx. h (f x)) summable_on A›
    with ‹bounded_linear h'› have ‹h' o h o f summable_on A›
      by (auto intro: summable_on_bounded_linear simp: o_def)
    then have ‹f summable_on A›
      by (simp add: assms(3))
    with False show False
      by blast
  qed
  then show ?thesis
    by (simp add: False assms(1) infsum_not_exists linear_simps(3))
qed


lemma summable_on_bdd_above_real: ‹bdd_above (f ` M)› if ‹f summable_on M› for f :: ‹'a ⇒ real›
proof -
  from that have ‹f abs_summable_on M›
    unfolding summable_on_iff_abs_summable_on_real[symmetric]
    by -
  then have ‹bdd_above (sum (λx. norm (f x)) ` {F. F ⊆ M ∧ finite F})›
    unfolding abs_summable_iff_bdd_above by simp
  then have ‹bdd_above (sum (λx. norm (f x)) ` (λx. {x}) ` M)›
    by (rule bdd_above_mono) auto
  then have ‹bdd_above ((λx. norm (f x)) ` M)›
    by (simp add: image_image)
  then show ?thesis
    by (simp add: bdd_above_mono2)
qed


end