Zulip Chat Archive
Stream: new members
Topic: multivariable sum function
jachym simon (Feb 09 2022 at 11:32):
Hi, i am working with multivariable functions of shape
$f(x_{1},...,x_{n}) = a + \sum_{i=1}^{n}b_{i}x_{i}.$
I need some kind of access to the coefficients, since i want to define a sum of absolute values of them
$s = \sum_{i=1}^{n}b_i$
and further down the line i want to define a set using just positive/negative coefficients
$PF(f) = \bigcup\limits_{b_i > 0} \{something\}.$
Is there any chance something like this is already defined in mathlib or do i have to define it myself? I was trying to look for this, but wasn't successful.
Eric Wieser (Feb 09 2022 at 13:14):
Any reason not to just use
def your_fun (a : R) (b x : fin n → R) : R := a + ∑ i, b i * x i
And then you will not need to extract a
and b
as you'll already have them
Alex J. Best (Feb 09 2022 at 14:08):
That would be a good way to go you could then use docs#matrix.dot_product to express the sum and use some of the lemmas there
jachym simon (Feb 10 2022 at 13:10):
Thank you for your answers. No reason really, i'm just not that great with lean hehe. This seems nice, i am not successful though with defining the PF(f) set yet (the set is a bit more complicated then i wrote above), so i might come back later with further questions.
jachym simon (Feb 18 2022 at 22:22):
I am playing around with the suggested definition. Seems it might work, but there are still some question marks. For example how can i prove the following?
example (m n : ℕ) (b: fin n → ℤ) (j: fin n) (hb: b j < 0) (hs: ∑ i, (b i).nat_abs = m + 1)
: ∑ i, (b i + ite (i = j) 1 0).nat_abs = m := sorry
Alex J. Best (Feb 18 2022 at 22:48):
Its easier to help if you provide a #mwe (with all imports and locales included.
Alex J. Best (Feb 18 2022 at 22:49):
Probably you want to add a few more lemmas to make some of the step here easier, but here is a rough outline with some sorries
import algebra.big_operators
open_locale big_operators
example (m n : ℕ) (b: fin n → ℤ) (j: fin n) (hb: b j < 0) (hs: ∑ i, (b i).nat_abs = m + 1) :
∑ i, (b i + ite (i = j) 1 0).nat_abs = m :=
begin
have hj : j ∈ finset.univ := finset.mem_univ _,
rw finset.sum_eq_sum_diff_singleton_add hj,
simp,
have : ∀ (x : fin n) (hx : x ∈ (finset.univ \ {j} : finset (fin n))), ¬ x = j,
sorry,
conv in (ite _ _ _) {
rw if_neg (this x H), },
simp,
have : (b j + 1).nat_abs = (b j).nat_abs  1,
sorry,
rw [this, ← nat.add_sub_assoc, ← finset.sum_eq_sum_diff_singleton_add hj,
hs, nat.add_succ_sub_one, add_zero],
sorry
end
jachym simon (Feb 18 2022 at 23:04):
Alex J. Best said:
Its easier to help if you provide a #mwe (with all imports and locales included.
Yes, sorry
jachym simon (Feb 18 2022 at 23:10):
Alex J. Best said:
Probably you want to add a few more lemmas to make some of the step here easier, but here is a rough outline with some sorries
import algebra.big_operators open_locale big_operators example (m n : ℕ) (b: fin n → ℤ) (j: fin n) (hb: b j < 0) (hs: ∑ i, (b i).nat_abs = m + 1) : ∑ i, (b i + ite (i = j) 1 0).nat_abs = m := begin have hj : j ∈ finset.univ := finset.mem_univ _, rw finset.sum_eq_sum_diff_singleton_add hj, simp, have : ∀ (x : fin n) (hx : x ∈ (finset.univ \ {j} : finset (fin n))), ¬ x = j, sorry, conv in (ite _ _ _) { rw if_neg (this x H), }, simp, have : (b j + 1).nat_abs = (b j).nat_abs  1, sorry, rw [this, ← nat.add_sub_assoc, ← finset.sum_eq_sum_diff_singleton_add hj, hs, nat.add_succ_sub_one, add_zero], sorry end
Thank you! Unfortunately, it says this at the second line
unknown identifier 'finset.sum_eq_sum_diff_singleton_add'
Is it possible the lemma is not in my mathlib?
Alex J. Best (Feb 18 2022 at 23:14):
That would be really surprising, it looks like that lemma has been there for quite a while, what version of mathlib is it / how did you add it?
jachym simon (Feb 18 2022 at 23:44):
Not sure, seems like my mathlib version is 0.1, could that be? But i think ill try to reinstall lean and mathlib on my computer completely (i wanted to do it anyway)
Kevin Buzzard (Feb 18 2022 at 23:46):
Here's how to get an up to date Lean and mathlib: https://leanprovercommunity.github.io/get_started.html
Alex J. Best (Feb 19 2022 at 00:01):
They all say version 0.1 actually, the thing to look for is the git commit, or when you last updated mathlib (did you just download mathlib, or some other project that uses it?)
jachym simon (Feb 21 2022 at 20:50):
@Alex J. Best I ended up reinstalling and now everything is up and running, including your lemma. Thanks :)
jachym simon (Feb 24 2022 at 08:26):
(deleted)
jachym simon (Feb 24 2022 at 09:24):
hi, following up on the above, the set $PF(f)$ i wanted to define is created using induction on $s(f)$ (see below). It is a set of logical formulas and its constructed like this (the meaning of $\oplus$ and $\&$ is not important):
Have $f(x_{1},...,x_{n}) = a + \sum_{i=1}^{n}b_{i}x_{i}$ and $s(f) = \sum_{i=1}^{n}b_i$. Have $X = \{X_1, .... X_n\}$ set of logical formulas.

