infinite product clash with type product

Stream: general

[Yakov Pechersky]

We currently have docs#tsum for infinite sums, and docs#list.tprod for type products. If we wanted to have infinite products, what should we do?

[Eric Wieser]

(polls have to be in their own message)

[Yakov Pechersky]

/poll Infinite products
Use infinite products in terms of additive and multiplicative of tsum
Use infinite products in terms of tendsto like we have for a lemma about sin x (Thanks @Eric Wieser )
Rename tprod to typrod or tproductor something else
Define infinite product as topprod, toprod, topoprod, and extend to_additive

[Reid Barton]

tprod doesn't seem to exist.

[Eric Wieser]

docs#list.tprod?

[Eric Wieser]

But that doesn't conflict, so perhaps the only question here is "should we to_additivize a bunch of things"

[Reid Barton]

Weird that the find/ results didn't consider that worthy of a mention.

[Yakov Pechersky]

Sorry, which find/ results do you mean? Please feel free to add an option

[Reid Barton]

Try clicking the second link in your original message.

[Reid Barton]

Uh, the unedited version.

[Eric Wieser]

The result of clicking docs#tprod is what Reid means

[Yakov Pechersky]

Right. I mistyped, thanks for that. Right, there are also a variety of definitions and lemmas related to tensor products, like docs#pi_tensor_product.tprod_coeff

[Eric Wieser]

They're all namespaced though so I don't think there's any clash to worry about

[Eric Wieser]

I think a bigger concern is that a bunch of tsum lemmas talk about continuous linear maps which don't have a multiplicative analogy

[Jireh Loreaux]

I think we should have tprod and we should to_additivize as much as possible. Of course that will exclude things involving linearity, but that's not weird.

[David Loeffler]

Can I just as for a clarification on what's meant by the following option in the poll?

Use infinite products in terms of tendsto like we have for a lemma about sin x (Thanks Eric Wieser)

If this is a reference to the discussion a few days ago (edit: here) where Eric mentioned docs#complex.tendsto_euler_sin_prod , then I want to point out that this is a bit misleading, because the notion of convergence used in that proof is not mathematically equivalent to the multiplicative analogue of tsum. What's used in euler_sin_prod is taking the limit as $N \to \infty$ of $\prod_{i = 0}^N f(i)$. However, the "morally right" notion of convergence, which we don't have an API or a name for yet, is taking the limit of $\prod_{i \in I} f(i)$, where $I$ is a finite subset of $\mathbb{N}$, wrt the cofinite filter. So euler_sin_prod isn't a model to follow here.

[Yaël Dillies]

Does this model of convergence match docs#has_sum?

[Jireh Loreaux]

Yes

[David Loeffler]

Yes -- what I called "the morally right notion" for products is the one matching the existing definition of has_sum.

[Yury G. Kudryashov]

After the porting is done, I'm going to refactor pi measures so that we no longer need list.tprod (unless someone wants to use them for another purpose). Also, list.tprod is in a namespace, so there is no actual name clash.

[David Loeffler]

So: are we agreed that the poll is rendered moot by the fact that list.tprod isn't in the root namespace, and Yakov has the green light to define tprod in the root namespace as the infinite-product version of tsum?

[Jireh Loreaux]

It would be nice to get it in before the port hits it.

[Yakov Pechersky]

Just to confirm, something like this is what you're okay with (morally):

import topology.algebra.infinite_sum

noncomputable theory
open finset filter function classical
open_locale topology classical big_operators nnreal

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}

section has_prod
variables [comm_monoid α] [topological_space α]

def has_prod (f : β → α) (a : α) : Prop := tendsto (λs:finset β, ∏ b in s, f b) at_top (𝓝 a)

/-- `proddable f` means that `f` has some (infinite) product. Use `tprod` to get the value. -/
def proddable (f : β → α) : Prop := ∃a, has_prod f a

/-- `∏' i, f i` is the product of `f` it exists, or 1 otherwise -/
@[irreducible] def tprod {β} (f : β → α) := if h : proddable f then classical.some h else 1

notation `∏'` binders `, ` r:(scoped:67 f, tprod f) := r

lemma has_sum_of_mul_iff_has_prod {f : β → α} {a : α} :
  has_sum (additive.of_mul ∘ f) (additive.of_mul a) ↔ has_prod f a := iff.rfl

lemma summable_of_mul_iff_proddable {f : β → α} :
  summable (additive.of_mul ∘ f) ↔ proddable f := iff.rfl

lemma tsum_of_mul_eq_of_mul_tprod (f : β → α) :
  ∑' i, additive.of_mul (f i) = additive.of_mul (∏' i, f i) :=
begin
  rw [tprod, tsum],
  by_cases h : proddable f,
  { rw [dif_pos h, dif_pos],
    refl },
  { rw [dif_neg h, dif_neg],
    { refl },
    { rwa summable_of_mul_iff_proddable } }
end

lemma to_mul_tsum_of_mul_eq_tprod (f : β → α) :
  additive.to_mul (∑' i, additive.of_mul (f i)) = ∏' i, f i := tsum_of_mul_eq_of_mul_tprod f

lemma proddable_of_zero {R : Type*} [comm_semiring R] [topological_space R]
  (f : β → R) (hf : ∃ b, f b = 0) : proddable f :=
begin
  refine ⟨0, _⟩,
  obtain ⟨b, hb⟩ := hf,
  rw has_prod,
  rw tendsto_at_top_nhds,
  intros U hU hU',
  refine ⟨{b}, λ V hV, _⟩,
  have hb' : b ∈ V := singleton_subset_iff.mp hV,
  rwa prod_eq_zero hb' hb
end

end has_prod

[Yakov Pechersky]

With example usage like:

import taoziegler.tomathlib.infinite_prod
import analysis.special_functions.log.basic

noncomputable theory
open finset filter function classical
open_locale topology classical big_operators nnreal

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}

lemma proddable_of_summable_log (f : β → ℝ) (hf : ∀ b, 0 < f b) (h : summable (real.log ∘ f)) :
  proddable f :=
begin
  have : ∀ x, (real.exp ∘ λ (s : finset β), ∑ (b : β) in s, (real.log ∘ f) b) x =
    (λ (s : finset β), ∏ (b : β) in s, f b) x,
  { intros s,
    simp only [comp_app],
    rw real.exp_sum,
    exact prod_congr rfl (λ b hb, real.exp_log (hf _)) },
  obtain ⟨x, h⟩ := h,
  refine ⟨real.exp x, _⟩,
  exact (tendsto_congr this).mp ((real.continuous_exp.tendsto _).comp h)
end

lemma summable_log_one_add_of_summable (s : β → ℝ) (hs : ∀ i, 0 ≤ s i) (h : summable s) :
  summable (λ i, real.log (1 + s i)) :=
begin
  refine summable_of_nonneg_of_le (λ b, real.log_nonneg _)
    (λ b, (real.log_le_sub_one_of_pos _).trans _) h;
  specialize hs b;
  linarith
end


lemma proddable_one_add_of_summable (s : β → ℝ) (hs : ∀ i, 0 < s i) (h : summable s) :
  proddable (λ i, 1 + s i) :=
begin
  refine proddable_of_summable_log _ (λ b, _) (summable_log_one_add_of_summable _ (λ b, _) h);
  specialize hs b;
  linarith
end

[Yakov Pechersky]

Correct?

[Yakov Pechersky]

Unfotunately, as Bhavik pointed out, the usage of proddable is less stable than summable, since finite values can make a previously un-proddable (not converging) function become proddable by adding at least one 0; non-summable functions cannot be made summable so easily.

[David Loeffler]

I think we need to handle zeroes and non-invertible elements a little differently.

If G is a (multiplicative) topological abelian group then the definition of convergence of a G-valued group should be exactly what you wrote. But if R is a topological ring, then I think we should define "convergence" of a product valued in R to mean that every term of the product is a unit in R, and the convergence holds be w.r.t. the morally-correct topology on $R^\times$, which is the one induced by its embedding into $R \times R$ via $t \mapsto (t, 1/t)$ -- this is not the same, in general, as the subspace topology from $R^\times \subset R$.

[Yakov Pechersky]

Yael had said something similar to me today on a call, regarding handling units properly.

[Yakov Pechersky]

Would the embedding $G \times G$ via $g \mapsto (g, 1/g)$ work also?

[Yakov Pechersky]

This way, we could have one case handle both, through[comm_monoid G].

[Eric Wieser]

Requiring every term to be a unit would mean that (∏' n : ℕ, if n = 0 then (2 : ℤ) else 1) = 1 though, wouldn't it?

[Eric Wieser]

Or is there not enough structure on ℤ to make that legal anyway?

[Sebastien Gouezel]

A better definition is probably to require that, for any finite set s, then the product on finsets in the complement of s converges as these finsets grow to cover univ \ s. But this would mean also changing our definition of summability, so this would be a pretty thorough refactor...

[Yaël Dillies]

I started multiplicativising topology.algebra.infinite_sum while on a call with Yakov yesterday. My thought is that even if we want to change the definition of prodable, we first want to make sure we have feature parity between the additive and multiplicative worlds.

[Yaël Dillies]

Then if we change the definition of summable in a way that only differs from the current for non-cancellative monoids, it shouldn't be too hard to refactor, as hopefully most uses of summable are in groups, or at the very least in cancellative monoids (looking at you, ennreal).

[Sebastien Gouezel]

There aren't really uses of summable in ennreal, fortunately, because everything is summable there. Cancellative monoids won't be enough most of the time, though, because one would need "continuity of subtraction", which we don't have a typeclass for (the definition would probably be: if u n + a tends to b + a, then u n tends to b). That's why results for nnreal are typically proved separately from the general results, because that's the only interesting example we use a lot which is not a group.

[Kevin Buzzard]

Reid posted a while ago a nice example of a cancellative topological monoid for which subtraction wasn't continuous (in case anyone was hoping it was always true). Consider the nonnegative reals with all usual sets open and also every subset of the interval [0,1] open. Then 1.5-1/n tends to 1.5 but 0.5-1/n doesn't tend to 0.5 because {0.5} is open.

[Kevin Buzzard]

This example also shows that cancellative topological monoids might be far from "homogeneous" (the topology near every point looks the same), whereas topological groups must be homogeneous.

[Chris Hughes]

Kevin Buzzard said:

Reid posted a while ago a nice example of a cancellative topological monoid for which subtraction wasn't continuous (in case anyone was hoping it was always true). Consider the nonnegative reals with all usual sets open and also every subset of the interval [0,1] open. Then 1.5-1/n tends to 1.5 but 0.5-1/n doesn't tend to 0.5 because {0.5} is open.

Is it even true that a group with continuous addition necessarily has continuous subtraction? If it is we should update the definition of topological group in mathlib.

[Eric Wieser]

What would need changing in docs#topological_group?

[Jireh Loreaux]

No, it's fine as is. Continuity of addition and negation imply continuity of subtraction trivially.

[Jireh Loreaux]

Surely docs#topological_group.to_has_continuous_div is a thing

[Chris Hughes]

Eric Wieser said:

What would need changing in docs#topological_group?

You wouldn't need the continuous_inv axiom. I don't think it is true though.

[Chris Hughes]

But I don't know a counter example

[Jireh Loreaux]

Sorry, I misread/misinterpreted what you were saying

[Jireh Loreaux]

Probably the real line with the lower limit topology is a counterexample.

[Yury G. Kudryashov]

BTW, should we move it from counterexamples to topology.instances?

[Yury G. Kudryashov]

Now I see that @Christopher Hoskin duplicated some of my work in docs#with_lower_topology

[Yury G. Kudryashov]

(though this file uses a more generic definition that works for preorders)

[Yury G. Kudryashov]

Sebastien Gouezel said:

There aren't really uses of summable in ennreal, fortunately, because everything is summable there. Cancellative monoids won't be enough most of the time, though, because one would need "continuity of subtraction", which we don't have a typeclass for (the definition would probably be: if u n + a tends to b + a, then u n tends to b). That's why results for nnreal are typically proved separately from the general results, because that's the only interesting example we use a lot which is not a group.

We have docs#has_continuous_sub but this is something else. ∀ a b, map ((+) a) (nhds b) = nhds (a + b)? no

[Yury G. Kudryashov]

@Christopher Hoskin Sorry, your file is about the lower topology while mine is about the lower limit topology. I should be more careful before making claims about work duplication.

[Yakov Pechersky]

I'm trying to prove something useful with the definition that I copied from summable. What's the better way to resolve the tendsto goal, instead of falling into working with opens? The proof ends up juggling through subtypes. Additionally, how should the proddable/has_prod definition look like, if this theorem proddable_of_summable_log example is a thing we'd like to prove?

import analysis.special_functions.log.basic

noncomputable theory
open finset filter function classical
open_locale topology classical big_operators

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}

