Gaps in Mathlib's ZeroAtFilter / BoundedAtFilter API

Mathlib's Filter.ZeroAtFilter and Filter.BoundedAtFilter are closed under binary sums (Filter.ZeroAtFilter.add, Filter.BoundedAtFilter.add), and the bounded functions are closed under a Finset.prod (Filter.BoundedAtFilter.prod, via boundedFilterSubalgebra). The additive counterpart of that product lemma is not recorded upstream; this file adds it for both predicates.

The gap shows up wherever an operator is a finite sum of slashes: proving that such an operator stays bounded, or stays vanishing, along atImInfty is an induction over the summands, and without these each call site reruns it.

Mathlib also has no rule for pushing a vanishing function through a map. ZeroAtFilter is convergence to 0, so only the behaviour of that map at 0 matters — global continuity is not needed, and asking for it would exclude the topological modules that carry ContinuousAdd rather than IsTopologicalAddGroup.

Main results

• Filter.ZeroAtFilter.sum: a finite sum of functions vanishing along l vanishes along l.
• Filter.BoundedAtFilter.sum: a finite sum of functions bounded along l is bounded along l.
• Filter.ZeroAtFilter.comp: a function vanishing along l, composed with a zero-preserving map continuous at 0, still vanishes along l.

Provenance

No code is transcribed. The gap was identified while porting the cusp chain of the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0), LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08: its heckeT_p_ut_zero_at_cusps (lines 62-70) open-codes precisely this induction with Finset.sum_induction, which is also the proof plan BoundedAtFilter.sum follows below. The statements here are about Mathlib's Filter.ZeroAtFilter / Filter.BoundedAtFilter at an arbitrary filter and index type, not about modular forms.

theorem Filter.ZeroAtFilter.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {l : Filter α} {s : Finset ι} {f : ι → α → β} [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] (h : ∀ i ∈ s, l.ZeroAtFilter (f i)) : l.ZeroAtFilter (∑ i ∈ s, f i)

A finite sum of functions vanishing along l vanishes along l. The additive companion of Filter.BoundedAtFilter.prod. The AddCommMonoid hypothesis is what Finset.sum requires.

theorem Filter.BoundedAtFilter.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {l : Filter α} {s : Finset ι} {f : ι → α → β} [SeminormedAddCommGroup β] (h : ∀ i ∈ s, l.BoundedAtFilter (f i)) : l.BoundedAtFilter (∑ i ∈ s, f i)

A finite sum of functions bounded along l is bounded along l — the additive companion of Filter.BoundedAtFilter.prod.

theorem Filter.ZeroAtFilter.comp {α : Type u_1} {β : Type u_2} {l : Filter α} {γ : Type u_4} [Zero β] [TopologicalSpace β] [Zero γ] [TopologicalSpace γ] {g : α → β} {φ : β → γ} (hg : l.ZeroAtFilter g) (hφ : ContinuousAt φ 0) (h0 : φ 0 = 0) : l.ZeroAtFilter (φ ∘ g)

A vanishing function stays vanishing under a zero-preserving map continuous at 0.

Only continuity at 0 is asked for. ZeroAtFilter is convergence to 0, so nothing about φ away from 0 is involved; requiring Continuous φ would be strictly stronger, and for a linear map the two coincide only when the topology is translation-invariant.

theorem Filter.ZeroAtFilter.of_eventually_eq_or_eq_zero {α : Type u_1} {β : Type u_2} {l : Filter α} [Zero β] [TopologicalSpace β] {f g : α → β} (hf : l.ZeroAtFilter f) (h : ∀ᶠ (a : α) in l, g a = f a ∨ g a = 0) : l.ZeroAtFilter g

Zeroing values keeps a function zero at a filter. If g eventually agrees with f or vanishes, then g inherits ZeroAtFilter: since 0 lies in every neighbourhood of 0, the preimage of such a neighbourhood under g contains the intersection of the one under f with the set where the hypothesis holds.

Only an eventual hypothesis is needed, because convergence along l sees g only through sets in l. Stated pointwise rather than for an indicator, so it carries no decidability hypothesis and also covers truncations that are not indicators.