$s(f) = 0:$
$a > 0$ then $PF(f) = \{X_i \to X_i : i=1,2,3...,n \}$
$a \le 0$ then $PF(f) = \{\neg (X_i \to X_i) : i=1,2,3...,n \}$ 
$s(f) = m$
$PF(f) = (\bigcup_{b_i>0} \{ (Q \oplus X_i) \& R : Q \in PF(f  x_i), R \in PF(f + 1  x_i) \} )\newline \cup \newline (\bigcup_{b_i<0} \{ (Q \oplus \neg X_i) \& R : Q \in PF(f + x_i  1), R \in PF(f + x_i) \})$
Definition is correct, because if $s(f) = m$ and $b_i > 0$ then $s(f  x_i) = m  1$ etc.
I managed to formalize it in lean in the following way, now i am proving some further lemmas and is seems to do what i want. But i don't know whether there isn't a better/simpler way. So, finally the question  is my formalization fine or can it be improved?
import algebra.big_operators
open_locale big_operators
 definition of logical formulas
inductive Form : Type
 p : ℕ → Form
 imp : Form → Form → Form
 neg : Form → Form
infixr `=>` : 80 := Form.imp
prefix `~` : 100 := Form.neg
notation P ` & ` Q := ~(P => ~Q)
notation P ` ⊕ ` Q := ~P => Q
 definition of f = a + ∑ i, bi*xi
def poly_fun (n : ℕ) := ℤ × (fin n → ℤ)
variable{n:ℕ}
def xj (j:fin n): poly_fun n :=
⟨0, (λ i, if i = j then 1 else 0)⟩
def cons (a : ℤ): poly_fun n :=
⟨a, (λ i, 0)⟩
def poly_fun.val (x:fin n → ℚ): poly_fun n → ℚ :=
by intro f; exact (f.1 + ∑ i, f.2 i * x i)
def poly_fun.degree (f : poly_fun n) : ℕ := ∑ i, (f.2 i).nat_abs
def add : poly_fun n → poly_fun n → poly_fun n :=
by intros f g; exact ⟨f.1 + g.1, (λ i, f.2 i + g.2 i)⟩
def sub : poly_fun n → poly_fun n → poly_fun n :=
by intros f g; exact ⟨f.1  g.1, (λ i, f.2 i  g.2 i)⟩
infix `⊹` : 100 := add
infix `−` : 100 := sub
prefix `σ` : 100 := poly_fun.degree
prefix `C` : 100 := cons
 help lemmas for definition
lemma sum_abs_gt_degree {m n : ℕ}(f : poly_fun n)(j : fin n)(hb : f.2 j > 0)(hf: σ f = m + 1)
: σ (f − xj j) = m := sorry
lemma sum_abs_lt_degree {m n : ℕ}(f : poly_fun n)(j : fin n)(hb : f.2 j < 0)(hf: σ f = m + 1)
: σ (f ⊹ xj j) = m := sorry
 definition of PF(f)
def PF (X : fin n → Form): ∀ {m : ℕ}, ∀ f : poly_fun n, ∀ hf: σ f = m, set Form
 0 := begin intros, by_cases (f.1:ℚ) > 0,
exact {K  ∃ i, K = X i => X i},
exact {K  ∃ i, K = ~(X i => X i)}
end
 (m+1) := begin
intros f hf,
have h_pos: ∀ j : fin n, f.2 j > 0 → σ (f − xj j) = m,
intros j hbb, exact (sum_abs_gt_degree f j hbb (hf)),
have h_pos_one: ∀ j : fin n, f.2 j > 0 → σ (f ⊹ (cons 1) − xj j) = m,
simp[cons, add], exact h_pos,
have h_neg: ∀ j : fin n, f.2 j < 0 → σ (f ⊹ xj j) = m,
intros j hbb, exact (sum_abs_lt_degree f j hbb hf),
have h_neg_one: ∀ j : fin n, f.2 j < 0 → σ (f − (cons 1) ⊹ xj j) = m,
simp[cons, add, sub], exact h_neg,
exact ⋃ i, by{by_cases (f.2 i) > 0,
exact {K  ∃ Q ∈ (PF (f − xj i) (h_pos i h)),
∃ R ∈ (PF (f ⊹ (cons 1) − xj i) (h_pos_one i h)),
K = ((Q⊕X i)&R)},
simp at h,
by_cases h_1: f.2 i = 0,
exact {},
have h2: f.2 i < 0, exact (ne.le_iff_lt h_1).mp h,
exact {K  ∃ Q ∈ (PF (f − (cons 1) ⊹ xj i) (h_neg_one i h2)),
∃ R ∈ (PF (f ⊹ xj i) (h_neg i h2)),
K = ((Q⊕~X i)&R)}},
end
Last updated: Dec 20 2023 at 11:08 UTC