-- begin header import limits namespace M1P1 -- end header /- Section The sandwich theorem -/ /- Sub-section Introduction -/ /- The sandwich theorem, or squeeze theorem, for real sequences is the statement that if \$(a_n)\$, \$(b_n)\$, and \$(c_n)\$ are three real-valued sequences satisfying \$a_n≤ b_n≤ c_n\$ for all \$n\$, and if furthermore \$a_n→ℓ\$ and \$c_n→ℓ\$, then \$b_n→ℓ\$. The idea of the proof is straightforward -- if we want to ensure that \$|b_n-ℓ|<ε\$ then it suffices to show that \$|a_n-ℓ|<ε\$ and \$|c_n-ℓ|<ε\$, and we can choose \$N\$ large enough such that this is true for all \$n≥ N\$. -/ /- Lemma If \$(a_n)\$, \$(b_n)\$, and \$(c_n)\$ are three real-valued sequences satisfying \$a_n ≤ b_n ≤ c_n\$ for all \$n\$, and if furthermore \$a_n→ℓ\$ and \$c_n→ℓ\$, then \$b_n→ℓ\$. -/ theorem sandwich (a b c : ℕ → ℝ) (l : ℝ) (ha : is_limit a l) (hc : is_limit c l) (hab : ∀ n, a n ≤ b n) (hbc : ∀ n, b n ≤ c n) : is_limit b l := begin -- We need to show that for all \$ε>0\$ there exists \$N\$ such that \$n≥N\$ implies \$|b_n-ℓ|<ε\$. So choose ε > 0. intros ε Hε, -- We now need an \$N\$. As usual it is the max of two other N's, one coming from \$(a_n)\$ and one from \$(c_n)\$. Choose \$N_a\$ and \$N_c\$ such that \$|a_n - l| < ε\$ for \$n ≥ N_a\$ and \$|c_n - l| < ε\$ for \$n ≥ N_c\$. cases ha ε Hε with Na Ha, cases hc ε Hε with Nc Hc, -- Now let \$N\$ be the max of \$N_a\$ and \$N_c\$; we claim that this works. let N := max Na Nc, use N, -- Note that \$N ≥ N_a\$ and \$N ≥ N_c\$, have HNa : Na ≤ N := by obvious_ineq, have HNc : Nc ≤ N := by obvious_ineq, -- so for all \$n ≥ N\$, intros n Hn, -- we have \$a_n ≤ b_n ≤ c_n\$, and \$|a_n - l|, |b_n - l|\$ are both less than \$ε\$. have h1 : a n ≤ b n := hab n, have h2 : b n ≤ c n := hbc n, have h3 : |a n - l| < ε := Ha n (le_trans HNa Hn), have h4 : |c n - l| < ε := Hc n (le_trans HNc Hn), -- The result now follows easily from these inequalities (as \$l-ε < a_n ≤ b_n ≤ c_n < l+ε\$ ). rw abs_sub_lt_iff at h3 h4 ⊢, cases h3, cases h4, split;linarith end /- Note that Lean finds the last line of the proof automatically -- we do not need to explicitly tell it the inequality argument. -/ end M1P1