section has_prod
variables [comm_monoid α] [topological_space α]

def has_prod (f : β → α) (a : α) : Prop := tendsto (λs:finset β, ∏ b in s, f b) at_top (𝓝 a)

def proddable (f : β → α) : Prop := ∃a, has_prod f a

lemma proddable_of_zero {R : Type*} [comm_semiring R] [topological_space R]
  (f : β → R) (hf : ∃ b, f b = 0) : proddable f :=
begin
  refine ⟨0, _⟩,
  obtain ⟨b, hb⟩ := hf,
  rw has_prod,
  rw tendsto_at_top_nhds,
  intros U hU hU',
  refine ⟨{b}, λ V hV, _⟩,
  have hb' : b ∈ V := singleton_subset_iff.mp hV,
  rwa prod_eq_zero hb' hb
end

end has_prod

namespace finset

variables [comm_monoid β] (p : α → Prop) [decidable_pred p] (s : finset α) (f : α → β)

@[simp] lemma map_subtype {s : finset (subtype p)} :
  finset.subtype p (map (embedding.subtype p) s) = s :=
begin
  rw [←(map_injective (embedding.subtype p)).eq_iff, subtype_map_of_mem],
  simp { contextual := tt }
end

@[to_additive]
lemma prod_subtype' :
  ∏ i in (s.subtype p), f i = ∏ i in s.filter p, f i :=
begin
  refine prod_bij' (λ a _, a) (λ a ha, mem_filter.mpr ⟨mem_subtype.mp ha, a.prop⟩) (λ _ _, rfl)
    (λ a ha, ⟨a, (mem_filter.mp ha).right⟩) _ _ _;
  simp { contextual := tt }
end

@[to_additive]
lemma prod_subtype_mem (p : set α) [decidable_pred (∈ p)] (s : finset α) (f : α → β) :
  ∏ (i : p) in (s.subtype (∈ p)), f i = ∏ i in s.filter p, f i :=
prod_subtype' _ _ _

end finset

lemma proddable_of_summable_log (f : β → ℝ) (hf : ∀ᶠ b in cofinite, 0 ≤ f b)
  (h : summable (real.log ∘ f)) : proddable f :=
begin
  by_cases H : ∃ x : β, f x = 0,
  { refine proddable_of_zero _ H },
  push_neg at H,
  set s := {b | f b < 0} with hs,
  have hsf : s.finite,
  { convert hf,
    ext,
    simp },
  have hsp : hsf.to_finset.prod f =
    (- 1) ^ hsf.to_finset.card * real.exp (hsf.to_finset.sum (real.log ∘ f)),
  { simp_rw [real.exp_sum, ←prod_const, ←prod_mul_distrib],
    rw prod_congr rfl,
    simp [real.exp_log_of_neg] {contextual := tt} },
  have hpos := h.subtype {b | 0 < f b},
  obtain ⟨x, hpos⟩ := hpos,
  refine ⟨hsf.to_finset.prod f * real.exp x, _⟩,
  suffices : tendsto (λ (s : finset β), (∏ (b : β) in s.filter (λ x, f x < 0), f b) *
    ∏ (b : β) in s.filter (λ x, 0 < f x), f b) at_top (𝓝 (hsf.to_finset.prod f * real.exp x)),
  { rw has_prod,
    convert this,
    ext s,
    rw [prod_filter, prod_filter, ←prod_mul_distrib, prod_congr rfl],
    intros b hs,
    rcases lt_trichotomy (f b) 0 with hb|hb|hb,
    { simp [hb, hb.not_lt] },
    { exact absurd hb (H _) },
    { simp [hb, hb.not_lt] } },
  refine tendsto.mul _ _,
  { rw tendsto_nhds,
    -- how to use tendsto relating to a finite set?
    intros t ht hmt,
    simp only [mem_at_top_sets, ge_iff_le, le_eq_subset, set.mem_preimage],
    refine ⟨hsf.to_finset, λ s' hs', _⟩,
    rw ←prod_subset (monotone_filter_left _ hs'),
    { simp [hmt] },
    { simp [not_le_of_lt] { contextual := tt } } },
  { have := (real.continuous_exp.tendsto _).comp hpos,
    -- how to use tendsto relating to (co)mapping with `finset.image coe`?
    rw tendsto_nhds at this ⊢,
    intros t ht hmt,
    specialize this t ht hmt,
    simp only [mem_at_top_sets, ge_iff_le, le_eq_subset, set.mem_preimage, comp_app] at this ⊢,
    obtain ⟨u, hu⟩ := this,
    refine ⟨u.map (embedding.subtype _), λ v hv, _⟩,
    convert hu (v.subtype _) _,
    { rw real.exp_sum,
      convert (finset.prod_subtype_mem {b : β | 0 < f b} _ _).symm,
      ext ⟨b, posb⟩,
      exact real.exp_log posb },
    { convert subtype_mono hv,
      rw finset.map_subtype } },
end

[Yakov Pechersky]

The "other direction" is much simpler:

lemma proddable_exp_of_summable (f : β → ℝ) (h : summable f) : proddable (real.exp ∘ f) :=
begin
  obtain ⟨x, h⟩ := h,
  refine ⟨real.exp x, ((real.continuous_exp.tendsto _).comp h).congr _⟩,
  simp [real.exp_sum]
end

[Yaël Dillies]

Yaël Dillies said:

I started multiplicativising topology.algebra.infinite_sum while on a call with Yakov yesterday. My thought is that even if we want to change the definition of prodable, we first want to make sure we have feature parity between the additive and multiplicative worlds.

#18405 (beware, huge)

[David Loeffler]

Build seems to have died with a timeout error (not sure if this is related to the PR or just random)

[Yakov Pechersky]

@David Loeffler Is this more what you were thinking of?

import topology.algebra.infinite_sum

noncomputable theory
open finset filter function classical
open_locale topology classical big_operators nnreal

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}

