# Theory Down

theory Down
imports Triangular_Function UpDown_Scheme
```section ‹ Down part ›

theory Down
imports Triangular_Function UpDown_Scheme
begin

lemma sparsegrid'_parents:
assumes b: "b ∈ sparsegrid' dm" and p': "p' ∈ parents d b p"
shows "p' ∈ sparsegrid' dm"
using assms parents_def sparsegrid'I by auto

lemma down'_β: "⟦ d < length b ; l + level b = lm ; b ∈ sparsegrid' dm ; p ∈ sparsegrid' dm ⟧ ⟹
down' d l b fl fr α p = (if p ∈ lgrid b {d} lm
then
(fl + (fr - fl) / 2 * (real_of_int (ix p d) / 2^(lv p d - lv b d) - real_of_int (ix b d) + 1)) / 2 ^ (lv p d + 1) +
(∑ p' ∈ parents d b p. (α p') * l2_φ (p ! d) (p' ! d))
else α p)"
proof (induct l arbitrary: b α fl fr p)
case (Suc l)

let ?l = "child b left d" and ?r = "child b right d"
let ?result = "((fl + fr) / 4 + (1 / 3) * (α b)) / 2 ^ (lv b d)"
let ?fm = "(fl + fr) / 2 + (α b)"
let ?down_l = "down' d l (child b left d) fl ?fm (α(b := ?result))"

have "length b = dm" using ‹b ∈ sparsegrid' dm›
unfolding sparsegrid'_def start_def by auto
hence "d < dm" using ‹d < length b› by auto

have "!!dir. d < length (child b dir d)" using ‹d < length b› by auto
have "!!dir. l + level (child b dir d) = lm"
using ‹d < length b› and ‹Suc l + level b = lm› and child_level by auto
have "!!dir. (child b dir d) ∈ sparsegrid' dm"
using ‹b ∈ sparsegrid' dm› and ‹d < dm› and sparsegrid'_def by auto
note hyps = Suc.hyps[OF ‹!! dir. d < length (child b dir d)›
‹!!dir. l + level (child b dir d) = lm›
‹!!dir. (child b dir d) ∈ sparsegrid' dm›]

show ?case
proof (cases "p ∈ lgrid b {d} lm")
case False
moreover hence "p ≠ b" and "p ∉ lgrid ?l {d} lm"
and "p ∉ lgrid ?r {d} lm" unfolding lgrid_def
unfolding grid_partition[where p=b] using ‹Suc l + level b = lm› by auto
ultimately show ?thesis
unfolding down'.simps Let_def fun_upd_def hyps[OF ‹p ∈ sparsegrid' dm›]
by auto
next
case True hence "level p < lm" and "p ∈ grid b {d}" unfolding lgrid_def by auto
let ?lb = "lv b d"   and ?ib = "real_of_int (ix b d)"
let ?lp   = "lv p d"  and ?ip   = "real_of_int (ix p d)"
show ?thesis
proof (cases "∃ dir. p ∈ grid (child b dir d){d}")
case True
obtain dir where p_grid: "p ∈ grid (child b dir d) {d}" using True by auto
hence "p ∈ lgrid (child b dir d) {d} lm" using ‹level p < lm› unfolding lgrid_def by auto
have "lv b d < lv p d" using child_lv[OF ‹d < length b›] and grid_single_level[OF p_grid ‹d < length (child b dir d)›] by auto

let ?ch = "child b dir d"
let ?ich = "child b (inv dir) d"

show ?thesis
proof (cases dir)
case right
hence "p ∈ lgrid ?r {d} lm" and "p ∈ grid ?r {d}"
using ‹p ∈ grid ?ch {d}› and ‹level p < lm› unfolding lgrid_def by auto

{ fix p' fix fl fr x assume p': "p' ∈ parents d (child b right d) p"
hence "p' ∈ grid (child b right d) {d}" unfolding parents_def by simp
hence "p' ∉ lgrid (child b left d) {d} lm" and "p' ≠ b"
unfolding lgrid_def
using grid_disjunct[OF ‹d < length b›] grid_not_child by auto

from hyps[OF sparsegrid'_parents[OF ‹child b right d ∈ sparsegrid' dm›
p']] this
have "down' d l (child b left d) fl fr (α(b := x)) p' = α p'" by auto }
thus  ?thesis
unfolding down'.simps Let_def hyps[OF ‹p ∈ sparsegrid' dm›]
parent_sum[OF ‹p ∈ grid ?r {d}› ‹d < length b›]
l2_child[OF ‹d < length b› ‹p ∈ grid ?r {d}›]
using child_ix child_lv ‹d < length b› level_shift[OF ‹lv b d < lv p d›]
sgn.simps ‹p ∈ lgrid b {d} lm› ‹p ∈ lgrid ?r {d} lm›
by (auto simp add: algebra_simps diff_divide_distrib add_divide_distrib)
next
case left
hence "p ∈ lgrid ?l {d} lm" and "p ∈ grid ?l {d}"
using ‹p ∈ grid ?ch {d}› and ‹level p < lm› unfolding lgrid_def by auto
hence "¬ p ∈ lgrid ?r {d} lm"
using grid_disjunct[OF ‹d < length b›] unfolding lgrid_def by auto
{ fix p' assume p': "p' ∈ parents d (child b left d) p"
hence "p' ∈ grid (child b left d) {d}" unfolding parents_def by simp
hence "p' ≠ b" using grid_not_child[OF ‹d < length b›] by auto }
thus ?thesis
unfolding down'.simps Let_def hyps[OF ‹p ∈ sparsegrid' dm›]
parent_sum[OF ‹p ∈ grid ?l {d}› ‹d < length b›]
l2_child[OF ‹d < length b› ‹p ∈ grid ?l {d}›] sgn.simps
if_P[OF ‹p ∈ lgrid b {d} lm›] if_P[OF ‹p ∈ lgrid ?l {d} lm›]
if_not_P[OF ‹p ∉ lgrid ?r {d} lm›]
using child_ix child_lv ‹d < length b› level_shift[OF ‹lv b d < lv p d›]
by (auto simp add: algebra_simps diff_divide_distrib add_divide_distrib)
qed
next
case False hence not_child: "!! dir. ¬ p ∈ grid (child b dir d) {d}" by auto
hence "p = b" using grid_onedim_split[where ds="{}" and d=d and b=b] ‹p ∈ grid b {d}› unfolding grid_empty_ds[where b=b] by auto
from not_child have lnot_child: "!! dir. ¬ p ∈ lgrid (child b dir d) {d} lm" unfolding lgrid_def by auto
have result: "((fl + fr) / 4 + 1 / 3 * α b) / 2 ^ lv b d = (fl + (fr - fl) / 2) / 2 ^ (lv b d + 1) + α b * l2_φ (b ! d) (b ! d)"
by (auto simp: l2_same diff_divide_distrib add_divide_distrib times_divide_eq_left[symmetric] algebra_simps)
show ?thesis
unfolding down'.simps Let_def fun_upd_def hyps[OF ‹p ∈ sparsegrid' dm›] if_P[OF ‹p ∈ lgrid b {d} lm›] if_not_P[OF lnot_child] if_P[OF ‹p = b›]
unfolding ‹p = b› parents_single unfolding result by auto
qed
qed
next
case 0
have "p ∉ lgrid b {d} lm"
proof (rule ccontr)
assume "¬ p ∉ lgrid b {d} lm"
hence "p ∈ grid b {d}" and "level p < lm" unfolding lgrid_def by auto
moreover from grid_level[OF ‹p ∈ grid b {d}›] and ‹0 + level b = lm› have "lm ≤ level p" by auto
ultimately show False by auto
qed
thus ?case unfolding down'.simps by auto
qed

lemma down: assumes "d < dm" and p: "p ∈ sparsegrid dm lm"
shows "(down dm lm d α) p = (∑ p' ∈ parents d (base {d} p) p. (α p') * l2_φ (p ! d) (p' ! d))"
proof -
let "?F d l p" = "down' d l p 0 0"
let "?S x p p'" = "if p' ∈ parents d (base {d} p) p then x * l2_φ (p ! d) (p' ! d) else 0"

{ fix p α assume "p ∈ sparsegrid dm lm"
from le_less_trans[OF grid_level sparsegridE(2)[OF this]]
have "parents d (base {d} p) p ⊆  lgrid (base {d} p) {d} lm"
unfolding lgrid_def parents_def by auto
hence "(∑p'∈lgrid (base {d} p) {d} lm. ?S (α p') p p') =
(∑p'∈parents d (base {d} p) p. α p' * l2_φ (p ! d) (p' ! d))"
using lgrid_finite by (intro sum.mono_neutral_cong_right) auto
} note sum_eq = this

{ fix l p b α
assume b: "b ∈ lgrid (start dm) ({0..<dm} - {d}) lm" and "l + level b = lm"
and "p ∈ sparsegrid dm lm"
hence b_spg: "b ∈ sparsegrid' dm" and p_spg: "p ∈ sparsegrid' dm" and
"d < length b" and "level p < lm"
using sparsegrid'_start sparsegrid_subset ‹d < dm› by auto
have "?F d l b α p = (if b = base {d} p then ∑p'∈lgrid b {d} lm. ?S (α p') p p' else α p)"
proof (cases "b = base {d} p")
case True
have "p ∈ lgrid (base {d} p) {d} lm"
using baseE(2)[OF p_spg] and ‹level p < lm›
unfolding lgrid_def by auto
thus ?thesis unfolding if_P[OF True]
unfolding True sum_eq[OF ‹p ∈ sparsegrid dm lm›]
unfolding down'_β[OF ‹d < length b› ‹l + level b = lm› b_spg p_spg,
unfolded True] by auto
next
case False
have "p ∉ lgrid b {d} lm"
proof (rule ccontr)
assume "¬ ?thesis" hence "p ∈ grid b {d}" by auto
from b this have "b = base {d} p" using baseI by auto
thus False using False by simp
qed
thus ?thesis
unfolding if_not_P[OF False]
unfolding down'_β[OF ‹d < length b› ‹l + level b = lm› b_spg p_spg]
by auto
qed }
from lift[OF ‹d < dm› ‹p ∈ sparsegrid dm lm›, where F = ?F and S = ?S, OF this]
show ?thesis
unfolding down_def
unfolding sum_eq[OF p] by simp
qed

end
```