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)" proof (rule sum.union_disjoint[symmetric], simp add: lgrid_finite, simp add: lgrid_finite parents_finite, 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 from grid_base_dim_add[OF _ p_spg' this(1)] 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) apply (simp add: sparsegrid_length) apply (rule has_bochner_integral_integrable) using p apply (simp add: sparsegrid_length Φ_def prod.distrib[symmetric]) proof (rule product_sigma_finite.product_integrable_prod) show "product_sigma_finite (λd. lborel)" .. qed (auto intro: integrable_φ2) end