feat: "outer product" of functions that tend to zero on the cocompact filter

[trivial1711]

Let M be a topological space with a continuous multiplication operation and a zero.

We prove that if f : α → M and g : β → M are continuous functions that both tend to zero on the cocompact filter, then the "outer product" fun (i : α × β) ↦ (f i.1) * (g i.2) also tends to zero on the cocompact filter.

We then specialize this result to the case that α and β have the discrete topology.

---

• [x] depends on: #12305

[ADedecker]

Very nice work, thanks a lot!

I think it would be nice to split up some useful lemmas from the main proof, e.g a version of Filter.Tendsto.zero_mul_isBoundedUnder_le where the "IsBoundedUnder" hypothesis is replaced by "being disjoint from cocompact". Then I would deduce a lemma saying that multiplication tends to zero along the infimum of coprod (𝓝 0) (𝓝 0) and any filter on the product which is disjoint from cocompact. And finally deduce your current result.

Does that make sense to you? The reason I'm suggesting this is because I think at least the first intermediate lemma will be useful, and probably the second as well (although I'm less sure).

[trivial1711]

Yes, that makes sense. Thank you for reading it. I'll work on it soon.

[github-actions[bot]]

PR summary 62d99d5bd4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ tendsto_mul_cocompact_nhds_zero + tendsto_mul_cofinite_nhds_zero

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).

[trivial1711]

I proved the lemmas that ADedecker requested. They're on another pull request: #19650

I can't figure out how to actually use those lemmas to simplify the proof of tendsto_mul_cocompact_nhds_zero, though.

I apologize that this has taken so long.

[ADedecker]

You don't have to apologize at all! In fact I should probably be the one apologizing for causing troubles by giving unclear instructions. What I had in mind is the following:

• using Filter.Tendsto.prod_map_coprod and Filter.coprod_cocompact, get that Prod.map f g tends to (𝓝 0).coprod (𝓝 0) along the cocompact filter.
• but Prod.map f g also converges to 𝓟 (range (Prod.map f g)), which is disjoint from the cocompact filter since that range is contained in a compact set.
• hence, you can apply tendsto_mul_nhds_zero_of_disjoint_cocompact (from your new PR) to l = map (Prod.map f g) (cocompact _) to get the result.

Does that make sense? If you're tired of this I can have a go at it as well.

[trivial1711]

Hi, I will try to modify the proof to use those facts as you describe. For now, I have reconfigured the branches so that this PR (#12313) now depends on #19650, instead of the other way around. Can you take a look at that one?

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12305~~
• ~~leanprover-community/mathlib4#19650~~ By Dependent Issues (🤖). Happy coding!

[trivial1711]

I'm still not entirely sure what to do with this. You can push directly to this branch if you have a way to simplify the proof.

[ADedecker]

I just pushed what I had in mind!

[trivial1711]

Thanks; I've added you as a coauthor.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style