fact: Fixpoint interp_domain (l : seq R) (d : domain) : Prop := match d with | Never => False | Always => True | Partial p e => p (interp l e) | Derivable n k f le => ex_derive_Rn k f n (nth 0 (map (interp l) le)) | Derivable2 m n k f le => let le' := map (interp l) le in locally_2d (fun u v => ex_derive_Rn k f m (fun i => if ssrnat.eqn i m then u else if ssrnat.eqn i n then v else nth 0 le' i)) (nth 0 le' m) (nth 0 le' n) /\ continuity_2d_pt (fun u v => Derive_Rn k f m (fun i => if ssrnat.eqn i m then u else if ssrnat.eqn i n then v else nth 0 le' i)) (nth 0 le' m) (nth 0 le' n) | Continuous n f => continuity_pt (fun x => interp (set_nth R0 l n x) f) (nth R0 l n) | Continuous2 m n f => continuity_2d_pt (fun x y => interp (set_nth R0 (set_nth R0 l n y) m x) f) (nth R0 l m) (nth R0 l n) | Integrable f e1 e2 => ex_RInt (fun x => interp (x :: l) f) (interp l e1) (interp l e2) | ParamIntegrable n f e1 e2 => locally (nth R0 l n) (fun y => ex_RInt (fun t => interp (t :: set_nth R0 l n y) f) (interp l e1) (interp l e2)) | LocallyParamIntegrable n f e => let a := interp l e in exists eps : posreal, locally (nth R0 l n) (fun y => ex_RInt (fun t => interp (t :: set_nth R0 l n y) f) (a - eps) (a + eps)) | And ld => foldr (fun d acc => interp_domain l d /\ acc) True ld | Forall e1 e2 s => let a1 := interp l e1 in let a2 := interp l e2 in forall t, Rmin a1 a2 <= t <= Rmax a1 a2 -> interp_domain (t :: l) s | Forone e s => interp_domain (interp l e :: l) s | Locally n s => locally (nth R0 l n) (fun x => interp_domain (set_nth R0 l n x) s) | Locally2 m n s => locally_2d (fun x y => interp_domain (set_nth R0 (set_nth R0 l n y) m x) s) (nth R0 l m) (nth R0 l n) | ForallWide n e1 e2 s => let a1 := interp l e1 in let a2 := interp l e2 in exists d : posreal, forall t u, Rmin a1 a2 - d < t < Rmax a1 a2 + d -> Rabs (u - nth R0 l n) < d -> interp_domain (t :: set_nth R0 l n u) s end.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct