A function that is a sum of said function

Stream: maths

[Mark Andrew Gerads]

The first step would be to change the statement to be in terms of the coefficients, which are equal to a sum of coefficients.
The next step would be to use modular arithmetic to show that the sum of ite simplifies to a single ite.
Here is my MWE (minimal working example):

import analysis.analytic.basic
import analysis.complex.basic

noncomputable theory

open formal_multilinear_series finset filter
open_locale nnreal ennreal big_operators

variables {𝕜 E : Type*} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E]
  [complete_space E] {p q : formal_multilinear_series 𝕜 𝕜 E} {n : ℕ} {f : 𝕜 → E} {w : 𝕜} {r : ennreal}

def plain_old_series (𝕜 : Type*) [nontrivially_normed_field 𝕜] {E : Type*}  [normed_add_comm_group E]
  [normed_space 𝕜 E] (a : ℕ → E) : formal_multilinear_series 𝕜 𝕜 E :=
λ n, continuous_multilinear_map.mk_pi_field 𝕜 (fin n) (a n)

------------------------

def rues_coeff (n : ℕ) (m : ℤ) (k : ℕ): ℂ := if ((k:ℤ) + m) % n = 0 then (1 : ℂ) / k.factorial else 0

def rues_series (n : ℕ) (m : ℤ) := plain_old_series ℂ (rues_coeff n m)

def ruesDiff (n : ℕ) (m : ℤ) : ℂ → ℂ := (rues_series n m).sum

lemma ruesDiffTsumForm (n:ℕ) (m:ℤ) (z:ℂ) : ruesDiff n m z = tsum (λ (k:ℕ), if ((k:ℤ)+m)%n=0 then z ^ k / k.factorial else 0) :=
begin
  sorry, --already proved, but here for reference
end

lemma ruesDiffSumOfRuesDiff (n k:ℕ) (h:0<n*k) (m:ℤ) (z:ℂ) : ruesDiff n m z = ∑ k₀ in range k, ruesDiff (n*k) (n*k₀+m) z:=
begin
  sorry, --what I need help proving
end

[Mark Andrew Gerads]

If anyone does not see motivation to proving this result, perhaps skimming https://github.com/Nazgand/nazgandMathBook/blob/master/RootOfUnityExponentialSumFunction.pdf and noting the lemma is a generalization of (5.3) would nerd-snipe someone into helping.

[Mark Andrew Gerads]

It seems to me that the easiest way to prove the sum of ite is an ite is to use the Type set Prop.
I have a rough draft of what this should look like. Please help. I don't even know how to define andSet, let alone how to properly define the output Type of iteSumOfIte.

import all
open_locale big_operators

-- andSet claims that every Prop in props is true
def andSet (props:set Prop) : Prop := sorry

lemma andSetElem (props:set Prop) (p:Prop) (h:p∈props) : andSet props → p := sorry

lemma andSetAndAndSet (props₀ props₁:set Prop) : (andSet props₀ ∧ andSet props₁) ↔ andSet (props₀ ∪ props₁) :=
begin
  sorry,
end

-- orSet claims that at least 1 Prop in props is true
def orSet (props:set Prop) : Prop := sorry

lemma orSetElem (props:set Prop) (p:Prop) (h:p∈props) : p → orSet props := sorry

-- mututallyExcusive claims that at most 1 Prop in props is true
def mutuallyExcusive (props:set Prop) : Prop := sorry
--  andSet {¬(h₀ ∧ h₁) | {h₀,h₁} ⊆ props ∧ h₀≠h₁} -- something like this but with init.data.set.set_of

-- exactly1True claims that exactly 1 Prop in props is true
def exactly1True (props:set Prop) : Prop := orSet props ∧ mutuallyExcusive props

-- decidableSet claims every Prop in props is decidable
def decidableSet (props:set Prop) : Prop := sorry
-- andSet {decidable p | p ∈ props} -- something like this but with init.data.set.set_of

noncomputable
lemma decidableSetElem (props:set Prop) (p:Prop) (h:p∈props) : decidableSet props → decidable p := sorry

