# Theory Up_Down

```section ‹ UpDown  ›

(* Definition of sparse grids, hierarchical bases and the up-down algorithm.
*
* Based on "updown_L2-Skalarprodukt.mws" from Dirk Pflüger <pflueged@in.tum.de>
*
* Author: Johannes Hölzl <hoelzl@in.tum.de>
*)
theory Up_Down
imports Up Down
begin

lemma updown': "⟦ d ≤ dm; p ∈ sparsegrid dm lm ⟧
⟹ (updown' dm lm d α) p = (∑ p' ∈ lgrid (base {0 ..< d} p) {0 ..< d} lm. α p' * (∏ d' ∈ {0 ..< d}. l2_φ (p' ! d') (p ! d')))"
(is "⟦ _ ; _ ⟧ ⟹ _ = (∑ p' ∈ ?subgrid d p. α p' * ?prod d p' p)")
proof (induct d arbitrary: α p)
case 0 hence "?subgrid 0 p = {p}" using base_empty unfolding lgrid_def and sparsegrid_def sparsegrid'_def by auto
thus ?case unfolding updown'.simps by auto
next
case (Suc d)
let "?leafs p" = "(lgrid p {d} lm) - {p}"
let "?parents" = "parents d (base {d} p) p"
let ?b = "base {0..<d} p"
have "d < dm" using ‹Suc d ≤ dm› by auto

have p_spg: "p ∈ grid (start dm) {0..<dm}" and p_spg': "p ∈ sparsegrid' dm" and "level p < lm" using ‹p ∈ sparsegrid dm lm›
unfolding sparsegrid_def and sparsegrid'_def and lgrid_def by auto
have p'_in_spg: "!! p'. p' ∈ ?subgrid d p ⟹ p' ∈ sparsegrid dm lm"
using base_grid[OF p_spg'] unfolding sparsegrid'_def sparsegrid_def lgrid_def by auto

from baseE[OF p_spg', where ds="{0..<d}"]
have "?b ∈ grid (start dm) {d..<dm}" and p_bgrid: "p ∈ grid ?b {0..<d}" by auto
hence "d < length ?b" using ‹Suc d ≤ dm› by auto
have "p ! d = ?b ! d" using base_out[OF _ _ p_spg'] ‹Suc d ≤ dm› by auto

have "length p = dm" using ‹p ∈ sparsegrid dm lm› unfolding sparsegrid_def lgrid_def by auto
hence "d < length p" using ‹d < dm› by auto

have "updown' dm lm d (up dm lm d α) p =
(∑ p' ∈ ?subgrid d p. (up dm lm d α) p' * (?prod d p' p))"
using Suc by auto
also have "… = (∑ p' ∈ ?subgrid d p. (∑ p'' ∈ ?leafs p'. α p'' * ?prod (Suc d) p'' p))"
proof (intro sum.cong refl)
fix p' assume "p' ∈ ?subgrid d p"
hence "d < length p'" unfolding lgrid_def using base_length[OF p_spg'] ‹Suc d ≤ dm› by auto

have "up dm lm d α p' * ?prod d p' p =
(∑ p'' ∈ ?leafs p'. α p'' * l2_φ (p'' ! d) (p' ! d)) * ?prod d p' p"
using ‹p' ∈ ?subgrid d p› up ‹Suc d ≤ dm› p'_in_spg by auto
also have "… = (∑ p'' ∈ ?leafs p'. α p'' * l2_φ (p'' ! d) (p' ! d) * ?prod d p' p)"
using sum_distrib_right by auto
also have "… = (∑ p'' ∈ ?leafs p'. α p'' * ?prod (Suc d) p'' p)"
proof (intro sum.cong refl)
fix p'' assume "p'' ∈ ?leafs p'"
have "?prod d p' p = ?prod d p'' p"
proof (intro prod.cong refl)
fix d' assume "d' ∈ {0..<d}"
hence d_lt_p: "d' < length p'" and d'_not_d: "d' ∉ {d}" using ‹d < length p'› by auto
hence "p' ! d' = p'' ! d'" using ‹p'' ∈ ?leafs p'› grid_invariant[OF d_lt_p d'_not_d] unfolding lgrid_def by auto
thus "l2_φ (p'!d') (p!d') = l2_φ (p''!d') (p!d')" by auto
qed
moreover have "p' ! d = p ! d"
using ‹p' ∈ ?subgrid d p› and grid_invariant[OF ‹d < length ?b›, where p=p' and ds="{0..<d}"] unfolding lgrid_def ‹p ! d = ?b ! d› by auto
ultimately have "l2_φ (p'' ! d) (p' ! d) * ?prod d p' p =
l2_φ (p'' ! d) (p ! d) * ?prod d p'' p" by auto
also have "… = ?prod (Suc d) p'' p"
proof -
have "insert d {0..<d} = {0..<Suc d}" by auto
moreover from prod.insert
have "prod (λ d'. l2_φ (p'' ! d') (p ! d')) (insert d {0..<d}) =
(λ d'. l2_φ (p'' ! d') (p ! d')) d * prod (λ d'. l2_φ (p'' ! d') (p ! d')) {0..<d}"
by auto
ultimately show ?thesis by auto
qed
finally show "α p'' * l2_φ (p'' ! d) (p' ! d) * ?prod d p' p = α p'' * ?prod (Suc d) p'' p" by auto
qed
finally show "(up dm lm d α) p' * (?prod d p' p) = (∑ p'' ∈ ?leafs p'. α p'' * ?prod (Suc d) p'' p)" by auto
qed
also have "… = (∑ (p', p'') ∈ Sigma (?subgrid d p) (λp'. (?leafs p')). (α p'') * (?prod (Suc d) p'' p))"
by (rule sum.Sigma, auto simp add: lgrid_finite)
also have "… = (∑ p''' ∈ (⋃ p' ∈ ?subgrid d p. (⋃ p'' ∈ ?leafs p'. { (p', p'') })).
(((λ p''. α p'' * ?prod (Suc d) p'' p) o snd) p''') )" unfolding Sigma_def by (rule sum.cong[OF refl], auto)
also have "… = (∑ p'' ∈ snd ` (⋃ p' ∈ ?subgrid d p. (⋃ p'' ∈ ?leafs p'. { (p', p'') })).
α p'' * (?prod (Suc d) p'' p))" unfolding lgrid_def
by (rule sum.reindex[symmetric],
rule subset_inj_on[OF grid_grid_inj_on[OF ivl_disj_int(15)[where l=0 and m="d" and u="d"], where b="?b"]])
auto
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. (⋃ p'' ∈ ?leafs p'. snd ` { (p', p'') })).
α p'' * (?prod (Suc d) p'' p))" by (auto simp only: image_UN)
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p'). α p'' * (?prod (Suc d) p'' p))" by auto
finally have up_part: "updown' dm lm d (up dm lm d α) p = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p'). α p'' * (?prod (Suc d) p'' p))" .

