namespace http://mathhub.info/MitM/core/calculus ❚

import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚

theory SimpleDerivatives : base:?Logic =
   include ?RealMetricSpace ❙
   include ☞base:?NaturalDeduction ❙
   include ?FunctionLimit ❙
   
   axiom_neqImplNotZero : {a : ℝ, b : ℝ} ⊦ neq ℝ a b ⟶ ⊦ neq ℝ (b - a) 0 ❘ # idnz 3 ❙
   
   differenceQuotient : {P : ℝ ⟶ bool, f: pred P ⟶ ℝ, a: pred P}{x : pred P, p:⊦ neq ℝ a x}ℝ ❘
   		= [P,f,a : pred P] ([x : pred P,p] ☞arith:?RealArithmetics?div ((f x) - (f a)) (x - a) (idnz p)) ❙
   
   prop_differentiableAt : {P : ℝ ⟶ bool}(pred P ⟶ ℝ) ⟶ pred P ⟶ prop ❘
   		= [P,f,a] prop_hasLimit_c (mpred P) ℝm ([x: pred P] neq ℝ a x) ([x,p] differenceQuotient P f a x p) a ❙
   	
   prop_differentiable : {P : ℝ ⟶ bool}(pred P ⟶ ℝ) ⟶ prop ❘ # diff 2 ❘
   		= [P,f] ∀ [x : pred P] prop_differentiableAt P f x ❙
   		
   /T derivative: P as predicate of where derivative is defined, f as a function on P of value ℝ, p as the proof that f is differentiable on P❙		
   derivative : {P : ℝ ⟶ bool,f : pred P ⟶ ℝ, p : ⊦ diff f} pred P ⟶ ℝ ❘
   		= [P,f,p][a] limit_c (mpred P) ℝm ([x: pred P] neq ℝ a x) ([x,q] differenceQuotient P f a x q) a (forall_elim (pred P) ([x : pred P] prop_differentiableAt P f x) p a) ❘ # 2 ' %I3 ❙
   		// defined as the limit of the diff_quotient on p, giving a proof that it is differentiable on P ❙
   	
   	f : pred ([x] true) ⟶ ℝ ❙
   	

 ❚