## Stream: new members

### Topic: sum of two negligible function is also a negligible function

#### Mukesh Tiwari (Jul 12 2020 at 07:28):

I am trying to prove that sum of two negligible functions are negligible, but I am stuck with this goal:

tactic failed, there are unsolved goals
state:
μ₁ μ₂ : ℕ → ℚ,
H₁ : ∀ (c : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n ≥ n₀ → μ₁ n * ↑n ^ c < 1,
H₂ : ∀ (c : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n ≥ n₀ → μ₂ n * ↑n ^ c < 1,
c n₁ n₂ n : ℕ,
Hn : n ≥ max n₁ (max n₂ 2),
Ht : n ≥ n₁ ∧ n ≥ max n₂ 2,
Ht₁ : n ≥ n₁,
Ht₃ : n ≥ n₂ ∧ n ≥ 2,
Ht₂ : n ≥ n₂,
Ht₃ : n ≥ 2,
Hn₁ : μ₁ n * ↑n ^ (c + 2) < 1,
Hn₂ : μ₂ n * ↑n ^ (c + 2) < 1
⊢ (μ₁ n + μ₂ n) * ↑n ^ c < 1


Based on my calculation, unless I missed something very obvious, adding
Hn₁ : μ₁ n * ↑n ^ (c + 2) < 1,
Hn₂ : μ₂ n * ↑n ^ (c + 2) < 1
would give me ( μ₁ n + μ₂ n) * ↑n ^ c * ↑n ^ 2 < 2 . Since n ≥ 2 (Ht₃ ), 2/↑n ^ 2 < 1 which proves the goal. Below is the complete working code:

import data.nat.basic
data.rat.basic data.rat.order
tactic.omega

def neg_fn (μ : ℕ → ℚ) : Prop :=
∀ (c : ℕ), ∃ (n₀ : ℕ),
∀ (n : ℕ), n ≥ n₀ → (μ n) * (n ^ c) < 1

def sum_neg_fn (μ₁ μ₂ : ℕ → ℚ) : ℕ → ℚ :=
λ (n : ℕ), μ₁ n + μ₂ n

theorem upper_bound_max : ∀ (n n₁ n₂ : ℕ), n ≥ max n₁ n₂ → n ≥ n₁ ∧ n ≥ n₂ :=
begin
intros n₁ n₂ Hn, exact max_le_iff.mp
end

theorem sum_neg_fn_is_neg_fn :
∀ (μ₁ μ₂ : ℕ → ℚ), neg_fn μ₁ → neg_fn μ₂ → neg_fn (sum_neg_fn μ₁ μ₂) :=
begin
unfold sum_neg_fn neg_fn, intros μ₁ μ₂ H₁ H₂ c,
destruct (H₁ (c + 2)), intros n₁ Hn₁,
destruct (H₂ (c + 2)), intros n₂ Hn₂,
existsi (max n₁ (max n₂ 2)), intros n Hn,
have Ht : n ≥ n₁ ∧  n ≥ max n₂ 2 := begin
apply upper_bound_max, apply_assumption,
end,
destruct Ht, intros Ht₁ Ht₂,
have Ht₃ : n ≥ n₂ ∧ n ≥ 2 := begin
apply upper_bound_max, apply_assumption,
end, clear Ht₂,
destruct Ht₃, intros Ht₂ Ht₃,
specialize (Hn₁ n Ht₁), specialize (Hn₂ n Ht₂),
/- How to finish rest -/
end


#### Kyle Miller (Jul 12 2020 at 09:26):

So far so good. I modified your tactics to look more like idiomatic Lean (as far as I understand it), and after a good amount of library_search, I found the following proof:

import data.nat.basic
import data.rat.basic
import data.rat.order
import tactic

def neg_fn (μ : ℕ → ℚ) : Prop :=
∀ (c : ℕ), ∃ (n₀ : ℕ),
∀ (n : ℕ), n₀ ≤ n → (μ n) * (n ^ c) < 1

def sum_neg_fn (μ₁ μ₂ : ℕ → ℚ) : ℕ → ℚ :=
λ (n : ℕ), μ₁ n + μ₂ n

theorem sum_neg_fn_is_neg_fn :
∀ (μ₁ μ₂ : ℕ → ℚ), neg_fn μ₁ → neg_fn μ₂ → neg_fn (sum_neg_fn μ₁ μ₂) :=
begin
intros μ₁ μ₂ H₁ H₂ c,
cases H₁ (c + 2) with n₁ Hn₁,
cases H₂ (c + 2) with n₂ Hn₂,
use max n₁ (max n₂ 2), intros n Hn,
repeat { rw max_le_iff at Hn },
rcases Hn with ⟨Ht₁, Ht₂, Ht₃⟩,
specialize Hn₁ n Ht₁,
specialize Hn₂ n Ht₂,
dunfold sum_neg_fn,
rw [pow_add, ←mul_assoc] at Hn₁ Hn₂,
have npos : 0 < (↑n : ℚ), { norm_cast, linarith },
have hsqp : 0 < (↑n : ℚ) ^ 2 := pow_pos npos 2,
rw ←lt_div_iff hsqp at Hn₁ Hn₂,
have Ht₃' : (4 : ℚ) ≤ (↑n : ℚ)^2,
{ norm_cast, exact nat.pow_le_pow_of_le_left Ht₃ 2 },
have Ht₃'' : 1/(↑n : ℚ)^2 ≤ 1/(4 : ℚ),
{ exact div_le_div_of_le_left zero_le_one (by linarith) Ht₃' },
linarith [Hn₁, Hn₂, Ht₃''],
end


#### Kyle Miller (Jul 12 2020 at 09:28):

One curiosity is that changing the proof of Ht₃'' to be term mode and not exact causes Lean to time out. I have no idea why this is.

#### Kyle Miller (Jul 12 2020 at 09:39):

Also, to get the max_le_iff rewrite to work, I changed the inequality in neg_fn to n₀ ≤ n. Lean tends to prefer ≤ since ≥ is defined in terms of it.

#### Kyle Miller (Jul 12 2020 at 09:44):

A question of my own: does mathlib have pointwise addition of functions? It seems like something like sum_neg_fn should be defined already.

#### Kyle Miller (Jul 12 2020 at 09:55):

Great!

In that case, this can be given as

import data.nat.basic
import data.rat.basic
import data.rat.order
import algebra.pi_instances
import tactic

def neg_fn (μ : ℕ → ℚ) : Prop :=
∀ (c : ℕ), ∃ (n₀ : ℕ),
∀ (n : ℕ), n₀ ≤ n → (μ n) * (n ^ c) < 1

theorem sum_neg_fn_is_neg_fn :
∀ (μ₁ μ₂ : ℕ → ℚ), neg_fn μ₁ → neg_fn μ₂ → neg_fn (μ₁ + μ₂) :=
begin
intros μ₁ μ₂ H₁ H₂ c,
cases H₁ (c + 2) with n₁ Hn₁,
cases H₂ (c + 2) with n₂ Hn₂,
use max n₁ (max n₂ 2), intros n Hn,
repeat { rw max_le_iff at Hn },
rcases Hn with ⟨Ht₁, Ht₂, Ht₃⟩,
specialize Hn₁ n Ht₁,
specialize Hn₂ n Ht₂,
rw [pow_add, ←mul_assoc] at Hn₁ Hn₂,
have npos : 0 < (↑n : ℚ), { norm_cast, linarith },
have hsqp : 0 < (↑n : ℚ) ^ 2 := pow_pos npos 2,
rw ←lt_div_iff hsqp at Hn₁ Hn₂,
have Ht₃' : (4 : ℚ) ≤ (↑n : ℚ)^2,
{ norm_cast, exact nat.pow_le_pow_of_le_left Ht₃ 2 },
have Ht₃'' : 1/(↑n : ℚ)^2 ≤ 1/(4 : ℚ),
{ exact div_le_div_of_le_left zero_le_one (by linarith) Ht₃' },
linarith [Hn₁, Hn₂, Ht₃''],
end


#### Kyle Miller (Jul 12 2020 at 10:02):

It is perhaps nicer to write the theorem statement as

theorem sum_neg_fn_is_neg_fn (μ₁ μ₂ : ℕ → ℚ) (H₁ : neg_fn μ₁) (H₂ : neg_fn μ₂) : neg_fn (μ₁ + μ₂)


and then adjust the intros to intro c accordingly.

Or, it could even be given with implicit arguments

theorem sum_neg_fn_is_neg_fn {μ₁ μ₂ : ℕ → ℚ} (H₁ : neg_fn μ₁) (H₂ : neg_fn μ₂) : neg_fn (μ₁ + μ₂)


since the functions can be inferred from H₁ and H₂.

#### Mukesh Tiwari (Jul 12 2020 at 10:36):

@Kyle Miller Thank you very much. I have a question: how did you find this lemma by lt_div_iff library search (to pattern match something in the assumptions and find the lemma)? What my understanding of library_search is: when I write library_search, it pattern matches the goal and try to come up with matching lemmas, and if it can not find any, then it fails. I have no idea how to use library_search to pattern match in assumptions.

#### Kevin Buzzard (Jul 12 2020 at 10:52):

@Mukesh Tiwari you can find lt_div_iff by guessing that this is what it is called. This is a really important technique. You try lt_div because one side is a < b / c and then you hit ctrl-space and you can see all Lean theorems which have lt_div in, and you scroll up and down with the arrow keys to find the one you want. See https://youtu.be/bghu6jVt0SY?t=320

#### Mukesh Tiwari (Jul 12 2020 at 11:06):

Thank you very much everyone for answering my questions patiently.

#### Kyle Miller (Jul 12 2020 at 20:04):

@Mukesh Tiwari I wasn't able to guess what it was called in this case out of inexperience, so what I did was create a new goal with the single transform I wanted to do:

have h : μ₁ n * ↑n ^ c < 1 / ↑n ^ 2, { library_search },


Then Lean responded with

Try this: exact (lt_div_iff hsqp).mpr Hn₁


and then I modified this suggested tactic to use rw since it could apply to both hypotheses.

One complication was that I knew the theorem would need to know n^2 > 0, so I made sure to prove that first. For (4 : ℚ) ≤ (↑n : ℚ)^2, I did a norm_cast first to turn it into 4 ≤ n^2, since I figured there would be a theorem about this for the naturals already, and that's when I used library_search again, even though I probably could have guessed the name.

Last updated: May 08 2021 at 04:14 UTC