multivariable sum function

Stream: new members

[jachym simon]

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]

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]

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]

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]

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]

Its easier to help if you provide a #mwe (with all imports and locales included.

[Alex J. Best]

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]

Alex J. Best said:

Its easier to help if you provide a #mwe (with all imports and locales included.

Yes, sorry

[jachym simon]

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]

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]

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]

Here's how to get an up to date Lean and mathlib: https://leanprover-community.github.io/get_started.html

[Alex J. Best]

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]

@Alex J. Best I ended up reinstalling and now everything is up and running, including your lemma. Thanks :)

[jachym simon]

(deleted)

[jachym simon]

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,
    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