[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas

[CBirkbeck]

---

[github-actions]

PR summary 9d2bcc539a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ multipliable_pnat_iff_multipliable_succ
+ tprod_comp_neg
+ tprod_int_eq_zero_mul_tprod_pnat_sq
+ tprod_zero_pnat_eq_tprod_nat

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[CBirkbeck]

I want to add the to_additive tag to pnat_multipliable_iff_multipliable_succ' and tprod_pnat_eq_tprod_succ' (and remove the non-primed versions) but it gives me an error which I can't figure out.

[loefflerd]

I admit that it's not clear to me why the changes in this PR are beneficial. Can you explain why you want them? E.g. the new formulation of tprod_pnat_eq_tprod_succ seems to be just the old one applied to f ∘ (↑) where (↑) is coercion from Nat to R.

(Generally I'm a bit wary of using PNat. I can see the appeal of writing ∑' n : ℕ+, f n rather than the slightly uglier ∑' n : ℕ, f (n + 1), but there's a price to be paid: it means you have to either duplicate large chunks of the immense existing Nat API for PNat, or manually insert coercions all over the place, or both.)

[CBirkbeck]

So the problem with the old one is that when I came to try and prove tsum_nat_eq_zero_two_pnat it became a pain with the coercions. Since I keep having to swap between infinite sums over PNat, Nat, and Int, having this made that a bit easier.

I could just try and ignore PNat and use (n + 1) everywhere, but that also becomes quite annoying. Obviously it's all doable with Nat and (n + 1), but for example, later we need things like, infinite sums over PNat of functions with -N/z (for z in the upper half plane and N a PNat) and its just nicer to have N's and not N+1's everywhere since any time you use ring it does a mul_add and thats just annoying. I don't actually think we need huge amounts of duplication to get some decent infinite sums over PNat API, so I've been gradually adding it as I find the need for it.

[loefflerd]

So the problem with the old one is that when I came to try and prove tsum_nat_eq_zero_two_pnat it became a pain with the coercions. Since I keep having to swap between infinite sums over PNat, Nat, and Int, having this made that a bit easier.

Here's a proof of tsum_nat_eq_zero_two_pnat using the existing formulations of the preceding lemmas (without this funny R):

section PNat

@[to_additive]
theorem multipliable_pnat_iff_multipliable_succ {f : ℕ → M} :
    Multipliable (fun x : ℕ+ ↦ f x) ↔ Multipliable fun x ↦ f (x + 1) :=
  Equiv.pnatEquivNat.symm.multipliable_iff.symm

@[to_additive]
theorem tprod_pnat_eq_tprod_succ {f : ℕ → M} : ∏' n : ℕ+, f n = ∏' n, f (n + 1) :=
  (Equiv.pnatEquivNat.symm.tprod_eq _).symm

@[to_additive]
lemma tprod_zero_pnat_eq_tprod_nat [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
    {f : ℕ → G} (hf : Multipliable f) :
    f 0 * ∏' n : ℕ+, f ↑n = ∏' n, f n := by
  simpa [hf.tprod_eq_zero_mul] using tprod_pnat_eq_tprod_succ

@[to_additive tsum_nat_eq_zero_two_pnat]
theorem tprod_nat_eq_zero_mul_tprod_pnat_sq [UniformSpace G] [IsUniformGroup G] [CompleteSpace G]
    [T2Space G] {f : ℤ → G} (hf : ∀ n : ℤ, f (-n) = f n) (hf2 : Multipliable f) :
    ∏' n, f n = f 0 * (∏' n : ℕ+, f n) ^ 2 := by
  have hf3 : Multipliable fun n : ℕ ↦ f n :=
    (multipliable_int_iff_multipliable_nat_and_neg.mp hf2).1
  have hf4 : Multipliable fun n : ℕ+ ↦ f n := by
    rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)),
      multipliable_nat_add_iff 1 (f := (f ·))]
  have := tprod_nat_mul_neg hf2
  rw [← tprod_zero_pnat_eq_tprod_nat (by simpa [hf] using hf3.mul hf3), mul_comm _ (f 0)] at this
  simp only [hf, Nat.cast_zero, mul_assoc, mul_right_inj] at this
  rw [← this, mul_right_inj, hf4.tprod_mul hf4, sq]

end PNat

[CBirkbeck]

Oh nice thanks. I honestly thought that using AddMonoidWithOne R was just more general and would ease more coercion issues. Edit: Ah but I see that they all come with a map into them from Nat, so this isnt really more general. I missed that.

[loefflerd]

Yes exactly. You're allowing a general R, but requiring your functions to be the composite of the coercion Nat -> R and a function R -> something; so this is actually less general than an arbitrary function Nat -> something.

[loefflerd]

LGTM modulo a minor naming comment

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[sgouezel]

Doesn't build yet.

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success