Infinite version of `Finset.prod_one_add`

Stream: Is there code for X?

[Weiyi Wang]

I am trying to find / proof some infinite version of docs#Finset.prod_one_add. Here is the sketch I have, which I am not sure if is correct

import Mathlib
variable {ι α : Type*} [CommSemiring α] [TopologicalSpace α]
theorem hasProd_one_add_of_hasSum {f : ι → α} {a : α}
    (h : HasSum (fun s : Finset ι ↦ ∏ i ∈ s, f i) a):
    HasProd (1 + f ·) a := by
  unfold HasProd
  unfold HasSum at h
  have : (fun s ↦ ∏ i ∈ s, (fun x ↦ 1 + f x) i) =
       (fun p ↦ ∑ s ∈ p, ∏ i ∈ s, f i ) ∘ (fun s ↦ s.powerset):= by
    ext s
    exact Finset.prod_one_add s
  rw [this]
  apply h.comp
  sorry  -- ⊢ Filter.Tendsto Finset.powerset Filter.atTop Filter.atTop

It left me with a goal which I don't find useful lemmas for, and which I don't know if is correct either

Is there existing results in mathlib, and what is the right statement of this?

[Chris Birkbeck]

So we have things like docs#multipliable_norm_one_add_of_summable_norm

[Weiyi Wang]

Oh, I guess I only searched for tprod and HasProd, but not Multipliable. Though, this one is in normed space. Mine is related to PowerSeries which I don't know if I can define a norm. I was able to prove my specific theorems in the specific setting, but I am curious if there is a more general version, like one that can give explicit formula other than just Multipliable

[Chris Birkbeck]

Do you mean (h : HasSum (fun s : Finset ι ↦ ∏ i ∈ s, f i) a)? It seems you are saying if the limit of the sums of bigger products is a then the infinite product is a, which seems wrong.

[Chris Birkbeck]

oh wait, ignore me you have a one_add which is maybe what I forgot

[Weiyi Wang]

Disclosure for LLM involvement: LLM insisted the last goal is wrong, even though I feel it is correct, which is why I asked here

[Weiyi Wang]

Ok, nvm, LLM lied to me

variable {ι α : Type*} [DecidableEq ι] [CommSemiring α] [TopologicalSpace α]
theorem hasProd_one_add_of_hasSum {f : ι → α} {a : α}
    (h : HasSum (fun s : Finset ι ↦ ∏ i ∈ s, f i) a):
    HasProd (1 + f ·) a := by
  unfold HasProd
  unfold HasSum at h
  have : (fun s ↦ ∏ i ∈ s, (fun x ↦ 1 + f x) i) =
       (fun p ↦ ∑ s ∈ p, ∏ i ∈ s, f i ) ∘ (fun s ↦ s.powerset):= by
    ext s
    exact Finset.prod_one_add s
  rw [this]
  apply h.comp
  rw [Filter.tendsto_atTop_atTop]
  intro t
  use t.sup id
  intro u hu v hv
  simp only [mem_powerset]
  refine le_trans ?_ hu
  exact le_sup_of_le hv fun _ a ↦ a

[Aaron Liu]

Weiyi Wang said:

Disclosure for LLM involvement: LLM insisted the last goal is wrong, even though I feel it is correct, which is why I asked here

I also feel it is correct

[Weiyi Wang]

I also asked myself whether the HasProd -> HasSum direction was correct. My guess is it is not in general, but I wonder if there are additional condition that can make it true (some condition in normed space might be it as hinted above)