# Theory UpDown_Scheme

theory UpDown_Scheme
imports Grid
```section ‹ UpDown Scheme ›

theory UpDown_Scheme
imports Grid
begin

fun down' :: "nat ⇒ nat ⇒ grid_point ⇒ real ⇒ real ⇒ vector ⇒ vector"
where
"down' d 0       p f⇩l f⇩r α = α"
| "down' d (Suc l) p f⇩l f⇩r α = (let
f⇩m = (f⇩l + f⇩r) / 2 + (α p);
α = α(p := ((f⇩l + f⇩r) / 4 + (1 / 3) * (α p)) / 2 ^ (lv p d));
α = down' d l (child p left d) f⇩l f⇩m α;
α = down' d l (child p right d) f⇩m f⇩r α
in α)"

definition down :: "nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector" where
"down = lift (λ d l p. down' d l p 0 0)"

fun up' :: "nat ⇒ nat ⇒ grid_point ⇒ vector ⇒ (real * real) * vector" where
"up' d       0 p α = ((0, 0), α)"
| "up' d (Suc l) p α = (let
((f⇩l, f⇩m⇩l), α) = up' d l (child p left d) α;
((f⇩m⇩r, f⇩r), α) = up' d l (child p right d) α;
result = (f⇩m⇩l + f⇩m⇩r + (α p) / 2 ^ (lv p d) / 2) / 2
in ((f⇩l + result, f⇩r + result), α(p := f⇩m⇩l + f⇩m⇩r)))"

definition up :: "nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector" where
"up = lift (λ d lm p α. snd (up' d lm p α))"

fun updown' :: "nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector" where
"updown' dm lm 0 α = α"
| "updown' dm lm (Suc d) α =
(sum_vector (updown' dm lm d (up dm lm d α)) (down dm lm d (updown' dm lm d α)))"

definition updown :: "nat ⇒ nat ⇒ vector ⇒ vector" where
"updown dm lm α = updown' dm lm dm α"

end
```