## 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 _,
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,
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 _,
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,
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://leanprover-community.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 :)

(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.

1. $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 \}$

2. $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,
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,
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