downsets in orders

Stream: general

[Johan Commelin]

Do we have notation for the set of all terms smaller than a given term?

[Johan Commelin]

I need to fill in the following sorrys:

import data.finsupp order.complete_lattice algebra.ordered_group

namespace finsupp
open lattice
variables {σ : Type*} {α : Type*} [decidable_eq σ]

instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
{ le := λ f g, ∀ s, f s ≤ g s,
  le_refl := λ f s, le_refl _,
  le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }

instance [partial_order α] [has_zero α] : partial_order (σ →₀ α) :=
{ le_antisymm := λ f g hfg hgf, finsupp.ext $ λ s, le_antisymm (hfg s) (hgf s),
  .. finsupp.preorder }

instance [canonically_ordered_monoid α] : order_bot (σ →₀ α) :=
{ bot := 0,
  bot_le := λ f s, zero_le _,
  .. finsupp.partial_order }

def downset [preorder α] (a : α) := {x | x ≤ a}

lemma nat_downset (f : σ →₀ ℕ) : finset (σ →₀ ℕ) := sorry

lemma nat_downset_eq_downset (f : σ →₀ ℕ) :
  (↑(nat_downset f) : set (σ →₀ ℕ)) = downset f := sorry

end finsupp

[Johan Commelin]

But this seems like I need to write some algorith that works on lists and multisets, because those are used under the hood in the support of finitely supported functions.

[Johan Commelin]

Any hints (or complete implementations) very much appreciated.

[Chris Hughes]

finset.filter on the support.

[Johan Commelin]

@Chris Hughes I have no idea how that would help me building the downset...

[Johan Commelin]

I guess I need to define pointwise addition for finsets. Then I can use finset.fold on the support with pointwise_add and map single s n to finset.map (finset.range (n+1)) (single s).

[Johan Commelin]

Might as well use finset.sum (-;
I'll start working on pointwise operations for finset.

[Neil Strickland]

There is some stuff at https://github.com/NeilStrickland/lean_lib/blob/master/src/homotopy/upper.lean which might possibly be useful.

[Kenny Lau]

def nat_downset (f : σ →₀ ℕ) : finset (σ →₀ ℕ) :=
(f.support.pi (λ x, finset.range $ f x + 1)).image $
λ g, f.support.attach.sum $ λ i, finsupp.single i.1 $ g i.1 i.2

theorem sum_apply' [decidable_eq α] [add_comm_monoid α] {β : Type w} {f : β → σ →₀ α} {ι : finset β} {i : σ} :
  ι.sum f i = ι.sum (λ x, f x i) :=
by classical; exact finset.induction_on ι rfl (λ x s hxs ih,
by rw [finset.sum_insert hxs, add_apply, ih, finset.sum_insert hxs])

lemma nat_downset_eq_downset (f : σ →₀ ℕ) :
  (↑(nat_downset f) : set (σ →₀ ℕ)) = downset f :=
begin
  ext g, simp only [finset.mem_coe, nat_downset, finset.mem_image], split,
  { rintros ⟨g, hg, rfl⟩ i,
    rw [finset.mem_pi] at hg,
    rw [sum_apply'],
    by_cases hi : i ∈ f.support,
    { rw finset.sum_eq_single (⟨i, hi⟩ : (↑f.support : set σ)),
      rw [single_apply, if_pos rfl],
      specialize hg i hi,
      rw [finset.mem_range, nat.lt_succ_iff] at hg,
      exact hg,
      { intros j hj hji, rw [single_apply, if_neg], refine mt _ hji, intros hji', exact subtype.eq hji' },
      { intro hi', exact hi'.elim (finset.mem_attach _ _) } },
    { rw finset.sum_eq_zero, exact nat.zero_le _,
      intros j hj, rw [single_apply, if_neg], rintros rfl, exact hi j.2 } },
  { intros hg, refine ⟨λ i hi, g i, _, _⟩,
    { rw finset.mem_pi, intros i hi, rw [finset.mem_range, nat.lt_succ_iff], exact hg i },
    { ext i, rw sum_apply',
      by_cases hi : i ∈ f.support,
      { rw finset.sum_eq_single (⟨i, hi⟩ : (↑f.support : set σ)),
        rw [single_apply, if_pos rfl],
        { intros j hj hji, rw [single_apply, if_neg], refine mt _ hji, intros hji', exact subtype.eq hji' },
        { intro hi', exact hi'.elim (finset.mem_attach _ _) } },
      { rw finset.sum_eq_zero, rw not_mem_support_iff at hi, symmetry,
        exact nat.eq_zero_of_le_zero (hi ▸ hg i),
        { intros j hj, rw [single_apply, if_neg], rintros rfl, exact hi j.2 } } } }
end

[Johan Commelin]

@Kenny Lau Thanks! That's quite a long proof actually.

[Kenny Lau]

it might be able to be broken down into lemmas / constructions

[Johan Commelin]

I wish we knew the following:

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n) :
  coeff n (φ * ψ) = finset.sum (finsupp.nat_downset n) (λ m, coeff m φ * coeff (n - m) ψ) := sorry

Making slow progress...

[Kenny Lau]

we have a similar theorem for polynomials right

[Johan Commelin]

Do we?

[Johan Commelin]

Aah, you mean single variable polynomials?

[Johan Commelin]

Possibly

[Mario Carneiro]

isn't there something like multiset.diagonal that gives you all the sub-multisets and their complements?