Inductive poof that polynomials are continuous in Lean 3

polynomials_are_continuous.lean

-- Inductive poof that polynomials are continuous in Lean 3
-- author: Michael Nestor (mdnest01@gmail.com)

import data.nat.basic
import data.real.basic
import analysis.normed.group.basic -- for triangle inequality

def is_limit (a: ℕ → ℝ) (L: ℝ) :=
  ∀ ε: ℝ, ∃ N: ℕ, ∀ n: ℕ, (0 < ε) ∧ (N ≤ n) → |a(n) - L| < ε

-- a sequence is convergent if it has a limit
def is_convergent (a: ℕ → ℝ) :=
  ∃ L: ℝ, is_limit a L

def is_bound (a: ℕ → ℝ) (B: ℝ) :=
  ∀ n: ℕ, |a(n)| ≤ B

def is_bounded (a: ℕ → ℝ) :=
  ∃ B: ℝ, is_bound a B

theorem convergent_implies_bounded (a: ℕ → ℝ)
  (h: is_convergent a) : is_bounded a :=
begin
  sorry,
end

-- example: constant sequence is convergent
example (L: ℝ) : is_limit (λ n: ℕ, L) L :=
begin
  intros ε, -- let epsilon be an artbirary real number
  use 0, -- take N = 0
  intros n h, -- assume 0 < ε and N ≤ n
  simp, -- simplify |(λ (n : ℕ), L) n - L| to 0
  apply h.left -- apply 0 < ε
end

-- the limit of the sum is the sum of the limits
theorem limit_sum (a1 a2: ℕ → ℝ) (L1 L2: ℝ) (h1: is_limit a1 L1) (h2: is_limit a2 L2):
  is_limit (a1 + a2) (L1 + L2) :=
begin
  intros ε, -- let ε be arbitrary
  cases h1 (ε / 2) with N1 h3, -- let N1 and N2 match the definition of h1 and h2 with ε/2
  cases h2 (ε / 2) with N2 h4,
  use max N1 N2, -- let N = max(N1, N2)
  intros n h5, -- assume n ≥ N; call this hypothesis h5
  cases h5 with h6 h7, -- call the hypotheses h6 and h7
  have h8: 0 < ε / 2, linarith, -- from 0 < ε conclude 0 < ε/2
  have h9: N1 ≤ n, { -- show N1 ≤ n
    have h9a: N1 <= max N1 N2, {
      exact le_max_left N1 N2,
    },
    linarith,
  },
  have h10: N2 ≤ n, { -- show N1 ≤ n by similar method
    have h10a: N2 <= max N1 N2, {
      exact le_max_right N1 N2,
    },
    linarith,
  },
  have h11: |a1(n) - L1| < ε / 2, {
    apply h3,
    split,
    exact h8,
    exact h9,
  },
  have h12: |a2(n) - L2| < ε / 2, {
    apply h4,
    split,
    exact h8,
    exact h10,
  },
  have h13: |(a1 + a2) n - (L1 + L2)| = |(a1 n - L1) + (a2 n - L2)|, {
    simp,
    ring_nf, -- distributive property
  },
  rw h13,
  have h14: |(a1 n - L1) + (a2 n - L2)| ≤ |a1 n - L1| + |a2 n - L2|, {
    apply norm_add_le (a1 n - L1) (a2 n - L2), -- triangle inequality
  },
  have h15: |(a1 n - L1) + (a2 n - L2)| < ε, {
    linarith,
  },
  exact h15,
end

-- corollary: the sum of two convergent sequences is convergent
theorem sum_is_convergent (a1 a2: ℕ → ℝ)
  (h1: is_convergent a1) (h2: is_convergent a2):
  is_convergent (a1 + a2) :=
begin
  cases h1 with L1 h3,
  cases h2 with L2 h4,
  use L1 + L2,
  apply limit_sum,
  exact h3,
  exact h4,
end

theorem limit_prod (a1 a2: ℕ → ℝ) (L1 L2: ℝ) (h1: is_limit a1 L1) (h2: is_limit a2 L2):
  is_limit (a1 * a2) (L1*L2) :=
begin
  sorry, -- a little harder. requires boundedness: https://math.stackexchange.com/questions/2362068
end

def is_continuous (f: ℝ → ℝ) :=
  ∀a: ℕ → ℝ, ∀L: ℝ, is_limit a L → is_limit (f ∘ a) (f L)

lemma constant_fn_is_continuous (c: ℝ): is_continuous (λ x: ℝ, c) :=
begin
  intros a L,    -- let a be a sequence and L a real number
  intro h1,      -- assume a → L, call this hypothesis h1
  intros ε,      -- let ε be an arbitrary real number
  use 0,         -- choose N = 0
  intros n h2,   -- assume 0 < ε and N ≤ n
  simp,          -- simplify |((λ x : ℝ, c) ∘ a) n - (λ x : ℝ, c) L| = 0
  apply h2.left, -- apply 0 < ε
end

lemma identity_fn_is_continuous: is_continuous (λ x: ℝ, x) :=
begin
  intros a L,
  intro h1,
  intros ε,
  use 0,
  intros n h2,
  simp,
  -- this is true by definition of h1
  sorry,
end

theorem continuous_sum_is_continuous (f g: ℝ → ℝ)
  (hf: is_continuous f) (hg: is_continuous g):
  is_continuous (f + g) :=
begin
  intros a L, -- let a be a sequence and L is a real number
  intro h, -- assume a -> L
  simp, -- simplify (f*g) (a) to f(a) * g(a)
  sorry,
end

-- the proof that the product of two continuous functions is continuous is very similar!
theorem continuous_prod_is_continuous (f g: ℝ → ℝ)
  (hf: is_continuous f) (hg: is_continuous g):
  is_continuous (f * g) :=
begin
  intros a L,
  intro h,
  simp,
  sorry,
end

inductive is_polynomial: (ℝ → ℝ) → Prop
| const (c : ℝ) : is_polynomial (λ x, c)
| x_mul_add_c (f: ℝ → ℝ) (c : ℝ) : is_polynomial f → is_polynomial(λ x, x * f(x) + c)

theorem polynomials_are_continuous (f: ℝ → ℝ) (h: is_polynomial f) :
  is_continuous f :=
begin
  induction h,
  case const {
    exact constant_fn_is_continuous h,
  },
  case x_mul_add_c {
    let id := λ x: ℝ, x,
    let f1 := λ x: ℝ, x * h_f(x),
    let f2 := λ x: ℝ, h_c,
    have h1: is_continuous f1, {
      have h1a : is_continuous id, {
        exact identity_fn_is_continuous,
      },
      exact continuous_prod_is_continuous id h_f h1a h_ih,
    },
    have h2: is_continuous f2, {
      exact constant_fn_is_continuous h_c,
    },
    exact continuous_sum_is_continuous f1 f2 h1 h2,
  },
end