Quelle  Up_Down.thy

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 inj_on_subset[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_\<alpha> ≡ λx. (∑p∈sparsegrid dm lm. α p * Φ p x)"
  shows "updown dm lm α p = (∫x. f_\<alpha> x * Φ p x ∂(Π_M d∈{..<dm}. lborel))"
  unfolding updown[OF p] l2_def f_\<alpha>_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