sum of two negligible function is also a negligible function

Stream: new members

[Mukesh Tiwari]

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]

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]

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]

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]

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

[Patrick Massot]

Sure, https://leanprover-community.github.io/mathlib_docs/algebra/pi_instances.html

[Kyle Miller]

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 pi.add_apply,
  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]

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]

@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]

@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]

Thank you very much everyone for answering my questions patiently.

[Kyle Miller]

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