have "down dm lm d (updown' dm lm d α) p = (∑ p' ∈ ?parents. (updown' dm lm d α p') * l2_φ (p ! d) (p' ! d))"
using ‹Suc d ≤ dm› and down and ‹p ∈ sparsegrid dm lm› by auto
also have "… = (∑ p' ∈ ?parents. ∑ p'' ∈ ?subgrid d p'. α p'' * ?prod (Suc d) p'' p)"
proof (rule sum.cong[OF refl])
fix p' let ?b' = "base {d} p"
assume "p' ∈ ?parents"
hence p_lgrid: "p' ∈ lgrid ?b' {d} (level p + 1)" using parents_subset_lgrid by auto
hence "p' ∈ sparsegrid dm lm" and p'_spg': "p' ∈ sparsegrid' dm" using ‹level p < lm› base_grid[OF p_spg'] unfolding sparsegrid_def lgrid_def sparsegrid'_def by auto
hence "length p' = dm" unfolding sparsegrid_def lgrid_def by auto
hence "d < length p'" using ‹Suc d ≤ dm› by auto

from p_lgrid have p'_grid: "p' ∈ grid ?b' {d}" unfolding lgrid_def by auto

have "(updown' dm lm d α p') * l2_φ (p ! d) (p' !  d) = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod d p'' p') * l2_φ (p ! d) (p' ! d)"
using ‹p' ∈ sparsegrid dm lm› Suc by auto
also have "… = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod d p'' p' * l2_φ (p ! d) (p' ! d))"
using sum_distrib_right by auto
also have "… = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod (Suc d) p'' p)"
proof (rule sum.cong[OF refl])
fix p'' assume "p'' ∈ ?subgrid d p'"

have "?prod d p'' p' = ?prod d p'' p"
proof (rule prod.cong, rule refl)
fix d' assume "d' ∈ {0..<d}"
hence "d' < dm" and "d' ∉ {d}" using ‹Suc d ≤ dm› by auto
from grid_base_out[OF this p_spg' p'_grid]
show "l2_φ (p''!d') (p'!d') = l2_φ (p''!d') (p!d')" by auto
qed
moreover
have "l2_φ (p ! d) (p' ! d) = l2_φ (p'' ! d) (p ! d)"
proof -
have "d < dm" and "d ∉ {0..<d}" using ‹Suc d ≤ dm› base_length p'_spg' by auto
from grid_base_out[OF this p'_spg'] ‹p'' ∈ ?subgrid d p'›[unfolded lgrid_def]
show ?thesis using l2_commutative by auto
qed
moreover have "?prod d p'' p * l2_φ (p'' ! d) (p ! d) = ?prod (Suc d) p'' p"
proof -
have "insert d {0..<d} = {0..<Suc d}" by auto
moreover from prod.insert
have "(λ d'. l2_φ (p'' ! d') (p ! d')) d * prod (λ d'. l2_φ (p'' ! d') (p ! d')) {0..<d} =
prod (λ d'. l2_φ (p'' ! d') (p ! d')) (insert d {0..<d})"
by auto
hence "(prod (λ d'. l2_φ (p'' ! d') (p ! d')) {0..<d}) * (λ d'. l2_φ (p'' ! d') (p ! d')) d =
prod (λ d'. l2_φ (p'' ! d') (p ! d')) (insert d {0..<d})"
by auto
ultimately show ?thesis by auto
qed
ultimately show "α p'' * ?prod d p'' p' * l2_φ (p ! d) (p' ! d) = α p'' * ?prod (Suc d) p'' p" by auto
qed
finally show "(updown' dm lm d α p') * l2_φ (p ! d) (p' ! d) = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod (Suc d) p'' p)" by auto
qed
also have "… = (∑ (p', p'') ∈ (Sigma ?parents (?subgrid d)). α p'' * ?prod (Suc d) p'' p)"
by (rule sum.Sigma, auto simp add: parents_finite lgrid_finite)
also have "… = (∑ p''' ∈ (⋃ p' ∈ ?parents. (⋃ p'' ∈ ?subgrid d p'. { (p', p'') })).
( ((λ p''. α p'' * ?prod (Suc d) p'' p) o snd) p''') )" unfolding Sigma_def by (rule sum.cong[OF refl], auto)
also have "… = (∑ p'' ∈ snd ` (⋃ p' ∈ ?parents. (⋃ p'' ∈ ?subgrid d p'. { (p', p'') })). α p'' * (?prod (Suc d) p'' p))"
proof (rule sum.reindex[symmetric], rule inj_onI)
fix x y
assume "x ∈ (⋃p'∈parents d (base {d} p) p. ⋃p''∈lgrid (base {0..<d} p') {0..<d} lm. {(p', p'')})"
hence x_snd: "snd x ∈ grid (base {0..<d} (fst x)) {0..<d}" and "fst x ∈ grid (base {d} p) {d}" and "p ∈ grid (fst x) {d}"
unfolding parents_def lgrid_def by auto
hence x_spg: "fst x ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto

assume "y ∈ (⋃p'∈parents d (base {d} p) p. ⋃p''∈lgrid (base {0..<d} p') {0..<d} lm. {(p', p'')})"
hence y_snd: "snd y ∈ grid (base {0..<d} (fst y)) {0..<d}" and "fst y ∈ grid (base {d} p) {d}" and "p ∈ grid (fst y) {d}"
unfolding parents_def lgrid_def by auto
hence y_spg: "fst y ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto
hence "length (fst y) = dm" unfolding sparsegrid'_def by auto

assume "snd x = snd y"
have "fst x = fst y"
proof (rule nth_equalityI)
show l_eq: "length (fst x) = length (fst y)" using grid_length[OF ‹p ∈ grid (fst y) {d}›] grid_length[OF ‹p ∈ grid (fst x) {d}›]
by auto
show "fst x ! i = fst y ! i" if "i < length (fst x)" for i
proof -
have "i < length (fst y)" and "i < dm" using that l_eq and ‹length (fst y) = dm› by auto
show "fst x ! i = fst y ! i"
proof (cases "i = d")
case False hence "i ∉ {d}" by auto
with grid_invariant[OF ‹i < length (fst x)› this ‹p ∈ grid (fst x) {d}›]
grid_invariant[OF ‹i < length (fst y)› this ‹p ∈ grid (fst y) {d}›]
show ?thesis by auto
next
case True with grid_base_out[OF ‹i < dm› _ y_spg y_snd] grid_base_out[OF ‹i < dm› _ x_spg x_snd]
show ?thesis using ‹snd x = snd y› by auto
qed
qed
qed
show "x = y" using prod_eqI[OF ‹fst x = fst y› ‹snd x = snd y›] .
qed
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?parents. (⋃ p'' ∈ ?subgrid d p'. snd ` { (p', p'') })).
α p'' * (?prod (Suc d) p'' p))" by (auto simp only: image_UN)
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)" by auto
finally have down_part: "down dm lm d (updown' dm lm d α) p =
(∑ p'' ∈ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)" .

have "updown' dm lm (Suc d) α p =
(∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p'). α p'' * ?prod (Suc d) p'' p) +
(∑ p'' ∈ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)"
unfolding sum_vector_def updown'.simps down_part and up_part ..
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p') ∪ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)"
rule iffD2[OF disjoint_iff_not_equal], rule ballI, rule ballI)
fix x y
assume "x ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p')"
then obtain px where "px ∈ grid (base {0..<d} p) {0..<d}" and "x ∈ grid px {d}" and "x ≠ px" unfolding lgrid_def by auto
with grid_base_out[OF _ _ p_spg' this(1)] ‹Suc d ≤ dm› base_length[OF p_spg'] grid_level_d
have "lv px d < lv x d" and "px ! d = p ! d" by auto
hence "lv p d < lv x d" unfolding lv_def by auto
moreover
assume "y ∈ (⋃ p' ∈ ?parents. ?subgrid d p')"
then obtain py where y_grid: "y ∈ grid (base {0..<d} py) {0..<d}" and "py ∈ ?parents" unfolding lgrid_def by auto
hence "py ∈ grid (base {d} p) {d}" and "p ∈ grid py {d}" unfolding parents_def by auto
hence py_spg: "py ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto
have "y ! d = py ! d" using grid_base_out[OF _ _ py_spg y_grid] ‹Suc d ≤ dm› by auto
hence "lv y d ≤ lv p d" using grid_single_level[OF ‹p ∈ grid py {d}›] ‹Suc d ≤ dm› and sparsegrid'_length[OF py_spg] unfolding lv_def by auto
ultimately
show "x ≠ y" by auto
qed
also have "… = (∑ p' ∈ ?subgrid (Suc d) p. α p' * ?prod (Suc d) p' p)" (is "(∑ x ∈ ?in. ?F x) = (∑ x ∈ ?out. ?F x)")
proof (rule sum.mono_neutral_left, simp add: lgrid_finite)
show "?in ⊆ ?out" (is "?children ∪ ?siblings ⊆ _")
proof (rule subsetI)
fix x assume "x ∈ ?in"
show "x ∈ ?out"
proof (cases "x ∈ ?children")
case False hence "x ∈ ?siblings" using ‹x ∈ ?in› by auto
then obtain px where "px ∈ parents d (base {d} p) p" and "x ∈ lgrid (base {0..<d} px) {0..<d} lm" by auto
hence "level x < lm" and "px ∈ grid (base {d} p) {d}" and "x ∈ grid (base {0..<d} px) {0..<d}" and "{d} ∪ {0..<d} = {0..<Suc d}" unfolding lgrid_def parents_def by auto
with grid_base_union[OF p_spg' this(2) this(3)] show ?thesis unfolding lgrid_def by auto
next
have d_eq: "{0..<Suc d} ∪ {d} = {0..<Suc d}" by auto
case True
then obtain px where "px ∈ ?subgrid d p" and "x ∈ lgrid px {d} lm" and "x ≠ px" by auto
hence "px ∈ grid (base {0..<d} p) {0..<d}" and "x ∈ grid px {d}" and "level x < lm" and "{d} ∪ {0..<d} = {0..<Suc d}" unfolding lgrid_def by auto
have "px ∈ grid (base {0..<Suc d} p) {0..<Suc d}" by auto
from grid_transitive[OF ‹x ∈ grid px {d}› this]
show ?thesis unfolding lgrid_def using ‹level x < lm› d_eq by auto
qed
qed

show "∀ x ∈ ?out - ?in. ?F x = 0"
proof
fix x assume "x ∈ ?out - ?in"

hence "x ∈ ?out" and up_ps': "!! p'. p' ∈ ?subgrid d p ⟹ x ∉ lgrid p' {d} lm - {p'}"
and down_ps': "!! p'. p' ∈ ?parents ⟹ x ∉ ?subgrid d p'" by auto
hence x_eq: "x ∈ grid (base {0..<Suc d} p) {0..<Suc d}" and "level x < lm" unfolding lgrid_def by auto
hence up_ps: "!! p'. p' ∈ ?subgrid d p ⟹ x ∉ grid p' {d} - {p'}" and
down_ps: "!! p'. p' ∈ ?parents ⟹ x ∉ grid (base {0..<d} p') {0..<d}"
using up_ps' down_ps' unfolding lgrid_def by auto

have ds_eq: "{0..<Suc d} = {0..<d} ∪ {d}" by auto
have "x ∉ grid (base {0..<d} p) {0..<Suc d} - grid (base {0..<d} p) {0..<d}"
proof
assume "x ∈ grid (base {0..<d} p) {0..<Suc d} - grid (base {0..<d} p) {0..<d}"
hence "x ∈ grid (base {0..<d} p) ({d} ∪ {0..<d})" and x_ngrid: "x ∉ grid (base {0..<d} p) {0..<d}" using ds_eq by auto
from grid_split[OF this(1)] obtain px where px_grid: "px ∈ grid (base {0..<d} p) {0..<d}" and "x ∈ grid px {d}" by auto
from grid_level[OF this(2)] ‹level x < lm› have "level px < lm" by auto
hence "px ∈ ?subgrid d p" using px_grid unfolding lgrid_def by auto
hence "x ∉ grid px {d} - {px}" using up_ps by auto
moreover have "x ≠ px" proof (rule ccontr) assume "¬ x ≠ px" with px_grid and x_ngrid show False by auto qed
ultimately show False using ‹x ∈ grid px {d}› by auto
qed
moreover have "p ∈ ?parents" unfolding parents_def using baseE(2)[OF p_spg'] by auto
hence "x ∉ grid (base {0..<d} p) {0..<d}" by (rule down_ps)
ultimately have x_ngrid: "x ∉ grid (base {0..<d} p) {0..<Suc d}" by auto

have x_spg: "x ∈ sparsegrid' dm" using base_grid[OF p_spg'] x_eq by auto
hence "length x = dm" using grid_length by auto

let ?bx = "base {0..<d} x" and ?bp = "base {0..<d} p" and ?bx1 = "base {d} x" and ?bp1 = "base {d} p" and ?px = "p[d := x ! d]"

have x_nochild_p: "?bx ∉ grid ?bp {d}"
proof (rule ccontr)
assume "¬ base {0..<d} x ∉ grid (base {0..<d} p) {d}"
hence "base {0..<d} x ∈ grid (base {0..<d} p) {d}" by auto
from grid_transitive[OF baseE(2)[OF x_spg] this]
have "x ∈ grid (base {0..<d} p) {0..<Suc d}" using ds_eq by auto
thus False using x_ngrid by auto
qed

have "d < length ?bx" and "d < length ?bp" and "d < length ?bx1" and "d < length ?bp1" using base_length[OF x_spg] base_length[OF p_spg'] and ‹d < dm› by auto
have p_nochild_x: "?bp ∉ grid ?bx {d}" (is "?assm")
proof (rule ccontr)
have ds: "{0..<d} ∪ {0..<Suc d} = {d} ∪ {0..<d}" by auto
have d_sub: "{d} ⊆ {0..<Suc d}" by auto
assume "¬ ?assm" hence b_in_bx: "base {0..<d} p ∈ grid ?bx {d}" by auto

have "d ∉ {0..<d}" and "d ∈ {d}" by auto
from grid_replace_dim[OF ‹d < length ?bx› ‹d < length p› grid.Start[where b=p and ds="{d}"] b_in_bx]
have "p ∈ grid ?px {d}" unfolding base_out[OF ‹d < dm› ‹d ∉ {0..<d}› x_spg] base_out[OF ‹d < dm› ‹d ∉ {0..<d}› p_spg'] list_update_id .
moreover
from grid_replace_dim[OF ‹d < length ?bx1› ‹d < length ?bp1› baseE(2)[OF p_spg', where ds="{d}"] baseE(2)[OF x_spg, where ds="{d}"]]
have "?px ∈ grid ?bp1 {d}" unfolding base_in[OF ‹d < dm› ‹d ∈ {d}› x_spg] unfolding base_in[OF ‹d < dm› ‹d ∈ {d}› p_spg', symmetric] list_update_id .
ultimately
have "x ∉ grid (base {0..<d} ?px) {0..<d}" using down_ps[unfolded parents_def, where p'="?px"] by (auto simp only:)
moreover
have "base {0..<d} ?px = ?bx"
proof (rule nth_equalityI)
from ‹?px ∈ grid ?bp1 {d}› have px_spg: "?px ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto
from base_length[OF this] base_length[OF x_spg] show l_eq: "length (base {0..<d} ?px) = length ?bx"  by auto
show "base {0..<d} ?px ! i = ?bx ! i" if "i < length (base {0..<d} ?px)" for i
proof -
have "i < length ?bx" and "i < dm" using that l_eq and base_length[OF px_spg] by auto
show "base {0..<d} ?px ! i = ?bx ! i"
proof (cases "i < d")
case True hence "i ∈ {0..<d}" by auto
from base_in[OF ‹i < dm› this] show ?thesis using px_spg x_spg by auto
next
case False hence "i ∉ {0..<d}" by auto
have "?px ! i = x ! i"
proof (cases "i > d")
have i_le: "i < length (base {0..<Suc d} p)" using base_length[OF p_spg'] and ‹i < dm› by auto
case True hence "i ∉ {0..<Suc d}" by auto
from grid_invariant[OF i_le this x_eq] base_out[OF ‹i < dm› this p_spg']
show ?thesis using list_update_id and True by auto
next
case False hence "d = i" using ‹¬ i < d› by auto
thus ?thesis unfolding ‹d = i› using ‹i < dm› ‹length p = dm› nth_list_update_eq by auto
qed
thus ?thesis using base_out[OF ‹i < dm› ‹i ∉ {0..<d}› px_spg] base_out[OF ‹i < dm› ‹i ∉ {0..<d}› x_spg] by auto
qed
qed
qed
ultimately have "x ∉ grid ?bx {0..<d}" by auto
thus False using baseE(2)[OF x_spg] by auto
qed

have x_grid: "?bx ∈ grid (base {0..<Suc d} p) {d}" using grid_shift_base[OF _ p_spg' x_eq[unfolded ds_eq]] unfolding ds_eq by auto

have p_grid: "?bp ∈ grid (base {0..<Suc d} p) {d}" using grid_shift_base[OF _ p_spg' baseE(2)[OF p_spg', where ds="{0..<d} ∪ {d}"]] unfolding ds_eq by auto

have "l2_φ (?bp ! d) (?bx ! d) = 0"
proof (cases "lv ?bx d ≤ lv ?bp d")
case True from l2_disjoint[OF _ x_grid p_grid p_nochild_x this] ‹d < dm› and base_length[OF p_spg']
show ?thesis by auto
next
case False hence "lv ?bx d ≥ lv ?bp d" by auto
from l2_disjoint[OF _ p_grid x_grid x_nochild_p this] ‹d < dm› and base_length[OF p_spg']
show ?thesis by (auto simp: l2_commutative)
qed
hence "l2_φ (p ! d) (x ! d) = 0" using base_out[OF ‹d < dm›] p_spg' x_spg by auto
hence "∃ d ∈ {0..<Suc d}. l2_φ (p ! d) (x ! d) = 0" by auto
from prod_zero[OF _ this]
show "?F x = 0" by (auto simp: l2_commutative)
qed
qed
finally show ?case .
qed

theorem updown:
assumes p_spg: "p ∈ sparsegrid dm lm"
shows "updown dm lm α p = (∑ p' ∈ sparsegrid dm lm. α p' * l2 p' p)"
proof -
have "p ∈ sparsegrid' dm" using p_spg unfolding sparsegrid_def sparsegrid'_def lgrid_def by auto
have "!!p'. p' ∈ lgrid (base {0..<dm} p) {0..<dm} lm ⟹ length p' = dm"
proof -
fix p' assume "p' ∈ lgrid (base {0..<dm} p) {0..<dm} lm"
with base_grid[OF ‹p ∈ sparsegrid' dm›] have "p' ∈ sparsegrid' dm" unfolding lgrid_def by auto
thus "length p' = dm"  by auto
qed
thus ?thesis
unfolding updown_def sparsegrid_def base_start_eq[OF p_spg]
using updown'[OF _ p_spg, where d=dm] p_spg[unfolded sparsegrid_def lgrid_def]
by (auto simp: atLeast0LessThan p_spg[THEN sparsegrid_length] l2_eq)
qed

corollary
fixes α
assumes p: "p ∈ sparsegrid dm lm"
defines "f⇩α ≡ λx. (∑p∈sparsegrid dm lm. α p * Φ p x)"
shows "updown dm lm α p = (∫x. f⇩α x * Φ p x ∂(Π⇩M d∈{..<dm}. lborel))"
unfolding updown[OF p] l2_def f⇩α_def sum_distrib_right
apply (intro has_bochner_integral_integral_eq[symmetric] has_bochner_integral_sum)
apply (subst mult.assoc)
apply (intro has_bochner_integral_mult_right)