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)"
  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. (psparsegrid 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