Zulip Chat Archive

Stream: maths

Topic: A function that is a sum of said function


Mark Andrew Gerads (Oct 02 2022 at 05:01):

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 (Oct 02 2022 at 06:54):

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 (Oct 03 2022 at 14:34):

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:pprops) : 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:pprops) : 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:pprops) : 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 (Oct 03 2022 at 14:43):

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

Mark Andrew Gerads (Oct 03 2022 at 15:19):

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 (Oct 03 2022 at 15:26):

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 (Oct 03 2022 at 15:57):

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

Jireh Loreaux (Oct 03 2022 at 16:15):

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 (Oct 03 2022 at 16:17):

mutuallyExclusive is docs#set.pairwise_disjoint

Jireh Loreaux (Oct 03 2022 at 16:26):

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

Adam Topaz (Oct 03 2022 at 16:28):

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

Floris van Doorn (Oct 03 2022 at 16:28):

src#Prop.distrib_lattice

Yaël Dillies (Oct 03 2022 at 16:31):

And orSet is of course just Sup.

Yaël Dillies (Oct 03 2022 at 16:32):

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 (Oct 03 2022 at 16:39):

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

Mark Andrew Gerads (Oct 03 2022 at 16:46):

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 (Oct 03 2022 at 16:58):

@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 (Oct 03 2022 at 16:59):

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

Vincent Beffara (Oct 03 2022 at 17:00):

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 (Oct 03 2022 at 17:01):

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 (Oct 03 2022 at 17:06):

@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 (Oct 03 2022 at 17:10):

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

Vincent Beffara (Oct 03 2022 at 17:13):

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 (Oct 03 2022 at 17:14):

Maybe something similar to docs#cardinal.supr_le_sum ?

Vincent Beffara (Oct 03 2022 at 17:24):

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

Yaël Dillies (Oct 03 2022 at 19:04):

@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 (Oct 03 2022 at 19:06):

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 (Oct 05 2022 at 08:49):

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{true,false}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 (Oct 05 2022 at 08:50):

Yaël Dillies said:

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

:point_up:

Yaël Dillies (Oct 05 2022 at 08:56):

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 (Oct 05 2022 at 11:59):

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 (Oct 05 2022 at 21:38):

Read my messages :upside_down:

Yaël Dillies (Oct 05 2022 at 21:40):

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 (Oct 05 2022 at 21:40):

Anyway, here is your lemma #16825

Eric Wieser (Oct 05 2022 at 22:02):

#16825?

Yaël Dillies (Oct 05 2022 at 22:03):

Yep, sorry. Keyboard should go to bed.

Mark Andrew Gerads (Oct 06 2022 at 00:01):

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

Eric Wieser (Oct 06 2022 at 00:19):

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 (Oct 06 2022 at 00:21):

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 (Oct 07 2022 at 15:22):

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 (Oct 08 2022 at 17:23):

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


Last updated: Dec 20 2023 at 11:08 UTC