lemma decidableSetSubset (props₀ props₁:set Prop) (h:props₀ ⊆ props₁) : decidableSet props₁ → decidableSet props₀ := sorry

noncomputable
lemma decidableSetAndSet (props:set Prop) : decidableSet props → decidable (andSet props) := sorry

noncomputable
lemma decidableSetOrSet (props:set Prop) : decidableSet props → decidable (orSet props) := sorry

-- having difficulty defining this lemma because of decidability
lemma iteSumOfIte (props:finset Prop) (h₀:exactly1True props) (h₁:decidableSet props) : ite (orSet props) 1 0 = ∑ p in props, ite p 1 0 :=
begin
  sorry, -- this is the needed proof
end

[Vincent Beffara]

Your andSetAndAndSet looks suspiciously like docs#Inf_union :-) have a look at docs#inf_Prop_eq and docs#Inf_Prop_eq

[Mark Andrew Gerads]

Any idea why iteSumOfIte is not accepted by the interpreter? It shows an error

failed to synthesize type class instance for
props : finset Prop,
h₀ : mutuallyExcusive ↑props,
h₁ : decidableSet ↑props
⊢ decidable (orSet ↑props)

[Jireh Loreaux]

it's trying to show that this is decidable, but can't find the type class instance (probably because it doesn't exist). Without really looking at any of this, but knowing that you have been working on things related to power series, my bet would be that you should just open classical at the top of the file, because I doubt you care about actual computability here. This will make everything decidable for you.

[Mark Andrew Gerads]

Thanks. I'll need to remember that. Edited. Next, mutuallyExcusive needs to be defined.

[Jireh Loreaux]

how about:

def mutuallyExcusive (props:set Prop) : Prop :=
∀ p q ∈ props, p → q → p = q

Note: I have not tried to understand why you are doing any of these set Prop manipulations, I'm just answering your questions briefly because I don't have much time. I suspect that for whatever you are trying to do, there is likely a much nicer way.

[Yaël Dillies]

mutuallyExclusive is docs#set.pairwise_disjoint

[Jireh Loreaux]

@Yaël Dillies Sorry, how is that exactly? What is the inf of two propositions?

[Adam Topaz]

I suppose it should be conjunction, but does Lean know that?

[Floris van Doorn]

src#Prop.distrib_lattice

[Yaël Dillies]

And orSet is of course just Sup.

[Yaël Dillies]

I think once you replace your adhoc constructions with the mathlib ones and generalize the 1 to anything, it's a fine lemma to have, if not a bit constricted.

[Yaël Dillies]

You can also prove the "dual" with Inf and prod, and write the multiplicative version.

[Mark Andrew Gerads]

I don't see any other way to prove the original problem without the lemma iteSumOfIte.
set.pairwise_disjoint asks for a function, though. Does the identity function work?
Is this right, @Yaël Dillies? I am not sure what you meant.
Also, I have been wondering how to prove iteSumOfIte. Induction on the set size seems like it might work, but I am unsure.

import algebra.big_operators.basic
import order.complete_lattice
import data.set.pairwise

open_locale classical big_operators

-- mututallyExclusive claims that at most 1 Prop in props is true
def mutuallyExclusive (props:set Prop) : Prop := set.pairwise_disjoint props id

lemma iteSumOfIte (props:finset Prop) (h₀:mutuallyExclusive props) : ite (Sup props) 1 0 = ∑ p in props, ite p 1 0 :=
begin
  sorry, -- this is the needed proof
end

[Eric Wieser]

@Mark Andrew Gerads, I'd strongly recommend dropping your camelCase naming convention and using the snake_case one prescribed by #naming. A powerful tool for working with mathlib is working out what the name of the result you want would be, and finding out if that name or similar already exists.

[Eric Wieser]

If you use your own naming scheme, you will never be told by Lean that the thing you're proving already exists!

[Vincent Beffara]

For the "at most one is true" you could build a function that counts how many of the props are true, using sum, so going from set Prop to nat (or enat if your sets can be infinite) and then state that this number is at most one.

[Vincent Beffara]

Although I agree that this feels quite contrived for what you want to do - but I am not completely sure that I understand what you want to do

[Mark Andrew Gerads]

@Vincent Beffara my main goal in this thread is to prove ruesDiffSumOfRuesDiff in the first post of this thread. Because the coefficients use an ite, this ultimately seems to require iteSumOfIte in my last post.

[Vincent Beffara]

Ah ok. There might be some case of #xy here but I think I see what you are looking for.

[Vincent Beffara]

The lemma that has to be in mathlib is that the sum of a non empty collection of nonnegative terms is at least equal to the largest term, and if you phrase "at least one" in terms of the sum on your this, which feels reasonable to me, then I would look in this direction

[Vincent Beffara]

Maybe something similar to docs#cardinal.supr_le_sum ?

[Vincent Beffara]

For your initial question, can you perhaps use docs#tsum_sum ?

[Yaël Dillies]

@Mark Andrew Gerads, yes set.pairwise_disjoint takes in an indexed family. In fact you could generalize your lemma to indexed families as well.

[Yaël Dillies]

Something like

(s : set \a).pairwise_disjoint f -> ite (\supr i \in s, f i) a 0 = \sum i in s, ite (f i) a 0

This allows you to apply it when you have several times false in the sum.

[Mark Andrew Gerads]

I just noticed a problem. Because sets can only contain 1 element once, and every Prop is either true or false, this means that $props \subseteq \{true,false\}$. props having at most 1 true statement is tautological.
I think I need props to be a list of Prop instead, so I need to read about lists in mathlib.

[Yaël Dillies]

Yaël Dillies said:

This allows you to apply it when you have several times false in the sum.

:point_up:

[Yaël Dillies]

To be explicit, you don't need lists, you need indexed families, which are a function ι → α along with a range of values you're interested in finset ι.

[Mark Andrew Gerads]

Okay, now I think I am asking for the right lemma. library_search failed. I have been thinking that if this is proved for n=2, that can be used for an inductive step. (n>0 and mutually_exclusive (range n:set ℕ) p) implies mutually_exclusive (range (n-1):set ℕ) p.
Also, ∃ k ∈ range n, p k=(p (n-1) or ∃ k ∈ range (n-1), p k), which is why I believe induction could work. I will think more about it later.

import algebra.big_operators.basic

open finset
open_locale classical big_operators

-- mutually_exclusive claims that at most 1 Prop is true in the indexed family I,p
def mutually_exclusive {α:Type} (I:set α) (p:α → Prop) : Prop := ∀ i₀ i₁ ∈ I, p i₀ ∧ p i₁ → i₀ = i₁

lemma ite_sum_of_ite {n:ℕ} {p:ℕ → Prop} (h₀:mutually_exclusive (range n:set ℕ) p) :
      ite (∃ k ∈ range n, p k) 1 0 = ∑ k in range n, ite (p k) 1 0 :=
begin
  sorry, -- this is the needed proof
end

[Yaël Dillies]

Read my messages :upside_down:

[Yaël Dillies]

The reasonlibrary_search failed is that you didn't teach it enough. Firstly, it doesn't know anything about mutually_exclusive so you can't expect it to do anything with that. Second it would only find exact matches, which we ruled out as the lemma doesn't exist in the library.

[Yaël Dillies]

Anyway, here is your lemma #16825

[Eric Wieser]

#16825?

[Yaël Dillies]

Yep, sorry. Keyboard should go to bed.

[Mark Andrew Gerads]

@Yaël Dillies Thank you very much for the lemma. It is quite helpful.

[Eric Wieser]

I'm not sure the lemma is actually that useful; you can immediately simplify the RHS with docs#finset.prod_filter and docs#finset.prod_const

[Eric Wieser]

Then we find that the actual lemma that is missing is that s.filter f = {a} when a ∈ s and pairwise s f

[Mark Andrew Gerads]

I don't care about the finer details too much; my main goal right now is ruesDiffSumOfRuesDiff.
I am waiting on the PR now though, so please decide whatever needs to be decided to pull the PR. If the suggested filter version is pulled, I'll just need to learn to use filters.

[Eric Wieser]

Note that docs#finset.filter is not related to "filters" (docs#filter)