section
variables [comm_monoid α] [topological_space α]

structure has_prod (f : β → α) (a : α) : Prop :=
(finite_not_unit : {b | ¬ is_unit (f b)}.finite)
(tendsto_units : ∃ x : αˣ, tendsto
  (λ s : finset β, ∏ b in (s.filter (λ i, is_unit (f i))), f b) at_top (𝓝 x))
(prod_eq : a = tendsto_units.some * ∏ b in finite_not_unit.to_finset, f b)

image.png

[Yakov Pechersky]

Here are two lemmas proved about that definition (and an auxiliary one):

def converges_prod (f : β → α) : Prop := ∃ (a : α), has_prod f a

lemma has_prod_zero_iff_converges_prod_and_exists_zero {f : β → ℝ} :
  has_prod f 0 ↔ converges_prod f ∧ ∃ i, f i = 0 :=
begin
  split,
  { intro h,
    have := h.prod_eq,
    simp only [zero_eq_mul, false_or, prod_eq_zero_iff, units.ne_zero, set.finite.mem_to_finset,
               set.mem_set_of_eq, exists_prop] at this,
    obtain ⟨i, -, hi⟩ := this,
    exact ⟨⟨_, h⟩, i, hi⟩ },
  { rintro ⟨⟨a, hf⟩, i, h⟩,
    refine ⟨hf.finite_not_unit, hf.tendsto_units, _⟩,
    simp only [prod_eq_zero_iff, zero_eq_mul, units.ne_zero, set.finite.mem_to_finset,
               set.mem_set_of_eq, exists_prop, false_or],
    use i,
    simp [h] }
end

lemma has_prod_ratio {f : β → ℝ} {a : ℝ} (hf : has_prod f a) :
  tendsto (λ sb : finset β × β, (
      ∏ b in ((insert sb.2 sb.1).filter (λ i, is_unit (f i))), f b) /
      ∏ b in (sb.1.filter (λ i, is_unit (f i))), f b)
    (at_top.comap prod.fst) (𝓝 1) :=
