If `f` has finite fibers than also `Finsupp.mapDomain` do

Stream: Is there code for X?

[Riccardo Brasca]

Am I reinventing the wheel here?

import Mathlib

variable (σ τ : Type*) (f : σ → τ)

open Function Filter Finsupp

example (hf : Tendsto f cofinite cofinite) (n : τ →₀ ℕ) : ((mapDomain f) ⁻¹' {n}).Finite := by
  have hF : (support (n ∘ f)).Finite := by
    simpa [support_eq_preimage, Set.preimage_compl, Set.preimage_comp] using hf n.finite_support
  refine BddAbove.finite ⟨ofSupportFinite _ hF, fun a ha i ↦ ?_⟩
  by_cases h : i ∈ a.support
  · simp only [Set.mem_preimage, mapDomain, Finsupp.sum, Set.mem_singleton_iff] at ha
    simpa [ha] using Finset.sum_le_sum_of_subset_of_nonneg (show {i} ⊆ a.support by simp [h])
      (f := fun x ↦ Finsupp.single (f x) (a x)) (by simp)
  · simp [Finsupp.not_mem_support_iff.mp h]

Note that Tendsto f cofinite cofinite just means that f has finite fibers (if someone know a more mathlib way of saying this I am open to suggestion). It's not clear to me if we have a typeclass that allows to replace ℕ by something else (surely it needs to be locally finite, but it is not enough).

[Aaron Liu]

Riccardo Brasca said:

It's not clear to me if we have a typeclass that allows to replace ℕ by something else (surely it needs to be locally finite, but it is not enough).

Is it not necessary and sufficient for (uncurried) addition to have finite fibers?

[Riccardo Brasca]

Yes, mathematically that's the point. I don't know if we have a typeclass for that (or at least enough for that)

[Junyan Xu]

An equivalent statement (using docs#Finsupp.toMultiset_map) is that Multiset.map f also have finite fibers if f does.

[Junyan Xu]

(uncurried) addition to have finite fibers

This condition is also what allows us to define multiplication on MvPowerSeries

[Riccardo Brasca]

Indeed this come up in working with power series

[Aaron Liu]

Riccardo Brasca said:

Yes, mathematically that's the point. I don't know if we have a typeclass for that (or at least enough for that)

Oh, it's docs#Finset.HasAntidiagonal

[Riccardo Brasca]

Ah nice!

[Riccardo Brasca]

Mmm, I now think it is not enough

[Riccardo Brasca]

I mean, we cannot replace N by any addcomm monoid A that has an antidiagonal.

[Riccardo Brasca]

Ok I may be confused, I will think about it next week

[Junyan Xu]

I think we also need that if 0=a+b then a=b=0 (if σ is infinite)

[Riccardo Brasca]

Yep I have a counterexample if this is not the case

[Aaron Liu]

So far

import Mathlib

theorem Set.preimage_insert {α β : Type*} (f : α → β) (x : β) (s : Set β) : f ⁻¹' (insert x s) = f ⁻¹' {x} ∪ f ⁻¹' s := by
  simp [Set.insert_eq, -Set.singleton_union]

theorem Filter.tendsto_cofinite_cofinite {α β : Type*} (f : α → β) :
    Filter.Tendsto f Filter.cofinite Filter.cofinite ↔ ∀ x, (f ⁻¹' {x}).Finite := by
  constructor
  · intro h x
    rw [← compl_compl (f ⁻¹' {x}), ← Filter.mem_cofinite, ← Set.preimage_compl, ← Filter.mem_map]
    apply h
    rw [Filter.mem_cofinite, compl_compl]
    exact Set.finite_singleton x
  · intro h s hs
    rw [Filter.mem_map, Filter.mem_cofinite, ← Set.preimage_compl]
    rw [Filter.mem_cofinite] at hs
    generalize sᶜ = s at *
    induction s, hs using Set.Finite.induction_on with
    | empty => simp
    | @insert x s hx hs ih =>
      rw [Set.preimage_insert, Set.finite_union]
      exact ⟨h x, ih⟩

theorem Finsupp.single_apply_self {α M : Type*} [Zero M] (a : α) (b : M) : (fun₀ | a => b) a = b :=
  let _ := isTrue (Eq.refl a)
  Finsupp.single_apply

variable {σ τ A : Type*} [AddCommMonoid A] [Subsingleton (AddUnits A)] [Finset.HasAntidiagonal A] (f : σ → τ)

open Function Filter Finsupp Set

example (hf : Tendsto f cofinite cofinite) : Tendsto (mapDomain (M := A) f) cofinite cofinite := by
  rw [tendsto_cofinite_cofinite] at hf ⊢
  intro n
  induction n using Finsupp.induction with
  | zero =>
    suffices h : mapDomain (M := A) f ⁻¹' {0} = {0} from h ▸ finite_singleton 0
    ext n
    simp_rw [mem_preimage, mem_singleton_iff, Finsupp.ext_iff, zero_apply,
      mapDomain, sum_apply, sum, Finset.sum_eq_zero_iff, Finsupp.single_apply_eq_zero]
    conv_lhs =>
      rw [forall_comm]
      intro i
      rw [forall_comm]
      intro hi t
      rw [eq_false (mem_support_iff.mp hi)]
    simp_rw [forall_eq, imp_false, ← Finset.eq_empty_iff_forall_not_mem, support_eq_empty, Finsupp.ext_iff, zero_apply]
  | single_add a b n ha hb ih =>
    suffices hsingle : (mapDomain f ⁻¹' {fun₀ | a => b}).Finite by
      sorry
    sorry