euler.lean

import analysis.normed_space.basic
import topology.instances.ennreal
import analysis.normed_space.basic
import topology.instances.ennreal
import algebra.archimedean algebra.geom_sum
import data.nat.choose data.complex.basic
import tactic.linarith
import analysis.calculus.deriv
import data.complex.exponential

open finset
open cau_seq
namespace complex
noncomputable theory


lemma is_cau_abs_cos (z : ℂ) : is_cau_seq _root_.abs
  (λ n, (range n).sum (λ m, abs (
      ((-1) ^ m) * z ^ (2 * m ) / nat.fact (2 * m )))) :=
begin
sorry,
end

lemma is_cau_abs_sin (z : ℂ) : is_cau_seq _root_.abs
  (λ n, (range n).sum (λ m, abs (
      ((-1) ^ m) * z ^ (2 * m + 1) / nat.fact (2 * m + 1)))) :=
begin
sorry,
/-
let ⟨n, hn⟩ := exists_nat_gt (abs z) in
have hn0 : (0 : ℝ) < n, from lt_of_le_of_lt (abs_nonneg _) hn,
series_ratio_test n (complex.abs z / n) 
(div_nonneg_of_nonneg_of_pos (complex.abs_nonneg _) hn0)
  (by rwa [div_lt_iff hn0, one_mul])
  (λ m hm,
    by rw [abs_abs, abs_abs, nat.fact_succ, pow_succ,
      mul_comm m.succ, nat.cast_mul, ← div_div_eq_div_mul, mul_div_assoc,
      mul_div_right_comm, abs_mul, abs_div, abs_cast_nat];
    exact mul_le_mul_of_nonneg_right
      (div_le_div_of_le_left (abs_nonneg _) hn0
        (nat.cast_le.2 (le_trans hm (nat.le_succ _)))) (abs_nonneg _))
-/
end

lemma is_cau_sin (z : ℂ) :
 is_cau_seq abs (λ n, (range n).sum (λ m, 
 ((-1) ^ m) * z ^ (2 * m + 1) / nat.fact (2 * m + 1))) 
:=
begin
    exact is_cau_series_of_abv_cau (is_cau_abs_sin z),
end

lemma is_cau_cos (z : ℂ) :
 is_cau_seq abs (λ n, (range n).sum (λ m, 
 ((-1) ^ m) * z ^ (2 * m ) / nat.fact (2 * m))) 
:=
begin
    exact is_cau_series_of_abv_cau (is_cau_abs_cos z),
end

def sin' (z : ℂ) : cau_seq ℂ complex.abs :=
 ⟨λ n, (range n).sum 
 (λ m, ((-1) ^ m) * z ^ (2 * m + 1) / nat.fact (2 * m + 1)), 
 is_cau_sin z⟩
def sin1 (z : ℂ) : ℂ := lim (sin' z)

def cos' (z : ℂ) : cau_seq ℂ complex.abs :=
 ⟨λ n, (range n).sum 
 (λ m, (-1) ^ m * z ^ (2 * m) / nat.fact (2 * m)), 
 is_cau_cos z⟩
def cos1 (z : ℂ) : ℂ := lim (cos' z)

theorem euler : ∀ x, exp (x * I) = cos1 x + sin1 x * I 
:= 
begin
    intros,
    
    have partials: ∀ n:ℕ , (exp' (x*I)).1 (2*n+1) =
     (cos' x).1 (n+1) + ((sin' x).1 n) * I,
    {
        intros,
        rw exp',
        simp,
        rw cos',
        simp,
        rw sin',
        simp,

        induction n with n0 hn,
        { -- case n0=0
            simp,
--            simp,
        },
        { -- induction on n0

            rw sum_range_succ _ _, -- takes out last term in cos

            have lastSin : 
            sum (range (nat.succ n0)) (λ (x_1 : ℕ), (-1) ^ x_1 * x ^ (1 + 2 * x_1) / ↑(nat.fact (1 + 2 * x_1))) 
            =
            (-1) ^ n0 * x ^ (1 + 2 * n0) / ↑(nat.fact (1 + 2 * n0)) 
            +
            sum (range (n0)) (λ (x_1 : ℕ), (-1) ^ x_1 * x ^ (1 + 2 * x_1) / ↑(nat.fact (1 + 2 * x_1))) 
            ,
            {
              rw sum_range_succ _ _,
            },

            have sinFactorial : 
            sum (range (nat.succ n0)) (λ (x_1 : ℕ), (-1) ^ x_1 * x ^ (2 * x_1 + 1) / ((2 * ↑x_1 + 1) * ↑(nat.fact (2 * x_1)))) 
            =
            sum (range (nat.succ n0)) (λ (x_1 : ℕ), (-1) ^ x_1 * x ^ (1 + 2 * x_1) / ↑(nat.fact (1 + 2 * x_1))),
            {
              sorry,
              --lean should fuckin know this!
            },
            rw sinFactorial,
            rw lastSin,
            
            have twoFromExp:
            sum (range (nat.succ (2 * nat.succ n0))) (λ (x_1 : ℕ), 
            (x * I) ^ x_1 / ↑(nat.fact x_1))
            =
            (x * I) ^ ( 2 * nat.succ n0) / ↑(nat.fact ( 2 * nat.succ n0))+
            sum (range ( 2 * nat.succ n0)) (λ (x_1 : ℕ), 
            (x * I) ^ x_1 / ↑(nat.fact x_1))
            ,
            {
              rw sum_range_succ _ ( 2 * nat.succ n0),
            },
            have twoFromExpv1 :
            (x * I) ^ ( 2 * nat.succ n0) / ↑(nat.fact ( 2 * nat.succ n0))+sum (range ( 2 * nat.succ n0)) (λ (x_1 : ℕ), (x * I) ^ x_1 / ↑(nat.fact x_1)) 
            =
            sum (range (nat.succ (2 * nat.succ n0))) (λ (x_1 : ℕ), 
            (x * I) ^ x_1 / ↑(nat.fact x_1)),
             {
               by exact eq.symm twoFromExp,
             },

            have twoNP1 : 1+ (2 * nat.succ n0) =nat.succ (2 * nat.succ n0)
            ,
            {
              exact add_comm 1 (2 * nat.succ n0),
            },

            have twoNP1v1 : nat.succ ( 2 * nat.succ n0) = 1 + (2 * nat.succ n0),
            {
              by exact eq.symm twoNP1,
            },

            --rw twoNP1v1,
            rw twoFromExpv1,

            have oneFromExp:
            sum (range (2 * nat.succ n0)) (λ (x_1 : ℕ), (x * I) ^ x_1 / ↑(nat.fact x_1))
            =
            (x * I) ^ (1+2 * n0) / ↑(nat.fact (1+2 * n0))
            +
            sum (range (1+ 2 * n0)) (λ (x_1 : ℕ), (x * I) ^ x_1 / ↑(nat.fact x_1))
            ,
            {
              have stupid : 2 * nat.succ n0 = nat.succ(1+2*n0),
              {
                have RRS : nat.succ(1+2*n0) = 1+(1+2*n0) ,
                {
                  sorry,
                },
                rw RRS,

                have realSt : 1+(1+2*n0) = 1+1+2*n0,
                {
                  simp,
                },
                rw realSt,
                exact nat.add_comm (nat.mul 2 n0) 2,
              },
              rw stupid,
              rw sum_range_succ _ (1 + 2 * n0),
            },
            --rw oneFromExp,
            --rw hn,
            --simp,

            --  need (x*I)^(2 n0 )= x^(2n0) (-1)^n0 etc, commutativity 

            sorry,
            --ring,
        },
    },

    have partialExp : lim (exp' (x * I)) = exp (x*I),
    {
      sorry,
    },

    have pulled_outta_my_derriere : ∀ (n : ℕ), (cos' x).val (n + 1) = cos1 x,
    {
      sorry,
    },
    
    rw exp,
    rw partialExp,

    -- Now: need to take limits on both sides, they're same, 
    -- but need to convince Lean that limit of exp' (2n+1) is same as
    -- limit of exp' (n) which is what exp is defined to be
end

end complex