Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 12 2020 at 09:49):

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

view this post on Zulip 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 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

view this post on Zulip 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₂.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mukesh Tiwari (Jul 12 2020 at 11:06):

Thank you very much everyone for answering my questions patiently.

view this post on Zulip 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