begin
  obtain ⟨x, hx⟩ := hf.tendsto_units,
  rw ←div_self x.ne_zero,
  simp_rw div_eq_mul_inv,
  refine tendsto.mul _ ((real.tendsto_inv x.ne_zero).comp _),
  { intros U hU,
    specialize hx hU,
    simp only [filter.mem_map, mem_comap, mem_at_top_sets, ge_iff_le, le_eq_subset,
               exists_prop] at hx ⊢,
    obtain ⟨s, hs⟩ := hx,
    simp only [set.mem_preimage] at hs,
    set s' : set (finset β) := (λ t, s ∪ t) '' set.univ with hs',
    refine ⟨s', ⟨s, _⟩, _⟩,
    { simp only [hs', set.image_univ, set.mem_range],
      intros t ht,
      refine ⟨t \ s, _⟩,
      simp [ht] },
    simp only [hs', set.image_univ],
    rintro ⟨t, b⟩,
    simp only [set.mem_preimage, set.mem_range, forall_exists_index],
    rintro x rfl,
    refine hs _ _,
    exact (subset_union_left _ _).trans (subset_insert _ _) },
  { refine (hx.comp tendsto_comap).congr _,
    simp }
end

[Yakov Pechersky]

I apologize if I am not using the right filter -- I'm still trying to figure out the best way to express "textbook limits" as filters in this situation.
image.png

[Eric Wieser]

This fails for products over multiplicative nnreal on functions with infinite support that converged additively

[Eric Wieser]

(because there is only one unit (multiplicative nnreal), 1)

[Yaël Dillies]

To give more context, Yakov's proposed definition can be additivised, and we should check the additivisation is not bogus.

[Yakov Pechersky]

@Eric Wieser, can you say more? Why would one do infinite products over multiplicative nnreal as opposed to just nnreal?

[Eric Wieser]

Infinite products over multiplicative nnreal should be analogous to infinite sums over nnreal, shouldn't they?

[Eric Wieser]

Meaning that one should converge iff the other does

[Yakov Pechersky]

I think the literature I have found so far says that one should treat infinite products differently than infinite sums.

[Yakov Pechersky]

In particular, the additivised statement is:
image.png

[Yakov Pechersky]

I think one can't just expect an add-mul correspondence because, at least in the literature I've read so far, infinite products are considered in the context of rings, where 0 plays a spoiler role.

[Eric Wieser]

Why is the spoiler role of 0 any different to the spoiler role of \top in the additive case?

[Yakov Pechersky]

If one wants a tsum-like product for some group, they can do it over additive G, perhaps

[Yakov Pechersky]

Because with 0, one can "converge" to 0 or diverge to 0; while with \top in something that isn't extended, one can only diverge to \top.

[Yakov Pechersky]

That's my understanding so far

[Eric Wieser]

Is extending a additive monoid with top any different to extending a multiplicative group with zero?

[Eric Wieser]

It sounds like part of the problem is that the literature doesn't care about monoids and only rings.

[Yakov Pechersky]

Consider the theorem in the screenshot, relating the convergence of \prod n, 1 + f_n to \sum n, f_n -- how would you interpret this outside of a ring's context?

[Eric Wieser]

Oh, I'm sure you can't; the question is whether having that theorem hold in rings is incompatible with having the multiplicative theorem I'm thinking of (has_sum f a \iff has_prod (of_add \comp f) (of_add f)) hold in monoids.

[Yakov Pechersky]

I see -- so in the context of a monoid where nothing is is_unit except 1, how does it work, right? And we can't phrase it in terms of "non zero divisors" if there isn't a 0 in the type.

[Eric Wieser]

At the hacky end of ideas, you can case the definition on whether a zero-like element exists

[Yakov Pechersky]

Before going hackier, I'd like to confirm from experts whether this definition is even on the way to "morally correct" =)

[Eric Wieser]

Sebastien Gouezel said:

Cancellative monoids won't be enough most of the time, though, because one would need "continuity of subtraction", which we don't have a typeclass for

Would I be right in saying that it's continuity of tsub / monus that we don't have?

[Yaël Dillies]

I think the important point is that the main property is not docs#is_unit but docs#is_regular. Almost all elements of nnreal are not units, but they are all regular.

[Yaël Dillies]

Yes and no. tsub looks like the best way to phrase it, but that implies having it defined in the first place. An intrinsic definition would be better, but I'm not sure how yet.

[David Loeffler]

Oh, I'm sure you can't; the question is whether having that theorem hold in rings is incompatible with having the multiplicative theorem I'm thinking of (has_sum f a \iff has_prod (of_add \comp f) (of_add f)) hold in monoids.

I'm afraid that the way that mathematicians conventionally use infinite products in topological rings seems to be genuinely incompatible with the naive "multiplicativization" of infinite sums: there is no single definition of "infinite operation on a topological monoid" which specialises to both.

(To see this, consider the product in $\mathbb{Z}_p$ of \lambda i : ℕ, p. All terms are regular, and even "topologically regular" (multiplication by p is a homomorphism onto its image); but the partial sums do not converge to anything in the unit group, so this product should definitely be considered divergent. However, if you take the additivization of the topological monoid of $\mathbb{Z}_p$ and quotient out by the units, you get with_top ℕ; and our existing treatment of sums in monoids would have everything converging! So I don't think these can be reconciled.)

@Yakov Pechersky In your candidate definition, what topology are you putting on αˣ ? Is it the subspace topology from α, or the subspace topology from α ^ 2 via (x, 1/x)?

[Yakov Pechersky]

I think in the definition as it is, it's the subspace topology from α because it is just evaluating the partial products in α, with the terms limited "propositionally" to the subspace of is_unit.
However, docs#units.topological_space is the one that is α × αᵐᵒᵖ

/-- The units of a monoid are equipped with a topology, via the embedding into `M × M`. -/
@[to_additive "The additive units of a monoid are equipped with a topology, via the embedding into
`M × M`."]
instance : topological_space Mˣ := prod.topological_space.induced (embed_product M)

[Yakov Pechersky]

Do you suggest to switch that topology, by using a different at_top filter?

[Eric Wieser]

Just to check, since I've been called out by a reviewer on it being ambiguous; is $\mathbb{Z}_p$ the same as $\mathbb{Z}/p\mathbb{Z}$ aka zmod p, or something else?

[Yakov Pechersky]

I think we're missing this:

instance units.uniform_space [monoid γ] [h : uniform_space γ] : uniform_space γˣ :=
(prod.uniform_space : uniform_space (γ × γᵐᵒᵖ)).comap (units.embed_product _)

[Yaël Dillies]

Eric Wieser said:

Just to check, since I've been called out by a reviewer on it being ambiguous; is $\mathbb{Z}_p$ the same as $\mathbb{Z}/p\mathbb{Z}$ aka zmod p, or something else?

Depends on your conventions, but it would usually refer to the $p$-adic numbers, namely the inverse limit of $ℤ/p^kℤ$ over $k = 0, 1, \dots$.

[Yaël Dillies]

In that case, David clearly means the p-adics, as else you get a boring product of zeroes.

[David Loeffler]

Number theorists invariably use $\mathbb{Z}_p$ for p-adics, and $\mathbb{F}_p$ or $\mathbb{Z} / p$ for integers mod p. I've only encountered the other usage in algebraic topology texts, although this seems to be shifting in recent years since algebraic topologists have belatedly discovered that p-adic arithmetic is useful!

[Kevin Buzzard]

Finite group theorists seem to call the cyclic group of order p $\Z_p$.

[Sebastien Gouezel]

Sebastien Gouezel said:

A better definition is probably to require that, for any finite set s, then the product on finsets in the complement of s converges as these finsets grow to cover univ \ s. But this would mean also changing our definition of summability, so this would be a pretty thorough refactor...

As I said above, I think this is the right definition for infinite products, that takes care of the problems created by zero and still ensures that changing a proddable sequence at finitely many places still gives a proddable sequence. And its additivisation is equivalent to the usual summability definition in "good" monoids (i.e., those for which u_n + b tends to a + b iff u_n tends to a). In the long run, this is probably the definition we should use. But given that this will be a painful refactor, I strongly advise that we don't embark on this now and wait for after the port.

[Kevin Buzzard]

I guess what's going on is that additively most (but not all) monoids that come up in practice are good (because they don't contain +infinity) but multiplicatively many are not (because they do contain 0). In analytic number theory you see infinite products in things like the definition of the Riemann zeta function $\prod_p(1-p^{-s})^{-1}$ and more generally of the L-function $\prod_p F(p^{-s})^{-1}$ associated to an elliptic curve, modular form, Galois representation, motive etc etc. But these products only converge when the complex parameter $s$ lies in some half plane and in this region none of the factors can be zero, yet we think of it as a product in $\mathbb{C}$ rather than the arguably more correct $\mathbb{C}^\times.$

[Junyan Xu]

It would be unnatural to exclude zero in the Weierstrass factorization theorem and Blaschke products / factorization of inner functions, and I think proving the Weierstrass theorem would be a nice test of the API around infinite products.