Session UpDown_Scheme

Theory Grid_Point

section ‹ Grid Points ›

theory Grid_Point
imports "HOL-Analysis.Multivariate_Analysis"
begin

type_synonym grid_point = "(nat × int) list"

definition lv :: "grid_point  nat  nat"
  where "lv p d = fst (p ! d)"

definition ix :: "grid_point  nat  int"
  where "ix p d = snd (p ! d)"

definition level :: "grid_point  nat"
  where "level p = ( i < length p. lv p i)"

lemma level_all_eq:
  assumes "d. d < length p  lv p d = lv p' d"
  and "length p = length p'"
  shows "level p' = level p"
  unfolding level_def using assms by auto

datatype dir = left | right

fun sgn :: "dir  int"
where
    "sgn left  = -1"
  | "sgn right =  1"

fun inv :: "dir  dir"
where
    "inv left = right"
  | "inv right = left"

lemma inv_inv[simp]: "inv (inv dir) = dir"
  by (cases dir) simp_all

lemma sgn_inv[simp]: "sgn (inv dir) = - sgn dir"
  by (cases dir, auto)

definition child :: "grid_point  dir  nat  grid_point"
  where "child p dir d = p[d := (lv p d + 1, 2 * (ix p d) + sgn dir)]"

lemma child_length[simp]: "length (child p dir d) = length p"
  unfolding child_def by simp

lemma child_odd[simp]: "d < length p  odd (ix (child p dir d) d)"
  unfolding child_def ix_def by (cases dir, auto)

lemma child_eq: "p ! d = (l, i)   j. child p dir d = p[d := (l + 1, j)]"
  by (auto simp add: child_def ix_def lv_def)

lemma child_other: "d  d'  child p dir d ! d' = p ! d'"
  unfolding child_def lv_def ix_def by (cases "d' < length p", auto)

lemma child_invariant: assumes "d' < length p" shows "(child p dir d ! d' = p ! d') = (d  d')"
proof -
  obtain l i where "p ! d' = (l, i)" using prod.exhaust .
  with assms show ?thesis
    unfolding child_def ix_def lv_def by auto
qed

lemma child_single_level: "d < length p  lv (child p dir d) d > lv p d"
  unfolding lv_def child_def by simp

lemma child_lv: "d < length p  lv (child p dir d) d = lv p d + 1"
  unfolding child_def lv_def by simp

lemma child_lv_other: assumes "d'  d" shows "lv (child p dir d') d = lv p d"
  using child_other[OF assms] unfolding lv_def by simp

lemma child_ix_left: "d < length p  ix (child p left d) d = 2 * ix p d - 1"
  unfolding child_def ix_def by simp

lemma child_ix_right: "d < length p  ix (child p right d) d = 2 * ix p d + 1"
  unfolding child_def ix_def by simp

lemma child_ix: "d < length p  ix (child p dir d) d = 2 * ix p d + sgn dir"
  unfolding child_def ix_def by simp

lemma child_level[simp]: assumes "d < length p"
  shows "level (child p dir d) = level p + 1"
proof -
  have inter: "{0..<length p}  {d} = {d}" using assms by auto

  have "level (child p dir d) =
    ( d' = 0..<length p. if d'  {d} then lv p d + 1 else lv p d')"
    by (auto intro!: sum.cong simp add: child_lv_other child_lv level_def)
  moreover have "level p + 1 =
    ( d' = 0..<length p. if d'  {d} then lv p d else lv p d') + 1"
    by (auto intro!: sum.cong simp add: child_lv_other child_lv level_def)
  ultimately show ?thesis
    unfolding sum.If_cases[OF finite_atLeastLessThan] inter
    using assms by auto
qed

lemma child_ex_neighbour: " b'. child b dir d = child b' (inv dir) d"
proof
  show "child b dir d = child (b[d := (lv b d, ix b d + sgn dir)]) (inv dir) d"
    unfolding child_def ix_def lv_def by (cases "d < length b", auto simp add: algebra_simps)
qed

lemma child_level_gt[simp]: "level (child p dir d) >= level p"
  by (cases "d < length p", simp, simp add: child_def)

lemma child_estimate_child:
  assumes "d < length p"
    and "l  lv p d"
    and i'_range: "ix p d < (i + 1) * 2^(lv p d - l) 
                   ix p d > (i - 1) * 2^(lv p d - l)"
                  (is "?top p  ?bottom p")
    and is_child: "p' = child p dir d"
  shows "?top p'  ?bottom p'"
proof
  from is_child and d < length p
  have "lv p' d = lv p d + 1" by (auto simp add: child_def ix_def lv_def)
  hence "lv p' d - l = lv p d - l + 1" using ‹lv p d >= l by auto
  hence pow_l'': "(2^(lv p' d - l) :: int) = 2 * 2^(lv p d - l)" by auto

  show "?top p'"
  proof -
    from is_child and d < length p
    have "ix p' d  2 * (ix p d) + 1"
      by (cases dir, auto simp add: child_def lv_def ix_def)
    also have " < (i + 1) * (2 * 2^(lv p d - l))" using i'_range by auto
    finally show ?thesis using pow_l'' by auto
  qed

  show "?bottom p'"
  proof -
    have "(i - 1) * 2^(lv p' d - l) = 2 * ((i - 1) * 2^(lv p d - l))"
      using pow_l'' by simp
    also have " < 2 * ix p d - 1" using i'_range by auto
    finally show ?thesis using is_child and d < length p
      by (cases dir, auto simp add: child_def lv_def ix_def)
  qed
qed

lemma child_neighbour: assumes "child p (inv dir) d = child ps dir d" (is "?c_p = ?c_ps")
  shows "ps = p[d := (lv p d, ix p d - sgn dir)]" (is "_ = ?ps")
proof (rule nth_equalityI)
  have "length ?c_ps = length ?c_p" using ?c_p = ?c_ps by simp
  hence len_eq: "length ps = length p" by simp
  thus "length ps = length ?ps" by simp

  show "ps ! i = ?ps ! i" if "i < length ps" for i
  proof -
    have "i < length p"
      using that len_eq by auto

    show "ps ! i = ?ps ! i"
    proof (cases "d = i")
      case [simp]: True

      have "?c_p ! i = ?c_ps ! i" using ?c_p = ?c_ps by auto
      hence "ix p i = ix ps d + sgn dir" and "lv p i = lv ps i"
        by (auto simp add: child_def
          nth_list_update_eq[OF i < length p]
          nth_list_update_eq[OF i < length ps])
      thus ?thesis by (simp add: lv_def ix_def i < length p)
    next
      assume "d  i"
      with child_other[OF this, of ps dir] child_other[OF this, of p "inv dir"]
      show ?thesis using assms by auto
    qed
  qed
qed

definition start :: "nat  grid_point"
where
  "start dm = replicate dm (0, 1)"

lemma start_lv[simp]: "d < dm  lv (start dm) d = 0"
  unfolding start_def lv_def by simp

lemma start_ix[simp]: "d < dm  ix (start dm) d = 1"
  unfolding start_def ix_def by simp

lemma start_length[simp]: "length (start dm) = dm"
  unfolding start_def by auto

lemma level_start_0[simp]: "level (start dm) = 0"
  using level_def by auto

end

Theory Grid

section ‹ Sparse Grids ›

theory Grid
imports Grid_Point
begin

subsection "Vectors"

type_synonym vector = "grid_point  real"

definition null_vector :: "vector"
where "null_vector  λ p. 0"

definition sum_vector :: "vector  vector  vector"
where "sum_vector α β  λ p. α p + β p"

subsection ‹ Inductive enumeration of all grid points ›

inductive_set
  grid :: "grid_point  nat set  grid_point set"
  for b :: "grid_point" and ds :: "nat set"
where
    Start[intro!]: "b  grid b ds"
  | Child[intro!]: " p  grid b ds ; d  ds   child p dir d  grid b ds"

lemma grid_length[simp]: "p'  grid p ds  length p' = length p"
  by (erule grid.induct, auto)

lemma grid_union_dims: " ds  ds' ; p  grid b ds   p  grid b ds'"
  by (erule grid.induct, auto)

lemma grid_transitive: " a  grid b ds ; b  grid c ds' ; ds'  ds'' ; ds  ds''   a  grid c ds''"
  by (erule grid.induct, auto simp add: grid_union_dims)

lemma grid_child[intro?]: assumes "d  ds" and p_grid: "p  grid (child b dir d) ds"
  shows "p  grid b ds"
  using d  ds grid_transitive[OF p_grid] by auto

lemma grid_single_level[simp]: assumes "p  grid b ds" and "d < length b"
  shows "lv b d  lv p d"
  using assms
proof induct
  case (Child p' d' dir)
  thus ?case by (cases "d' = d", auto simp add: child_def ix_def lv_def)
qed auto

lemma grid_child_level:
  assumes "d < length b"
  and p_grid: "p  grid (child b dir d) ds"
  shows "lv b d < lv p d"
proof -
  have "lv b d < lv (child b dir d) d" using child_lv[OF d < length b] by auto
  also have "  lv p d" using p_grid assms by (intro grid_single_level) auto
  finally show ?thesis .
qed

lemma child_out: "length p  d  child p dir d = p"
  unfolding child_def by auto

lemma grid_dim_remove:
  assumes inset: "p  grid b ({d}  ds)"
  and eq: "d < length b  p ! d = b ! d"
  shows "p  grid b ds"
  using inset eq
proof induct
  case (Child p' d' dir)
  show ?case
  proof (cases "d'  length p'")
    case True with child_out[OF this]
    show ?thesis using Child by auto
  next
    case False hence "d' < length p'" by simp
    show ?thesis
    proof (cases "d' = d")
      case True
      hence "lv b d  lv p' d" and "lv p' d < lv (child p' dir d) d"
        using child_single_level Child d' < length p' by auto
      hence False using Child and d' = d and lv_def and ¬ d'  length p' by auto
      thus ?thesis ..
    next
      case False
      hence "d'  ds" using Child by auto
      moreover have "d < length b  p' ! d = b ! d"
      proof -
        assume "d < length b"
        hence "d < length p'" using Child by auto
        hence "child p' dir d' ! d = p' ! d" using child_invariant and False by auto
        thus ?thesis using Child and d < length b by auto
      qed
      hence "p'  grid b ds" using Child by auto
      ultimately show ?thesis using grid.Child by auto
    qed
  qed
qed auto

lemma gridgen_dim_restrict:
  assumes inset: "p  grid b (ds'  ds)"
  and eq: " d  ds'. d  length b"
  shows "p  grid b ds"
  using inset eq
proof induct
  case (Child p' d dir)
  thus ?case
  proof (cases "d  ds")
    case False thus ?thesis using Child and child_def by auto
  qed auto
qed auto

lemma grid_dim_remove_outer: "grid b ds = grid b {d  ds. d < length b}"
proof
  have "{d  ds. d < length b}  ds" by auto
  from grid_union_dims[OF this]
  show "grid b {d  ds. d < length b}  grid b ds" by auto

  have "ds = (ds - {d  ds. d < length b})  {d  ds. d < length b}" by auto
  moreover
  have "grid b ((ds - {d  ds. d < length b})  {d  ds. d < length b})  grid b {d  ds. d < length b}"
  proof
    fix p
    assume "p  grid b (ds - {d  ds. d < length b}  {d  ds. d < length b})"
    moreover have " d  (ds - {d  ds. d < length b}). d  length b" by auto
    ultimately show "p  grid b {d  ds. d < length b}" by (rule gridgen_dim_restrict)
  qed
  ultimately show "grid b ds  grid b {d  ds. d < length b}" by auto
qed

lemma grid_level[intro]: assumes "p  grid b ds" shows "level b  level p"
proof -
  have *: "length p = length b" using grid_length assms by auto
  { fix i assume "i  {0 ..< length p}"
    hence "lv b i  lv p i" using p  grid b ds and grid_single_level * by auto
  } thus ?thesis unfolding level_def * by (auto intro!: sum_mono)
qed
lemma grid_empty_ds[simp]: "grid b {} = { b }"
proof -
  have "!! z. z  grid b {}  z = b"
    by (erule grid.induct, auto)
  thus ?thesis by auto
qed
lemma grid_Start: assumes inset: "p  grid b ds" and eq: "level p = level b" shows "p = b"
  using inset eq
proof induct
  case (Child p d dir)
  show ?case
  proof (cases "d < length b")
    case True
    from Child
    have "level p  level b" by auto
    moreover
    have "level p  level (child p dir d)" by (rule child_level_gt)
    hence "level p  level b" using Child by auto
    ultimately have "level p = level b" by auto
    hence "p = b " using Child(2) by auto
    with Child(4) have "level (child b dir d) = level b" by auto
    moreover have "level (child b dir d)   level b" using child_level and d < length b by auto
    ultimately show ?thesis by auto
  next
    case False
    with Child have "length p = length b" by auto
    with False have "child p dir d = p" using child_def by auto
    moreover with Child have "level p = level b" by auto
    with Child(2) have "p = b" by auto
    ultimately show ?thesis by auto
  qed
qed auto
lemma grid_estimate:
  assumes "d < length b" and p_grid: "p  grid b ds"
  shows "ix p d < (ix b d + 1) * 2^(lv p d - lv b d)  ix p d > (ix b d - 1) * 2^(lv p d - lv b d)"
  using p_grid
proof induct
  case (Child p d' dir)
  show ?case
  proof (cases "d = d'")
    case False with Child show ?thesis unfolding child_def lv_def ix_def by auto
  next
    case True with child_estimate_child and Child and d < length b
    show ?thesis using grid_single_level by auto
  qed
qed auto
lemma grid_odd: assumes "d < length b" and p_diff: "p ! d  b ! d" and p_grid: "p  grid b ds"
  shows "odd (ix p d)"
  using p_grid and p_diff
proof induct
  case (Child p d' dir)
  show ?case
  proof (cases "d = d'")
    case True with child_odd and d < length b and Child show ?thesis by auto
  next
    case False with Child and d < length b show ?thesis using child_def and ix_def and lv_def by auto
  qed
qed auto
lemma grid_invariant: assumes "d < length b" and "d  ds" and p_grid: "p  grid b ds"
  shows "p ! d = b ! d"
  using p_grid
proof (induct)
  case (Child p d' dir) hence "d'  d" using d  ds by auto
  thus ?case using child_def and Child by auto
qed auto
lemma grid_part: assumes "d < length b" and p_valid: "p  grid b {d}" and p'_valid: "p'  grid b {d}"
  and level: "lv p' d  lv p d"
  and right: "ix p' d  (ix p d + 1) * 2^(lv p' d - lv p d)" (is "?right p p' d")
  and left: "ix p' d  (ix p d - 1) * 2^(lv p' d - lv p d)" (is "?left p p' d")
  shows "p'  grid p {d}"
  using p'_valid left right level and p_valid
proof induct
  case (Child p' d' dir)
  hence "d = d'" by auto
  let ?child = "child p' dir d'"

  show ?case
  proof (cases "lv p d = lv ?child d")
    case False
    moreover have "lv ?child d = lv p' d + 1" using child_lv and d < length b and Child and d = d' by auto
    ultimately have "lv p d < lv p' d + 1" using Child by auto
    hence lv: "Suc (lv p' d) - lv p d = Suc (lv p' d - lv p d)" by auto

    have "?left p p' d  ?right p p' d"
    proof (cases dir)
      case left
      with Child have "2 * ix p' d - 1  (ix p d + 1) * 2^(Suc (lv p' d) - lv p d)"
        using d = d' and d < length b by (auto simp add: child_def ix_def lv_def)
      also have " = 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" using lv by auto
      finally have "2 * ix p' d - 2 < 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" by auto
      also have " = 2 * ((ix p d + 1) * 2^(lv p' d - lv p d))" by auto
      finally have left_r: "ix p' d  (ix p d + 1) * 2^(lv p' d - lv p d)" by auto

      have "2 * ((ix p d - 1) * 2^(lv p' d - lv p d)) = 2 * (ix p d - 1) * 2^(lv p' d - lv p d)" by auto
      also have " = (ix p d - 1) * 2^(Suc (lv p' d) - lv p d)" using lv by auto
      also have "  2 * ix p' d - 1"
        using left and Child and d = d' and d < length b by (auto simp add: child_def ix_def lv_def)
      finally have right_r: "((ix p d - 1) * 2^(lv p' d - lv p d))  ix p' d" by auto

      show ?thesis using left_r and right_r by auto
    next
      case right
      with Child have "2 * ix p' d + 1  (ix p d + 1) * 2^(Suc (lv p' d) - lv p d)"
        using d = d' and d < length b by (auto simp add: child_def ix_def lv_def)
      also have " = 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" using lv by auto
      finally have "2 * ix p' d < 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" by auto
      also have " = 2 * ((ix p d + 1) * 2^(lv p' d - lv p d))" by auto
      finally have left_r: "ix p' d  (ix p d + 1) * 2^(lv p' d - lv p d)" by auto

      have "2 * ((ix p d - 1) * 2^(lv p' d - lv p d)) = 2 * (ix p d - 1) * 2^(lv p' d - lv p d)" by auto
      also have " = (ix p d - 1) * 2^(Suc (lv p' d) - lv p d)" using lv by auto
      also have "  2 * ix p' d + 1"
        using right and Child and d = d' and d < length b by (auto simp add: child_def ix_def lv_def)
      also have " < 2 * (ix p' d + 1)" by auto
      finally have right_r: "((ix p d - 1) * 2^(lv p' d - lv p d))  ix p' d" by auto

      show ?thesis using left_r and right_r by auto
    qed
    with Child and lv have "p'  grid p {d}" by auto
    thus ?thesis using d = d' by auto
  next
    case True
    moreover with Child have "?left p ?child d  ?right p ?child d" by auto
    ultimately have range: "ix p d - 1  ix ?child d  ix ?child d  ix p d + 1" by auto

    have "p ! d  b ! d"
    proof (rule ccontr)
      assume "¬ (p ! d  b ! d)"
      with ‹lv p d = lv ?child d have "lv b d = lv ?child d" by (auto simp add: lv_def)
      hence "lv b d = lv p' d + 1" using d = d' and Child and d < length b and child_lv by auto
      moreover have "lv b d  lv p' d" using d = d' and Child and d < length b and grid_single_level by auto
      ultimately show False by auto
    qed
    hence "odd (ix p d)" using grid_odd and p  grid b {d} and d < length b by auto
    hence "¬ odd (ix p d + 1)" and "¬ odd (ix p d - 1)" by auto

    have "d < length p'" using p'  grid b {d} and d < length b by auto
    hence odd_child: "odd (ix ?child d)" using child_odd and d = d' by auto

    have "ix p d - 1  ix ?child d"
    proof (rule ccontr)
      assume "¬ (ix p d - 1  ix ?child d)"
      hence "odd (ix p d - 1)" using odd_child by auto
      thus False using ¬ odd (ix p d - 1) by auto
    qed
    moreover
    have "ix p d + 1  ix ?child d"
    proof (rule ccontr)
      assume "¬ (ix p d + 1  ix ?child d)"
      hence "odd (ix p d + 1)" using odd_child by auto
      thus False using ¬ odd (ix p d + 1) by auto
    qed
    ultimately have "ix p d = ix ?child d" using range by auto
    with True have d_eq: "p ! d = (?child) ! d" by (auto simp add: prod_eqI ix_def lv_def)

    have "length p = length ?child" using p  grid b {d} and p'  grid b {d} by auto
    moreover have "p ! d'' = ?child ! d''" if "d'' < length p" for d''
    proof -
      have "d'' < length b" using that p  grid b {d} by auto
      show "p ! d'' = ?child ! d''"
      proof (cases "d = d''")
        case True with d_eq show ?thesis by auto
      next
        case False hence "d''  {d}" by auto
        from d'' < length b and this and p  grid b {d}
        have "p ! d'' = b ! d''" by (rule grid_invariant)
        also have " = p' ! d''" using d'' < length b and d''  {d} and p'  grid b {d}
          by (rule grid_invariant[symmetric])
        also have " = ?child ! d''"
        proof -
          have "d'' < length p'" using d'' < length b and p'  grid b {d} by auto
          hence "?child ! d'' = p' ! d''" using child_invariant and d  d'' and d = d' by auto
          thus ?thesis by auto
        qed
        finally show ?thesis .
      qed
    qed
    ultimately have "p = ?child" by (rule nth_equalityI)
    thus "?child  grid p {d}" by auto
  qed
next
  case Start
  moreover hence "lv b d  lv p d" using grid_single_level and d < length b by auto
  ultimately have "lv b d = lv p d" by auto

  have "level p = level b"
  proof -
    { fix d'
      assume "d' < length b"
      have "lv b d' = lv p d'"
      proof (cases "d = d'")
        case True with ‹lv b d = lv p d show ?thesis by auto
      next
        case False hence "d'  {d}" by auto
        from d' < length b and this and p  grid b {d}
        have "p ! d' = b ! d'" by (rule grid_invariant)
        thus ?thesis by (auto simp add: lv_def)
      qed }
    moreover have "length b = length p" using p  grid b {d} by auto
    ultimately show ?thesis by (rule level_all_eq)
  qed
  hence "p = b" using grid_Start and p  grid b {d} by auto
  thus ?case by auto
qed
lemma grid_disjunct: assumes "d < length p"
  shows "grid (child p left d) ds  grid (child p right d) ds = {}"
  (is "grid ?l ds  grid ?r ds = {}")
proof (intro set_eqI iffI)
  fix x
  assume "x  grid ?l ds  grid ?r ds"
  hence "ix x d < (ix ?l d + 1) * 2^(lv x d - lv ?l d)"
    and "ix x d > (ix ?r d - 1) * 2^(lv x d - lv ?r d)"
    using grid_estimate d < length p by auto
  thus "x  {}" using d < length p and child_lv and child_ix by auto
qed auto

lemma grid_level_eq: assumes eq: " d  ds. lv p d = lv b d" and grid: "p  grid b ds"
  shows "level p = level b"
proof (rule level_all_eq)
  { fix i assume "i < length b"
    show "lv b i = lv p i"
    proof (cases "i  ds")
      case True with eq show ?thesis by auto
    next case False with i < length b and grid show ?thesis
        using lv_def ix_def grid_invariant by auto
    qed }
  show "length b = length p" using grid by auto
qed

lemma grid_partition:
  "grid p {d} = {p}  grid (child p left d) {d}  grid (child p right d) {d}"
  (is "_ = _  grid ?l {d}  grid ?r {d}")
proof -
  have "!! x.  x  grid p {d} ; x  p ; x  grid ?r {d}   x  grid ?l {d}"
  proof (cases "d < length p")
    case True
    fix x

    let "?nr_r p" = "ix x d > (ix p d + 1) * 2 ^ (lv x d - lv p d)"
    let "?nr_l p" = "(ix p d - 1) * 2 ^ (lv x d - lv p d) > ix x d"

    have ix_r_eq: "ix ?r d = 2 * ix p d + 1" using d < length p and child_ix by auto
    have lv_r_eq: "lv ?r d = lv p d + 1" using d < length p and child_lv by auto

    have ix_l_eq: "ix ?l d = 2 * ix p d - 1" using d < length p and child_ix by auto
    have lv_l_eq: "lv ?l d = lv p d + 1" using d < length p and child_lv by auto

    assume "x  grid p {d}" and "x  p" and "x  grid ?r {d}"
    hence "lv p d  lv x d" using grid_single_level and d < length p by auto
    moreover have "lv p d  lv x d"
    proof (rule ccontr)
      assume "¬ lv p d  lv x d"
      hence "level x = level p" using x  grid p {d} and grid_level_eq[where ds="{d}"] by auto
      hence "x = p" using grid_Start and x  grid p {d} by auto
      thus False using x  p by auto
    qed
    ultimately have "lv p d < lv x d" by auto
    hence "lv ?r d  lv x d" and "?r  grid p {d}" using child_lv and d < length p by auto
    with d < length p and x  grid p {d}
    have r_range: "¬ ?nr_r ?r  ¬ ?nr_l ?r  x  grid ?r {d}"
      using grid_part[where p="?r" and p'=x and b=p and d=d] by auto
    have "x  grid ?r {d}  ?nr_l ?r  ?nr_r ?r" by (rule ccontr, auto simp add: r_range)
    hence "?nr_l ?r  ?nr_r ?r" using x  grid ?r {d} by auto

    have gt0: "lv x d - lv p d > 0" using ‹lv p d < lv x d by auto

    have ix_shift: "ix ?r d = ix ?l d + 2" and lv_lr: "lv ?r d = lv ?l d" and right1: "!! x :: int. x + 2 - 1 = x + 1"
      using d < length p and child_ix and child_lv by auto

    have "lv x d - lv p d = Suc (lv x d - (lv p d + 1))"
      using gt0 by auto
    hence lv_shift: "!! y :: int. y * 2 ^ (lv x d - lv p d) = y * 2 * 2 ^ (lv x d - (lv p d + 1))"
      by auto

    have "ix x d < (ix p d + 1) * 2 ^ (lv x d - lv p d)"
      using x  grid p {d} grid_estimate and d < length p by auto
    also have " = (ix ?r d + 1) * 2 ^ (lv x d - lv ?r d)"
      using ‹lv p d < lv x d and ix_r_eq and lv_r_eq lv_shift[where y="ix p d + 1"] by auto
    finally have "?nr_l ?r" using ?nr_l ?r  ?nr_r ?r by auto
    hence r_bound: "(ix ?l d + 1) * 2 ^ (lv x d - lv ?l d) > ix x d"
      unfolding ix_shift lv_lr using right1 by auto

    have "(ix ?l d - 1) * 2 ^ (lv x d - lv ?l d) = (ix p d - 1) * 2 * 2 ^ (lv x d - (lv p d + 1))"
      unfolding ix_l_eq lv_l_eq by auto
    also have " = (ix p d - 1) * 2 ^ (lv x d - lv p d)"
      using lv_shift[where y="ix p d - 1"] by auto
    also have "  < ix x d"
      using x  grid p {d} grid_estimate and d < length p by auto
    finally have l_bound: "(ix ?l d - 1) * 2 ^ (lv x d - lv ?l d) < ix x d" .

    from l_bound r_bound d < length p and x  grid p {d} ‹lv ?r d  lv x d and lv_lr
    show "x  grid ?l {d}" using grid_part[where p="?l" and p'=x and d=d] by auto
  qed (auto simp add: child_def)
  thus ?thesis by (auto intro: grid_child)
qed
lemma grid_change_dim: assumes grid: "p  grid b ds"
  shows "p[d := X]  grid (b[d := X]) ds"
  using grid
proof induct
  case (Child p d' dir)
  show ?case
  proof (cases "d  d'")
    case True
    have "(child p dir d')[d := X] = child (p[d := X]) dir d'"
      unfolding child_def and ix_def and lv_def
      unfolding list_update_swap[OF d  d'] and nth_list_update_neq[OF d  d'] ..
    thus ?thesis using Child by auto
  next
    case False hence "d = d'" by auto
    with Child show ?thesis unfolding child_def d = d' list_update_overwrite by auto
  qed
qed auto
lemma grid_change_dim_child: assumes grid: "p  grid b ds" and "d  ds"
  shows "child p dir d  grid (child b dir d) ds"
proof (cases "d < length b")
  case True thus ?thesis using grid_change_dim[OF grid]
    unfolding child_def lv_def ix_def grid_invariant[OF True d  ds grid] by auto
next
  case False hence "length b  d" and "length p  d" using grid by auto
  thus ?thesis unfolding child_def using list_update_beyond assms by auto
qed
lemma grid_split: assumes grid: "p  grid b (ds'  ds)" shows " x  grid b ds. p  grid x ds'"
  using grid
proof induct
  case (Child p d dir)
  show ?case
  proof (cases "d  ds'")
    case True with Child show ?thesis by auto
  next
    case False
    hence "d  ds" using Child by auto
    obtain x where "x  grid b ds" and "p  grid x ds'" using Child by auto
    hence "child x dir d  grid b ds" using d  ds by auto
    moreover have "child p dir d  grid (child x dir d) ds'"
      using p  grid x ds' False and grid_change_dim_child by auto
    ultimately show ?thesis by auto
  qed
qed auto
lemma grid_union_eq: "( p  grid b ds. grid p ds') = grid b (ds'  ds)"
  using grid_split and grid_transitive[where ds''="ds'  ds" and ds=ds' and ds'=ds, OF _ _ Un_upper2 Un_upper1] by auto
lemma grid_onedim_split:
  "grid b (ds  {d}) = grid b ds  grid (child b left d) (ds  {d})  grid (child b right d) (ds  {d})"
  (is "_ = ?g  ?l (ds  {d})  ?r (ds  {d})")
proof -
  have "?g  ?l (ds  {d})  ?r (ds  {d}) = ?g  ( p  ?l {d}. grid p ds)  ( p  ?r {d}. grid p ds)"
    unfolding grid_union_eq ..
  also have " = ( p  ({b}  ?l {d}  ?r {d}). grid p ds)" by auto
  also have " = ( p  grid b {d}. grid p ds)" unfolding grid_partition[where p=b] ..
  finally show ?thesis unfolding grid_union_eq by auto
qed
lemma grid_child_without_parent: assumes grid: "p  grid (child b dir d) ds" (is "p  grid ?c ds") and "d < length b"
  shows "p  b"
proof -
  have "level ?c  level p" using grid by (rule grid_level)
  hence "level b < level p" using child_level and d < length b by auto
  thus ?thesis by auto
qed
lemma grid_disjunct':
  assumes "p  grid b ds" and "p'  grid b ds" and "x  grid p ds'" and "p  p'" and "ds  ds' = {}"
  shows "x  grid p' ds'"
proof (rule ccontr)
  assume "¬ x  grid p' ds'" hence "x  grid p' ds'" by auto
  have l: "length b = length p" and l': "length b = length p'" using p  grid b ds and p'  grid b ds by auto
  hence "length p' = length p" by auto
  moreover have " d < length p'. p' ! d = p ! d"
  proof (rule allI, rule impI)
    fix d assume dl': "d < length p'" hence "d < length b" using l' by auto
    hence dl: "d < length p" using l by auto
    show "p' ! d = p ! d"
    proof (cases "d  ds'")
      case True with ds  ds' = {} have "d  ds" by auto
      hence "p' ! d = b ! d" and "p ! d = b ! d"
        using d < length b p'  grid b ds and p  grid b ds and grid_invariant by auto
      thus ?thesis by auto
    next
      case False
      show ?thesis
        using grid_invariant[OF dl' False x  grid p' ds']
          and grid_invariant[OF dl False x  grid p ds'] by auto
    qed
  qed
  ultimately have "p' = p" by (metis nth_equalityI)
  thus False using p  p' by auto
qed
lemma grid_split1: assumes grid: "p  grid b (ds'  ds)" and "ds  ds' = {}"
  shows "∃! x  grid b ds. p  grid x ds'"
proof (rule ex_ex1I)
  obtain x where "x  grid b ds" and "p  grid x ds'" using grid_split[OF grid] by auto
  thus " x. x  grid b ds  p  grid x ds'" by auto
next
  fix x y
  assume "x  grid b ds  p  grid x ds'" and "y  grid b ds  p  grid y ds'"
  hence "x  grid b ds" and "p  grid x ds'" and "y  grid b ds" and "p  grid y ds'" by auto
  show "x = y"
  proof (rule ccontr)
    assume "x  y"
    from grid_disjunct'[OF x  grid b ds y  grid b ds p  grid x ds' this ds  ds' = {}]
    show False using p  grid y ds' by auto
  qed
qed

subsection ‹ Grid Restricted to a Level ›

definition lgrid :: "grid_point  nat set  nat  grid_point set"
where "lgrid b ds lm = { p  grid b ds. level p < lm }"

lemma lgridI[intro]:
  " p  grid b ds ; level p < lm   p  lgrid b ds lm"
  unfolding lgrid_def by simp

lemma lgridE[elim]:
  assumes "p  lgrid b ds lm"
  assumes " p  grid b ds ; level p < lm   P"
  shows P
  using assms unfolding lgrid_def by auto

lemma lgridI_child[intro]:
  "d  ds  p  lgrid (child b dir d) ds lm  p  lgrid b ds lm"
  by (auto intro: grid_child)

lemma lgrid_empty[simp]: "lgrid p ds (level p) = {}"
proof (rule equals0I)
  fix p' assume "p'  lgrid p ds (level p)"
  hence "level p' < level p" and "level p  level p'" by auto
  thus False by auto
qed

lemma lgrid_empty': assumes "lm  level p" shows "lgrid p ds lm = {}"
proof (rule equals0I)
  fix p' assume "p'  lgrid p ds lm"
  hence "level p' < lm" and "level p  level p'" by auto
  thus False using lm  level p by auto
qed

lemma grid_not_child:
  assumes [simp]: "d < length p"
  shows "p  grid (child p dir d) ds"
proof (rule ccontr)
  assume "¬ ?thesis"
  have "level p < level (child p dir d)" by auto
  with grid_level[OF ¬ ?thesis[unfolded not_not]]
  show False by auto
qed

subsection ‹ Unbounded Sparse Grid ›

definition sparsegrid' :: "nat  grid_point set"
where
  "sparsegrid' dm = grid (start dm) { 0 ..< dm }"

lemma grid_subset_alldim:
  assumes p: "p  grid b ds"
  defines "dm  length b"
  shows "p  grid b {0..<dm}"
proof -
  have "ds  {dm..}  ds  {0..<dm} = ds" by auto
  from gridgen_dim_restrict[where ds="ds  {0..<dm}" and ds'="ds  {dm..}"] this
  have "ds  {0..<dm}  {0..<dm}"
    and "p  grid b (ds  {0..<dm})" using p unfolding dm_def by auto
  thus ?thesis by (rule grid_union_dims)
qed

lemma sparsegrid'_length[simp]:
  "b  sparsegrid' dm  length b = dm" unfolding sparsegrid'_def by auto

lemma sparsegrid'I[intro]:
  assumes b: "b  sparsegrid' dm" and p: "p  grid b ds"
  shows "p  sparsegrid' dm"
  using sparsegrid'_length[OF b] b
       grid_transitive[OF grid_subset_alldim[OF p], where c="start dm" and ds''="{0..<dm}"]
  unfolding sparsegrid'_def by auto

lemma sparsegrid'_start:
  assumes "b  grid (start dm) ds"
  shows "b  sparsegrid' dm"
  unfolding sparsegrid'_def
  using grid_subset_alldim[OF assms] by simp

subsection ‹ Sparse Grid ›

definition sparsegrid :: "nat  nat  grid_point set"
where
  "sparsegrid dm lm = lgrid (start dm) { 0 ..< dm } lm"

lemma sparsegrid_length: "p  sparsegrid dm lm  length p = dm"
  by (auto simp: sparsegrid_def)

lemma sparsegrid_subset[intro]: "p  sparsegrid dm lm  p  sparsegrid' dm"
  unfolding sparsegrid_def sparsegrid'_def lgrid_def by auto

lemma sparsegridI[intro]:
  assumes "p  sparsegrid' dm" and "level p < lm"
  shows "p  sparsegrid dm lm"
  using assms unfolding sparsegrid'_def sparsegrid_def lgrid_def by auto

lemma sparsegrid_start:
  assumes "b  lgrid (start dm) ds lm"
  shows "b  sparsegrid dm lm"
proof
  have "b  grid (start dm) ds" using assms by auto
  thus "b  sparsegrid' dm" by (rule sparsegrid'_start)
qed (insert assms, auto)

lemma sparsegridE[elim]:
  assumes "p  sparsegrid dm lm"
  shows "p  sparsegrid' dm" and "level p < lm"
  using assms unfolding sparsegrid'_def sparsegrid_def lgrid_def by auto

subsection ‹ Compute Sparse Grid Points ›

fun gridgen :: "grid_point  nat set  nat  grid_point list"
where
  "gridgen p ds 0 = []"
| "gridgen p ds (Suc l) = (let
      sub = λ d. gridgen (child p left d) { d'  ds . d'  d } l @
                 gridgen (child p right d) { d'  ds . d'  d } l
      in p # concat (map sub [ d  [0 ..< length p]. d  ds]))"

lemma gridgen_lgrid_eq: "set (gridgen p ds l) = lgrid p ds (level p + l)"
proof (induct l arbitrary: p ds)
  case (Suc l)
  let "?subg dir d" = "set (gridgen (child p dir d) { d'  ds . d'   d } l)"
  let "?sub dir d" = "lgrid (child p dir d) { d'  ds . d'   d } (level p + Suc l)"
  let "?union F dm" = "{p}  ( d  { d  ds. d < dm }. F left d  F right d)"

  have hyp: "!! dir d. d < length p  ?subg dir d = ?sub dir d"
    using Suc.hyps using child_level by auto

  { fix dm assume "dm  length p"
    hence "?union ?sub dm = lgrid p {d  ds. d < dm} (level p + Suc l)"
    proof (induct dm)
      case (Suc dm)
      hence "dm  length p" by auto

      let ?l = "child p left dm" and ?r = "child p right dm"

      have p_lgrid: "p  lgrid p {d  ds. d < dm} (level p + Suc l)" by auto

      show ?case
      proof (cases "dm  ds")
        case True
        let ?ds = "{d  ds. d < dm}  {dm}"
        have ds_eq: "{d'  ds. d'  dm} = ?ds" using True by auto
        have ds_eq': "{d  ds. d < Suc dm} = {d  ds. d < dm }  {dm}" using True by auto

        have "?union ?sub (Suc dm) = ?union ?sub dm  ({p}  ?sub left dm  ?sub right dm)"
          unfolding ds_eq' by auto
        also have " = lgrid p {d  ds. d < dm} (level p + Suc l)  ?sub left dm  ?sub right dm"
          unfolding Suc.hyps[OF dm  length p] using p_lgrid by auto
        also have " = {p'  grid p {d  ds. d<dm}  (grid ?l ?ds)  (grid ?r ?ds).
          level p' < level p + Suc l}" unfolding lgrid_def ds_eq by auto
        also have " = lgrid p {d  ds. d < Suc dm} (level p + Suc l)"
          unfolding lgrid_def ds_eq' unfolding grid_onedim_split[where b=p] ..
        finally show ?thesis .
      next
        case False hence "{d  ds. d < Suc dm} = {d  ds. d < dm  d = dm}" by auto
        hence ds_eq: "{d  ds. d < Suc dm} = {d  ds. d < dm}" using dm  ds by auto
        show ?thesis unfolding ds_eq Suc.hyps[OF dm  length p] ..
      qed
    next case 0 thus ?case unfolding lgrid_def by auto
    qed }
  hence "?union ?sub (length p) = lgrid p {d  ds. d < length p} (level p + Suc l)" by auto
  hence union_lgrid_eq: "?union ?sub (length p) = lgrid p ds (level p + Suc l)"
    unfolding lgrid_def using grid_dim_remove_outer by auto

  have "set (gridgen p ds (Suc l)) = ?union ?subg (length p)"
    unfolding gridgen.simps and Let_def by auto
  hence "set (gridgen p ds (Suc l)) = ?union ?sub (length p)"
    using hyp by auto
  also have " = lgrid p ds (level p + Suc l)"
    using union_lgrid_eq .
  finally show ?case .
qed auto

lemma gridgen_distinct: "distinct (gridgen p ds l)"
proof (induct l arbitrary: p ds)
  case (Suc l)
  let ?ds = "[d  [0..<length p]. d  ds]"
  let "?left d" = "gridgen (child p left d) { d'  ds . d'  d } l"
  and "?right d" = "gridgen (child p right d) { d'  ds . d'  d } l"
  let "?sub d" = "?left d @ ?right d"

  have "distinct (concat (map ?sub ?ds))"
  proof (cases l)
    case (Suc l')

    have inj_on: "inj_on ?sub (set ?ds)"
    proof (rule inj_onI, rule ccontr)
      fix d d' assume "d  set ?ds" and "d'  set ?ds"
      hence "d < length p" and "d  set ?ds" and "d' < length p" by auto
      assume *: "?sub d = ?sub d'"
      have in_d: "child p left d  set (?sub d)"
        using d  set ?ds Suc
        by (auto simp add: gridgen_lgrid_eq lgrid_def grid_Start)

      have in_d': "child p left d'  set (?sub d')"
        using d  set ?ds Suc
        by (auto simp add: gridgen_lgrid_eq lgrid_def grid_Start)

      { fix p' d assume "d  set ?ds" and "p'  set (?sub d)"
        hence "lv p d < lv p' d"
          using grid_child_level
          by (auto simp add: gridgen_lgrid_eq lgrid_def grid_child_level) }
      note level_less = this

      assume "d  d'"
      show False
      proof (cases "d' < d")
        case True
        with in_d' ?sub d = ?sub d' level_less[OF d  set ?ds]
        have "lv p d < lv (child p left d') d" by simp
        thus False unfolding lv_def
          using child_invariant[OF d < length p, of left d'] d  d'
          by auto
      next
        case False hence "d < d'" using d  d' by auto
        with in_d ?sub d = ?sub d' level_less[OF d'  set ?ds]
        have "lv p d' < lv (child p left d) d'" by simp
        thus False unfolding lv_def
          using child_invariant[OF d' < length p, of left d] d  d'
          by auto
      qed
    qed

    show ?thesis
    proof (rule distinct_concat)
      show "distinct (map ?sub ?ds)"
        unfolding distinct_map using inj_on by simp
    next
      fix ys assume "ys  set (map ?sub ?ds)"
      then obtain d where "d  ds" and "d < length p"
        and *: "ys = ?sub d" by auto

      show "distinct ys" unfolding *
        using grid_disjunct[OF d < length p, of "{d'  ds. d'  d}"]
          gridgen_lgrid_eq lgrid_def ‹distinct (?left d) ‹distinct (?right d)
        by auto
    next
      fix ys zs
      assume "ys  set (map ?sub ?ds)"
      then obtain d where ys: "ys = ?sub d" and "d  set ?ds" by auto
      hence "d < length p" by auto

      assume "zs  set (map ?sub ?ds)"
      then obtain d' where zs: "zs = ?sub d'" and "d'  set ?ds" by auto
      hence "d' < length p" by auto

      assume "ys  zs"
      hence "d'  d" unfolding ys zs by auto

      show "set ys  set zs = {}"
      proof (rule ccontr)
        assume "¬ ?thesis"
        then obtain p' where "p'  set (?sub d)" and "p'  set (?sub d')"
          unfolding ys zs by auto

        hence "lv p d < lv p' d" "lv p d' < lv p' d'"
          using grid_child_level d  set ?ds d'  set ?ds
          by (auto simp add: gridgen_lgrid_eq lgrid_def grid_child_level)

        show False
        proof (cases "d < d'")
          case True
          from p'  set (?sub d)
          have "p ! d' = p' ! d'"
            using grid_invariant[of d' "child p right d" "{d'  ds. d'  d}"]
            using grid_invariant[of d' "child p left d" "{d'  ds. d'  d}"]
            using child_invariant[of d' _ _ d] d < d' d' < length p
            using gridgen_lgrid_eq lgrid_def by auto
          thus False using ‹lv p d' < lv p' d' unfolding lv_def by auto
        next
          case False hence "d' < d" using d'  d by simp
          from p'  set (?sub d')
          have "p ! d = p' ! d"
            using grid_invariant[of d "child p right d'" "{d  ds. d  d'}"]
            using grid_invariant[of d "child p left d'" "{d  ds. d  d'}"]
            using child_invariant[of d _ _ d'] d' < d d < length p
            using gridgen_lgrid_eq lgrid_def by auto
          thus False using ‹lv p d < lv p' d unfolding lv_def by auto
        qed
      qed
    qed
  qed (simp add: map_replicate_const)
  moreover
  have "p  set (concat (map ?sub ?ds))"
    using gridgen_lgrid_eq lgrid_def grid_not_child[of _ p] by simp
  ultimately show ?case
    unfolding gridgen.simps Let_def distinct.simps by simp
qed auto

lemma lgrid_finite: "finite (lgrid b ds lm)"
proof (cases "level b  lm")
  case True from iffD1[OF le_iff_add True]
  obtain l where l: "lm = level b + l" by auto
  show ?thesis unfolding l gridgen_lgrid_eq[symmetric] by auto
next
  case False hence "!! x. x  grid b ds  (¬ level x < lm)"
  proof -
    fix x assume "x  grid b ds"
    from grid_level[OF this] show "¬ level x < lm" using False by auto
  qed
  hence "lgrid b ds lm = {}" unfolding lgrid_def by auto
  thus ?thesis by auto
qed

lemma lgrid_sum:
  fixes F :: "grid_point  real"
  assumes "d < length b" and "level b < lm"
  shows "( p  lgrid b {d} lm. F p) =
          ( p  lgrid (child b left d) {d} lm. F p) + ( p  lgrid (child b right d) {d} lm. F p) + F b"
  (is "( p  ?grid b. F p) = ( p  ?grid ?l . F p) + (?sum (?grid ?r)) + F b")
proof -
  have "!! dir. b  ?grid (child b dir d)"
    using grid_child_without_parent[where ds="{d}"] and d < length b and lgrid_def by auto
  hence b_distinct: "b  (?grid ?l  ?grid ?r)" by auto

  have "?grid ?l  ?grid ?r = {}"
    unfolding lgrid_def using grid_disjunct and d < length b by auto
  from lgrid_finite lgrid_finite and this
  have child_eq: "?sum ((?grid ?l)  (?grid ?r)) = ?sum (?grid ?l) + ?sum (?grid ?r)"
    by (rule sum.union_disjoint)

  have "?grid b = {b}  (?grid ?l)  (?grid ?r)" unfolding lgrid_def grid_partition[where p=b] using assms by auto
  hence "?sum (?grid b) = F b + ?sum ((?grid ?l)  (?grid ?r))" using b_distinct and lgrid_finite by auto
  thus ?thesis using child_eq by auto
qed

subsection ‹ Base Points ›

definition base :: "nat set  grid_point  grid_point"
where "base ds p = (THE b. b  grid (start (length p)) ({0 ..< length p} - ds)  p  grid b ds)"

lemma baseE: assumes p_grid: "p  sparsegrid' dm"
  shows "base ds p  grid (start dm) ({0..<dm} - ds)"
  and "p  grid (base ds p) ds"
proof -
  from p_grid[unfolded sparsegrid'_def]
  have *: "∃! x  grid (start dm) ({0..<dm} - ds). p  grid x ds"
    by (intro grid_split1) (auto intro: grid_union_dims)
  then obtain x where x_eq: "x  grid (start dm) ({0..<dm} - ds)  p  grid x ds"
    by auto
  with * have "base ds p = x" unfolding base_def by auto
  thus "base ds p  grid (start dm) ({0..<dm} - ds)" and "p  grid (base ds p) ds"
    using x_eq by auto
qed

lemma baseI: assumes x_grid: "x  grid (start dm) ({0..<dm} - ds)" and p_xgrid: "p  grid x ds"
  shows "base ds p = x"
proof -
  have "p  grid (start dm) (ds  ({0..<dm} - ds))"
    using grid_transitive[OF p_xgrid x_grid, where ds''="ds  ({0..<dm} - ds)"] by auto
  moreover have "ds  ({0..<dm} - ds) = {}" by auto
  ultimately have "∃! x  grid (start dm) ({0..<dm} - ds). p  grid x ds"
    using grid_split1[where p=p and b="start dm" and ds'=ds and ds="{0..<dm} - ds"] by auto
  thus "base ds p = x" using x_grid p_xgrid unfolding base_def by auto
qed

lemma base_empty: assumes p_grid: "p  sparsegrid' dm" shows "base {} p = p"
  using grid_empty_ds and p_grid and grid_split1[where ds="{0..<dm}" and ds'="{}"] unfolding base_def sparsegrid'_def by auto

lemma base_start_eq: assumes p_spg: "p  sparsegrid dm lm"
  shows "start dm = base {0..<dm} p"
proof -
  from p_spg
  have "start dm  grid (start dm) ({0..<dm} - {0..<dm})"
    and "p  grid (start dm) {0..<dm}" using sparsegrid'_def by auto
  from baseI[OF this(1) this(2)] show ?thesis by auto
qed

lemma base_in_grid: assumes p_grid: "p  sparsegrid' dm" shows "base ds p  grid (start dm) {0..<dm}"
proof -
  let ?ds = "ds  {0..<dm}"
  have ds_eq: "{ d  ?ds. d < length (start dm) } = { 0..< dm}"
    unfolding start_def by auto
  have "base ds p  grid (start dm) ?ds"
    using grid_union_dims[OF _ baseE(1)[OF p_grid, where ds=ds], where ds'="?ds"] by auto
  thus ?thesis using grid_dim_remove_outer[where b="start dm" and ds="?ds"] unfolding ds_eq by auto
qed

lemma base_grid: assumes p_grid: "p  sparsegrid' dm" shows "grid (base ds p) ds  sparsegrid' dm"
proof
  fix x assume xgrid: "x  grid (base ds p) ds"
  have ds_eq: "{ d  {0..<dm}  ds. d < length (start dm) } = {0..<dm}" by auto
  from grid_transitive[OF xgrid base_in_grid[OF p_grid], where ds''="{0..<dm}  ds"]
  show "x  sparsegrid' dm" unfolding sparsegrid'_def
    using grid_dim_remove_outer[where b="start dm" and ds="{0..<dm}  ds"] unfolding ds_eq unfolding Un_ac(3)[of "{0..<dm}"]
    by auto
qed
lemma base_length[simp]: assumes p_grid: "p  sparsegrid' dm" shows "length (base ds p) = dm"
proof -
  from baseE[OF p_grid] have "base ds p  grid (start dm) ({0..<dm} - ds)" by auto
  thus ?thesis by auto
qed
lemma base_in[simp]: assumes "d < dm" and "d  ds" and p_grid: "p  sparsegrid' dm" shows "base ds p ! d = start dm ! d"
proof -
  have ds: "d  {0..<dm} - ds" using d  ds by auto
  have "d < length (start dm)" using d < dm by auto
  with grid_invariant[OF this ds] baseE(1)[OF p_grid] show ?thesis by auto
qed
lemma base_out[simp]: assumes "d < dm" and "d  ds" and p_grid: "p  sparsegrid' dm" shows "base ds p ! d = p ! d"
proof -
  have "d < length (base ds p)" using base_length[OF p_grid] d < dm by auto
  with grid_invariant[OF this d  ds] baseE(2)[OF p_grid] show ?thesis by auto
qed
lemma base_base: assumes p_grid: "p  sparsegrid' dm" shows "base ds (base ds' p) = base (ds  ds') p"
proof (rule nth_equalityI)
  have b_spg: "base ds' p  sparsegrid' dm" unfolding sparsegrid'_def
    using grid_union_dims[OF Diff_subset[where A="{0..<dm}" and B="ds'"] baseE(1)[OF p_grid]] .
  from base_length[OF b_spg] base_length[OF p_grid] show "length (base ds (base ds' p)) = length (base (ds  ds') p)" by auto

  show "base ds (base ds' p) ! i = base (ds  ds') p ! i" if "i < length (base ds (base ds' p))" for i
  proof -
    have "i < dm" using that base_length[OF b_spg] by auto
    show "base ds (base ds' p) ! i = base (ds  ds') p ! i"
    proof (cases "i  ds  ds'")
      case True
      show ?thesis
      proof (cases "i  ds")
        case True from base_in[OF i < dm i  ds  ds' p_grid] base_in[OF i < dm this b_spg] show ?thesis by auto
      next
        case False hence "i  ds'" using i  ds  ds' by auto
        from base_in[OF i < dm i  ds  ds' p_grid] base_out[OF i < dm i  ds b_spg] base_in[OF i < dm i  ds' p_grid] show ?thesis by auto
      qed
    next
      case False hence "i  ds" and "i  ds'" by auto
      from base_out[OF i < dm i  ds  ds' p_grid] base_out[OF i < dm i  ds b_spg] base_out[OF i < dm i  ds' p_grid] show ?thesis by auto
    qed
  qed
qed
lemma grid_base_out: assumes "d < dm" and "d  ds" and p_grid: "b  sparsegrid' dm" and "p  grid (base ds b) ds"
  shows "p ! d = b ! d"
proof -
  have "base ds b ! d = b ! d" using assms by auto
  moreover have "d < length (base ds b)" using assms by auto
  from grid_invariant[OF this]
  have "p ! d = base ds b ! d" using assms by auto
  ultimately show ?thesis by auto
qed

lemma grid_grid_inj_on: assumes "ds  ds' = {}" shows "inj_on snd (p'grid b ds. p''grid p' ds'. {(p', p'')})"
proof (rule inj_onI)
  fix x y
  assume "x  (p'grid b ds. p''grid p' ds'. {(p', p'')})"
  hence "snd x  grid (fst x) ds'" and "fst x  grid b ds" by auto

  assume "y  (p'grid b ds. p''grid p' ds'. {(p', p'')})"
  hence "snd y  grid (fst y) ds'" and "fst y  grid b ds" by auto

  assume "snd x = snd y"
  have "fst x = fst y"
  proof (rule ccontr)
    assume "fst x  fst y"
    from grid_disjunct'[OF ‹fst x  grid b ds ‹fst y  grid b ds ‹snd x  grid (fst x) ds' this ds  ds' = {}]
    show False using ‹snd y  grid (fst y) ds' unfolding ‹snd x = snd y by auto
  qed
  show "x = y" using prod_eqI[OF ‹fst x = fst y ‹snd x = snd y] .
qed

lemma grid_level_d: assumes "d < length b" and p_grid: "p  grid b {d}" and "p  b" shows "lv p d > lv b d"
proof -
  from p_grid[unfolded grid_partition[where p=b]]
  show ?thesis using grid_child_level using assms by auto
qed

lemma grid_base_base: assumes "b  sparsegrid' dm"
  shows "base ds' b  grid (base ds (base ds' b)) (ds  ds')"
proof -
  from base_grid[OF b  sparsegrid' dm] have "base ds' b  sparsegrid' dm" by auto
  from grid_union_dims[OF _ baseE(2)[OF this], of ds "ds  ds'"] show ?thesis by auto
qed

lemma grid_base_union: assumes b_spg: "b  sparsegrid' dm" and p_grid: "p  grid (base ds b) ds" and x_grid: "x  grid (base ds' p) ds'"
  shows "x  grid (base (ds  ds') b) (ds  ds')"
proof -
  have ds_union: "ds  ds' = ds'  (ds  ds')" by auto

  from base_grid[OF b_spg] p_grid have p_spg: "p  sparsegrid' dm"  by auto
  with assms and grid_base_base have base_b': "base ds' p  grid (base ds (base ds' p)) (ds  ds')" by auto
  moreover have "base ds' (base ds b) = base ds' (base ds p)" (is "?b = ?p")
  proof (rule nth_equalityI)
    have bb_spg: "base ds b  sparsegrid' dm" using base_grid[OF b_spg] grid.Start by auto
    hence "dm = length (base ds b)" by auto
    have bp_spg: "base ds p  sparsegrid' dm" using base_grid[OF p_spg] grid.Start by auto

    show "length ?b = length ?p" using base_length[OF bp_spg] base_length[OF bb_spg] by auto
    show "?b ! i = ?p ! i" if "i < length ?b" for i
    proof -
      have "i < dm" and "i < length (base ds b)" using that base_length[OF bb_spg] dm = length (base ds b) by auto
      show "?b ! i = ?p ! i"
      proof (cases "i  ds  ds'")
        case True
        hence "!! x. base ds x  sparsegrid' dm  x  sparsegrid' dm  base ds' (base ds x) ! i = (start dm) ! i"
        proof - fix x assume x_spg: "x  sparsegrid' dm" and xb_spg: "base ds x  sparsegrid' dm"
          show "base ds' (base ds x) ! i = (start dm) ! i"
          proof (cases "i  ds'")
            case True from base_in[OF i < dm this xb_spg] show ?thesis .
          next
            case False hence "i  ds" using i  ds  ds' by auto
            from base_out[OF i < dm False xb_spg] base_in[OF i < dm this x_spg] show ?thesis by auto
          qed
        qed
        from this[OF bp_spg p_spg] this[OF bb_spg b_spg] show ?thesis by auto
      next
        case False hence "i  ds" and "i  ds'" by auto
        from grid_invariant[OF i < length (base ds b) i  ds p_grid]
          base_out[OF i < dm i  ds' bp_spg] base_out[OF i < dm i  ds p_spg] base_out[OF i < dm i  ds' bb_spg]
        show ?thesis by auto
      qed
    qed
  qed
  ultimately have "base ds' p  grid (base (ds  ds') b) (ds  ds')"
    by (simp only: base_base[OF p_spg] base_base[OF b_spg] Un_ac(3))
  from grid_transitive[OF x_grid this] show ?thesis using ds_union by auto
qed
lemma grid_base_dim_add: assumes "ds'  ds" and b_spg: "b  sparsegrid' dm" and p_grid: "p  grid (base ds' b) ds'"
  shows "p  grid (base ds b) ds"
proof -
  have ds_eq: "ds'  ds = ds" using assms by auto

  have "p  sparsegrid' dm" using base_grid[OF b_spg] p_grid by auto
  hence "p  grid (base ds p) ds" using baseE by auto
  from grid_base_union[OF b_spg p_grid this]
  show ?thesis using ds_eq by auto
qed
lemma grid_replace_dim: assumes "d < length b'" and "d < length b" and p_grid: "p  grid b ds" and p'_grid: "p'  grid b' ds"
  shows "p[d := p' ! d]  grid (b[d := b' ! d]) ds" (is "_  grid ?b ds")
  using p'_grid and p_grid
proof induct
  case (Child p'' d' dir)
  hence p''_grid: "p[d := p'' ! d]  grid ?b ds" and "d < length p''" using assms by auto
  have "d < length p" using p_grid assms by auto
  thus ?case
  proof (cases "d' = d")
    case True
    from grid.Child[OF p''_grid d'  ds]
    show ?thesis unfolding child_def ix_def lv_def list_update_overwrite d' = d nth_list_update_eq[OF d < length p''] nth_list_update_eq[OF d < length p] .
  next
    case False
    show ?thesis unfolding child_def nth_list_update_neq[OF False] using Child by auto
  qed
qed (rule grid_change_dim)
lemma grid_shift_base:
  assumes ds_dj: "ds  ds' = {}" and b_spg: "b  sparsegrid' dm" and p_grid: "p  grid (base (ds'  ds) b) (ds'  ds)"
  shows "base ds' p  grid (base (ds  ds') b) ds"
proof -
  from grid_split[OF p_grid]
  obtain x where x_grid: "x  grid (base (ds'  ds) b) ds" and p_xgrid: "p  grid x ds'" by auto
  from grid_union_dims[OF _ this(1)]
  have x_spg: "x  sparsegrid' dm" using base_grid[OF b_spg] by auto

  have b_len: "length (base (ds'  ds) b) = dm" using base_length[OF b_spg] by auto

  define d' where "d' = dm"
  moreover have "d'  dm  x  grid (start dm) ({0..<dm} - {d  ds'. d < d'})"
  proof (induct d')
    case (Suc d')
    with b_len have d'_b: "d' < length (base (ds'  ds) b)" by auto
    show ?case
    proof (cases "d'  ds'")
      case True hence "d'  ds" and "d'  ds'  ds" using ds_dj by auto
      have "{0..<dm} - {d  ds'. d < d'} = ({0..<dm} - {d  ds'. d < d'}) - {d'}  {d'}" using ‹Suc d'  dm by auto
      also have " = ({0..<dm} - {d  ds'. d < Suc d'})  {d'}" by auto
      finally have x_g: "x  grid (start dm) ({d'}  ({0..<dm} - {d  ds'. d < Suc d'}))" using Suc by auto
      from grid_invariant[OF d'_b d'  ds x_grid] base_in[OF _ d'  ds'  ds b_spg] ‹Suc d'  dm
      have "x ! d' = start dm ! d'" by auto
      from grid_dim_remove[OF x_g this] show ?thesis .
    next
      case False
      hence "{d  ds'. d < Suc d'} = {d  ds'. d < d'  d = d'}" by auto
      also have " = {d  ds'. d < d'}" using False by auto
      finally show ?thesis using Suc by auto
    qed
  next
    case 0 show ?case using x_spg[unfolded sparsegrid'_def] by auto
  qed
  moreover have "{0..<dm} - ds' = {0..<dm} - {d  ds'. d < dm}" by auto
  ultimately have "x  grid (start dm) ({0..<dm} - ds')" by auto
  from baseI[OF this p_xgrid] and x_grid
  show ?thesis by (auto simp: Un_ac(3))
qed

subsection ‹ Lift Operation over all Grid Points ›

definition lift :: "(nat  nat  grid_point  vector  vector)  nat  nat  nat  vector  vector"
where "lift f dm lm d = foldr (λ p. f d (lm - level p) p) (gridgen (start dm) ({ 0 ..< dm } - { d }) lm)"

lemma lift:
  assumes "d < dm" and "p  sparsegrid dm lm"
  and Fintro: " l b p α.  b  lgrid (start dm) ({0..<dm} - {d}) lm ;
                          l + level b = lm ; p  sparsegrid dm lm 
              F d l b α p = (if b = base {d} p
                               then ( p'  lgrid b {d} lm. S (α p') p p')
                               else α p)"
  shows "lift F dm lm d α p = ( p'  lgrid (base {d} p) {d} lm. S (α p') p p')"
        (is "?lift = ?S p α")
proof -
  let ?gridgen = "gridgen (start dm) ({0..<dm} - {d}) lm"
  let "?f p" = "F d (lm - level p) p"

  { fix bs β b
    assume "set bs  set ?gridgen" and "distinct bs" and "p  sparsegrid dm lm"
    hence "foldr ?f bs β p = (if base {d} p  set bs then ?S p β else β p)"
    proof (induct bs arbitrary: p)
      case (Cons b bs)
      hence "b  lgrid (start dm) ({0..<dm} - {d}) lm"
        and "(lm - level b) + level b = lm"
        and b_grid: "b  grid (start dm) ({0..<dm} - {d})"
        using lgrid_def gridgen_lgrid_eq by auto
      note F = Fintro[OF this(1,2) p  sparsegrid dm lm]

      have "b  set bs" using ‹distinct (b#bs) by auto

      show ?case
      proof (cases "base {d} p  set (b#bs)")
        case True note base_in_set = this

        show ?thesis
        proof (cases "b = base {d} p")
          case True
          moreover
          { fix p' assume "p'  lgrid b {d} lm"
            hence "p'  grid b {d}" and "level p' < lm" unfolding lgrid_def by auto
            from grid_transitive[OF this(1) b_grid, of "{0..<dm}"] d < dm
              baseI[OF b_grid p'  grid b {d}] b  set bs
              Cons.prems Cons.hyps[of p'] this(2)
            have "foldr ?f bs β p' = β p'" unfolding sparsegrid_def lgrid_def by auto }
          ultimately show ?thesis
            using F base_in_set by auto
        next
          case False
          with base_in_set have "base {d} p  set bs" by auto
          with Cons.hyps[of p] Cons.prems
          have "foldr ?f bs β p = ?S p β" by auto
          thus ?thesis using F base_in_set False by auto
        qed
      next
        case False
        hence "b  base {d} p" by auto
        from False Cons.hyps[of p] Cons.prems
        have "foldr ?f bs β p = β p" by auto
        thus ?thesis using False F b  base {d} p by auto
      qed
    qed auto
  }
  moreover have "base {d} p  set ?gridgen"
  proof -
    have "p  grid (base {d} p) {d}"
      using p  sparsegrid dm lm[THEN sparsegrid_subset] by (rule baseE)
    from grid_level[OF this] baseE(1)[OF sparsegrid_subset[OF p  sparsegrid dm lm]]
    show ?thesis using p  sparsegrid dm lm
      unfolding gridgen_lgrid_eq sparsegrid'_def lgrid_def sparsegrid_def
      by auto
  qed
  ultimately show ?thesis unfolding lift_def
    using gridgen_distinct p  sparsegrid dm lm by auto
qed

subsection ‹ Parent Points ›

definition parents :: "nat  grid_point  grid_point  grid_point set"
where "parents d b p = { x  grid b {d}. p  grid x {d} }"

lemma parents_split: assumes p_grid: "p  grid (child b dir d) {d}"
  shows "parents d b p = { b }  parents d (child b dir d) p"
proof (intro set_eqI iffI)
  let ?chd = "child b dir d" and ?chid = "child b (inv dir) d"
  fix x assume "x  parents d b p"
  hence "x  grid b {d}" and "p  grid x {d}" unfolding parents_def by auto
  hence x_split: "x  {b}  grid ?chd {d}  grid ?chid {d}" using grid_onedim_split[where ds="{}" and b=b] and grid_empty_ds
    by (cases dir, auto)
  thus "x  {b}  parents d (child b dir d) p"
  proof (cases "x = b")
    case False
    have "d < length b"
    proof (rule ccontr)
      assume "¬ d < length b" hence empty: "{d'  {d}. d' < length b} = {}" by auto
      have "x = b" using x  grid b {d}
        unfolding grid_dim_remove_outer[where ds="{d}" and b=b] empty
        using grid_empty_ds by auto
      thus False using ¬ x = b by auto
    qed
    have "x  grid ?chid {d}"
    proof (rule ccontr)
      assume "¬ x  grid ?chid {d}"
      hence "p  grid ?chid {d}" using grid_transitive[OF p  grid x {d}, where ds'="{d}"]
        by auto
      hence "p  grid ?chd {d}" using grid_disjunct[OF d < length b] by (cases dir, auto)
      thus False using p  grid ?chd {d} ..
    qed
    with False and x_split
    have "x  grid ?chd {d}" by auto
    thus ?thesis unfolding parents_def using p  grid x {d} by auto
  qed auto
next
  let ?chd = "child b dir d" and ?chid = "child b (inv dir) d"
  fix x assume x_in: "x  {b}  parents d ?chd p"
  thus "x  parents d b p"
  proof (cases "x = b")
    case False
    hence "x  parents d ?chd p" using x_in by auto
    thus ?thesis unfolding parents_def using grid_child[where b=b] by auto
  next
    from p_grid have "p  grid b {d}" using grid_child[where b=b] by auto
    case True thus ?thesis unfolding parents_def using p  grid b {d} by auto
  qed
qed

lemma parents_no_parent: assumes "d < length b" shows "b  parents d (child b dir d) p" (is "_  parents _ ?ch _")
proof
  assume "b  parents d ?ch p" hence "b  grid ?ch {d}" unfolding parents_def by auto
  from grid_level[OF this]
  have "level b + 1  level b" unfolding child_level[OF d < length b] .
  thus False by auto
qed

lemma parents_subset_lgrid: "parents d b p  lgrid b {d} (level p + 1)"
proof
  fix x assume "x  parents d b p"
  hence "x  grid b {d}" and "p  grid x {d}" unfolding parents_def by auto
  moreover hence "level x  level p" using grid_level by auto
  hence "level x < level p + 1" by auto
  ultimately show "x  lgrid b {d} (level p + 1)" unfolding lgrid_def by auto
qed

lemma parents_finite: "finite (parents d b p)"
  using finite_subset[OF parents_subset_lgrid lgrid_finite] .

lemma parent_sum: assumes p_grid: "p  grid (child b dir d) {d}" and "d < length b"
  shows "( x  parents d b p. F x) = F b + ( x  parents d (child b dir d) p. F x)"
  unfolding parents_split[OF p_grid] using parents_no_parent[OF d < length b, where dir=dir and p=p] using parents_finite
  by auto

lemma parents_single: "parents d b b = { b }"
proof
  have "parents d b b  lgrid b {d} (level b + (Suc 0))" using parents_subset_lgrid by auto
  also have " = {b}" unfolding gridgen_lgrid_eq[symmetric] gridgen.simps Let_def by auto
  finally show "parents d b b  { b }" .
next
  have "b  parents d b b" unfolding parents_def by auto
  thus "{ b }  parents d b b" by auto
qed

lemma grid_single_dimensional_specification:
  assumes "d < length b"
  and "odd i"
  and "lv b d + l' = l"
  and "i < (ix b d + 1) * 2^l'"
  and "i > (ix b d - 1) * 2^l'"
  shows "b[d := (l,i)]  grid b {d}"
using assms proof (induct l' arbitrary: b)
  case 0
  hence "i = ix b d" and "l = lv b d" by auto
  thus ?case unfolding ix_def lv_def by auto
next
  case (Suc l')

  have "d  {d}" by auto

  show ?case
  proof (rule linorder_cases)
    assume "i = ix b d * 2^(Suc l')"
    hence "even i" by auto
    thus ?thesis using ‹odd i by blast
  next
    assume *: "i < ix b d * 2^(Suc l')"

    let ?b = "child b left d"

    have "d < length ?b" using Suc by auto
    moreover note ‹odd i
    moreover have "lv ?b d + l' = l"
      and "i < (ix ?b d + 1) * 2^l'"
      and "(ix ?b d - 1) * 2^l' < i"
      unfolding child_ix_left[OF Suc.prems(1)]
      using Suc.prems * child_lv by (auto simp add: field_simps)
    ultimately have "?b[d := (l,i)]  grid ?b {d}"
      by (rule Suc.hyps)
    thus ?thesis
      by (auto intro!: grid_child[OF d  {d}, of _ b left]
        simp add: child_def)
  next
    assume *: "ix b d * 2^(Suc l') < i"

    let ?b = "child b right d"

    have "d < length ?b" using Suc by auto
    moreover note ‹odd i
    moreover have "lv ?b d + l' = l"
      and "i < (ix ?b d + 1) * 2^l'"
      and "(ix ?b d - 1) * 2^l' < i"
      unfolding child_ix_right[OF Suc.prems(1)]
      using Suc.prems * child_lv by (auto simp add: field_simps)
    ultimately have "?b[d := (l,i)]  grid ?b {d}"
      by (rule Suc.hyps)
    thus ?thesis
      by (auto intro!: grid_child[OF d  {d}, of _ b right]
        simp add: child_def)
  qed
qed

lemma grid_multi_dimensional_specification:
  assumes "dm  length b" and "length p = length b"
  and " d. d < dm 
    odd (ix p d) 
    lv b d  lv p d 
    ix p d < (ix b d + 1) * 2^(lv p d - lv b d) 
    ix p d > (ix b d - 1) * 2^(lv p d - lv b d)"
    (is " d. d < dm  ?bounded p d")
  and " d.  dm  d ; d < length b   p ! d = b ! d"
  shows "p  grid b {0..<dm}"
using assms proof (induct dm arbitrary: p)
  case 0
  hence "p = b" by (auto intro!: nth_equalityI)
  thus ?case by auto
next
  case (Suc dm)
  hence "dm  length b"
    and "dm < length p" by auto

  let ?p = "p[dm := b ! dm]"

  note dm  length b
  moreover have "length ?p = length b" using ‹length p = length b by simp
  moreover
  {
    fix d assume "d < dm"
    hence *: "d < Suc dm" and "dm  d" by auto
    have "?p ! d = p ! d"
      by (rule nth_list_update_neq[OF dm  d])
    hence "?bounded ?p d"
      using Suc.prems(3)[OF *] lv_def ix_def
      by simp
  }
  moreover
  {
    fix d assume "dm  d" and "d < length b"
    have "?p ! d = b ! d"
    proof (cases "d = dm")
      case True thus ?thesis using d < length b ‹length p = length b by auto
    next
      case False
      hence "Suc dm  d" using dm  d by auto
      thus ?thesis using Suc.prems(4) d < length b by auto
    qed
  }
  ultimately
  have *: "?p  grid b {0..<dm}"
    by (auto intro!: Suc.hyps)

  have "lv b dm  lv p dm" using Suc.prems(3)[OF lessI] by simp

  have [simp]: "lv ?p dm = lv b dm" using lv_def dm < length p by auto
  have [simp]: "ix ?p dm = ix b dm" using ix_def dm < length p by auto
  have [simp]: "p[dm := (lv p dm, ix p dm)] = p"
    using lv_def ix_def dm < length p by auto
  have "dm < length ?p" and
    [simp]: "lv b dm + (lv p dm - lv b dm) = lv p dm"
    using dm < length p ‹lv b dm  lv p dm by auto
  from grid_single_dimensional_specification[OF this(1),
    where l="lv p dm" and i="ix p dm" and l'="lv p dm - lv b dm", simplified]
  have "p  grid ?p {dm}"
    using Suc.prems(3)[OF lessI] by blast
  from grid_transitive[OF this *]
  show ?case by auto
qed

lemma sparsegrid:
  "sparsegrid dm lm = {p.
    length p = dm  level p < lm 
    ( d < dm. odd (ix p d)  0 < ix p d  ix p d < 2^(lv p d + 1))}"
  (is "_ = ?set")
proof (rule equalityI[OF subsetI subsetI])
  fix p
  assume *: "p  sparsegrid dm lm"
  hence "length p = dm" and "level p < lm" unfolding sparsegrid_def by auto
  moreover
  { fix d assume "d < dm"
    hence **: "p  grid (start dm) {0..<dm}" and "d < length (start dm)"
      using * unfolding sparsegrid_def by auto
    have "odd (ix p d)"
    proof (cases "p ! d = start dm ! d")
      case True
      thus ?thesis unfolding start_def using d < dm ix_def by auto
    next
      case False
      from grid_odd[OF _ this **]
      show ?thesis using d < dm by auto
    qed
    hence "odd (ix p d)  0 < ix p d  ix p d < 2^(lv p d + 1)"
      using grid_estimate[OF d < length (start dm) **]
      unfolding ix_def lv_def start_def using d < dm by auto
  }
  ultimately show "p  ?set"
    using sparsegrid_def lgrid_def by auto
next
  fix p
  assume "p  ?set"
  with grid_multi_dimensional_specification[of dm "start dm" p]
  have "p  grid (start dm) {0..<dm}" and "level p < lm"
    by auto
  thus "p  sparsegrid dm lm"
    unfolding sparsegrid_def lgrid_def by auto
qed

end

Theory Triangular_Function

section ‹ Hat Functions ›

theory Triangular_Function
imports
 "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
 Grid
begin

lemma continuous_on_max[continuous_intros]:
  fixes f :: "_  'a::linorder_topology"
  shows "continuous_on S f  continuous_on S g  continuous_on S (λx. max (f x) (g x))"
  by (auto simp: continuous_on_def intro: tendsto_max)

definition φ :: "(nat × int)  real  real" where
  "φ  (λ(l,i) x. max 0 (1 - ¦ x * 2^(l + 1) - real_of_int i ¦))"

definition Φ :: "(nat × int) list  (nat  real)  real" where
  "Φ p x = (d<length p. φ (p ! d) (x d))"

definition l2_φ where
  "l2_φ p1 p2 = (x. φ p1 x * φ p2 x lborel)"

definition l2 where
  "l2 a b = (x. Φ a x * Φ b x (ΠM d{..<length a}. lborel))"

lemma measurable_φ[measurable]: p  borel_measurable borel"
  by (cases p) (simp add: φ_def)

lemma φ_nonneg: "0  φ p x"
  by (simp add: φ_def split: prod.split)

lemma φ_zero_iff:
  (l,i) x = 0  x  {real_of_int (i - 1) / 2^(l + 1) <..< real_of_int (i + 1) / 2^(l + 1)}"
  by (auto simp: φ_def field_simps split: split_max)

lemma φ_zero: "x  {real_of_int (i - 1) / 2^(l + 1) <..< real_of_int (i + 1) / 2^(l + 1)}  φ (l,i) x = 0"
  unfolding φ_zero_iff by simp

lemma φ_eq_0: assumes x: "x < 0  1 < x" and i: "0 < i" "i < 2^Suc l" shows (l, i) x = 0"
  using x
proof
  assume "x < 0"
  also have "0  real_of_int (i - 1) / 2^(l + 1)"
    using i by (auto simp: field_simps)
  finally show ?thesis
    by (auto intro!: φ_zero simp: field_simps)
next
  have "real_of_int (i + 1) / 2^(l + 1)  1"
    using i by (subst divide_le_eq_1_pos) (auto simp del: of_int_add power_Suc)
  also assume "1 < x"
  finally show ?thesis
    by (auto intro!: φ_zero simp: field_simps)
qed

lemma ix_lt: "p  sparsegrid dm lm  d < dm  ix p d < 2^(lv p d + 1)"
  unfolding sparsegrid_def lgrid_def
  using grid_estimate[of d "start dm" p "{0 ..< dm}"] by auto

lemma ix_gt: "p  sparsegrid dm lm  d < dm  0 < ix p d"
  unfolding sparsegrid_def lgrid_def
  using grid_estimate[of d "start dm" p "{0 ..< dm}"] by auto

lemma Φ_eq_0: assumes x: "d<length p. x d < 0  1 < x d" and p: "p  sparsegrid dm lm" shows p x = 0"
  unfolding Φ_def
proof (rule prod_zero)
  from x guess d ..
  with p[THEN ix_lt, of d] p[THEN ix_gt, of d] p
  show "a{..<length p}. φ (p ! a) (x a) = 0"
    apply (cases "p!d")
    apply (intro bexI[of _ d])
    apply (auto intro!: φ_eq_0 simp: sparsegrid_length ix_def lv_def)
    done
qed simp

lemma φ_left_support':
  "x  {real_of_int (i - 1) / 2^(l + 1) .. real_of_int i / 2^(l + 1)}  φ (l,i) x = 1 + x * 2^(l + 1) - real_of_int i"
  by (auto simp: φ_def field_simps split: split_max)

lemma φ_left_support: "x  {-1 .. 0::real}  φ (l,i) ((x + real_of_int i) / 2^(l + 1)) = 1 + x"
  by (auto simp: φ_def field_simps split: split_max)

lemma φ_right_support':
  "x  {real_of_int i / 2^(l + 1) .. real_of_int (i + 1) / 2^(l + 1)}  φ (l,i) x = 1 - x * 2^(l + 1) + real_of_int i"
  by (auto simp: φ_def field_simps split: split_max)

lemma φ_right_support: 
  "x  {0 .. 1::real}  φ (l,i) ((x + real i) / 2^(l + 1)) = 1 - x"
  by (auto simp: φ_def field_simps split: split_max)

lemma integrable_φ: "integrable lborel (φ p)"
proof (induct p)
  case (Pair l i)
  have "integrable lborel (λx. indicator {real_of_int (i - 1) / 2^(l + 1) .. real_of_int (i + 1) / 2^(l + 1)} x *R φ (l, i) x)"
    unfolding φ_def by (intro borel_integrable_compact) (auto intro!: continuous_intros)
  then show ?case
    by (rule integrable_cong[THEN iffD1, rotated -1]) (auto simp: φ_zero_iff)
qed

lemma integrable_φ2: "integrable lborel (λx. φ p x * φ q x)"
proof (cases p q rule: prod.exhaust[case_product prod.exhaust])
  case (Pair_Pair l i l' i')
  have "integrable lborel
      (λx. indicator {real_of_int (i - 1) / 2^(l + 1) .. real_of_int (i + 1) / 2^(l + 1)} x *R (φ (l, i) x * φ (l', i') x))"
    unfolding φ_def by (intro borel_integrable_compact) (auto intro!: continuous_intros)
  then show ?thesis unfolding Pair_Pair
    by (rule integrable_cong[THEN iffD1, rotated -1]) (auto simp: φ_zero_iff)
qed

lemma l2_φI_DERIV:
  assumes n: " x. x  { (real_of_int i' - 1) / 2^(l' + 1) .. real_of_int i' / 2^(l' + 1) } 
    DERIV Φ_n x :> (φ (l', i') x * φ (l, i) x)" (is " x. x  {?a..?b}  DERIV _ _ :> ?P x")
    and p: " x. x  { real_of_int i' / 2^(l' + 1) .. (real_of_int i' + 1) / 2^(l' + 1) } 
    DERIV Φ_p x :> (φ (l', i') x * φ (l, i) x)" (is " x. x  {?b..?c}  _")
  shows "l2_φ (l', i') (l, i) = (Φ_n ?b - Φ_n ?a) + (Φ_p ?c - Φ_p ?b)"
proof -
  have "has_bochner_integral lborel
      (λx. ?P x * indicator {?a..?b} x + ?P x * indicator {?b..?c} x)
      ((Φ_n ?b - Φ_n ?a) + (Φ_p ?c - Φ_p ?b))"
    by (intro has_bochner_integral_add has_bochner_integral_FTC_Icc_nonneg n p)
       (auto simp: φ_nonneg field_simps)
  then have "has_bochner_integral lborel?P ((Φ_n ?b - Φ_n ?a) + (Φ_p ?c - Φ_p ?b))"
    by (rule has_bochner_integral_discrete_difference[where X="{?b}", THEN iffD1, rotated -1])
       (auto simp: power_add intro!: φ_zero integral_cong split: split_indicator)
  then show ?thesis by (simp add: has_bochner_integral_iff l2_φ_def)
qed

lemma l2_eq: "length a = length b  l2 a b = (d<length a. l2_φ (a!d) (b!d))"
  unfolding l2_def l2_φ_def Φ_def 
  apply (simp add: prod.distrib[symmetric])
proof (rule product_sigma_finite.product_integral_prod)
  show "product_sigma_finite (λd. lborel)" ..
qed (auto intro: integrable_φ2)

lemma l2_when_disjoint:
  assumes "l  l'"
  defines "d == l' - l"
  assumes "(i + 1) * 2^d < i'  i' < (i - 1) * 2^d" (is "?right  ?left")
  shows "l2_φ (l', i') (l, i) = 0"
proof -
  let ?sup = "λl i. {real_of_int (i - 1) / 2^(l + 1) <..< real_of_int (i + 1) / 2^(l + 1)}"

  have l': "l' = l + d"
    using assms by simp
  have *: "i l. 2 ^ l = real_of_int (2 ^ l::int)"
    by simp
  have [arith]: "0 < (2^d::int)"
    by simp

  from ?right  ?left l  l' have empty_support: "?sup l i  ?sup l' i' = {}"
    by (auto simp add: min_def max_def divide_simps l' power_add * of_int_mult[symmetric]
                simp del: of_int_diff of_int_add of_int_mult of_int_power)
       (simp_all add: field_simps)
  then have "x. φ (l', i') x * φ (l, i) x = 0"
    unfolding φ_zero_iff mult_eq_0_iff by blast
  then show ?thesis
    by (simp add: l2_φ_def del: mult_eq_0_iff vector_space_over_itself.scale_eq_0_iff)
qed

lemma l2_commutative: "l2_φ p q = l2_φ q p"
  by (simp add: l2_φ_def mult.commute)

lemma l2_when_same: "l2_φ (l, i) (l, i) = 1/3 / 2^l"
proof (subst l2_φI_DERIV)
  let ?l = "(2 :: real)^(l + 1)"
  let ?in = "real_of_int i - 1"
  let ?ip = "real_of_int i + 1"
  let  = (l,i)"
  let ?φ2 = "λx.  x *  x"

  { fix x assume "x  {?in / ?l .. real_of_int i / ?l}"
    hence φ_eq: " x = ?l * x  - ?in" using φ_left_support' by auto
    show "DERIV (λx. x^3 / 3 * ?l^2 + x * ?in^2 - x^2/2 * 2 * ?l * ?in) x :> ?φ2 x"
      by (auto intro!: derivative_eq_intros simp add: power2_eq_square field_simps φ_eq) }

  { fix x assume "x  {real_of_int i / ?l .. ?ip / ?l}"
    hence φ_eq: " x = ?ip - ?l * x" using φ_right_support' by auto
    show "DERIV (λx. x^3 / 3 * ?l^2 + x * ?ip^2 - x^2/2 * 2 * ?l * ?ip) x :> ?φ2 x"
      by (auto intro!: derivative_eq_intros simp add: power2_eq_square field_simps φ_eq) }
qed (simp_all add: field_simps power_eq_if[of _ 2] power_eq_if[of _ 3])

lemma l2_when_left_child:
  assumes "l < l'"
  and i'_bot: "i' > (i - 1) * 2^(l' - l)"
  and i'_top: "i' < i * 2^(l' - l)"
  shows "l2_φ (l', i') (l, i) = (1 + real_of_int i' / 2^(l' - l) - real_of_int i) / 2^(l' + 1)"
proof (subst l2_φI_DERIV)
  let ?l' = "(2 :: real)^(l' + 1)"
  let ?in' = "real_of_int i' - 1"
  let ?ip' = "real_of_int i' + 1"
  let ?l = "(2 :: real)^(l + 1)"
  let ?i = "real_of_int i - 1"
  let ?φ' = (l',i')"
  let  = (l, i)"
  let "?φ2 x" = "?φ' x *  x"
  define Φ_n where "Φ_n x = x^3 / 3 * ?l' * ?l + x * ?i * ?in' - x^2 / 2 * (?in' * ?l + ?i * ?l')" for x
  define Φ_p where "Φ_p x = x^2 / 2 * (?ip' * ?l + ?i * ?l') - x^3 / 3 * ?l' * ?l - x * ?i * ?ip'" for x

  have level_diff: "2^(l' - l) = 2^l' / (2^l :: real)" using power_diff[of "2::real" l l'] l < l' by auto

  { fix x assume x: "x  {?in' / ?l' .. ?ip' / ?l'}"
    have "?i * 2^(l' - l)  ?in'"
      using i'_bot int_less_real_le by auto
    hence "?i / ?l  ?in' / ?l'"
      using level_diff by (auto simp: field_simps)
    hence "?i / ?l  x" using x by auto
    moreover
    have "?ip'  real_of_int i * 2^(l' - l)"
      using i'_top int_less_real_le by auto
    hence ip'_le_i: "?ip' / ?l'  real_of_int i / ?l"
      using level_diff by (auto simp: field_simps)
    hence "x  real_of_int i / ?l" using x by auto
    ultimately have " x = ?l * x  - ?i" using φ_left_support' by auto
  } note φ_eq = this

  { fix x assume x: "x  {?in' / ?l' .. real_of_int i' / ?l'}"
    hence φ'_eq: "?φ' x = ?l' * x  - ?in'" using φ_left_support' by auto
    from x have x': "x  {?in' / ?l' .. ?ip' / ?l'}" by (auto simp add: field_simps)
    show "DERIV Φ_n x :> ?φ2 x" unfolding φ_eq[OF x'] φ'_eq Φ_n_def
      by (auto intro!: derivative_eq_intros simp add: power2_eq_square algebra_simps) }

  { fix x assume x: "x  {real_of_int i' / ?l' .. ?ip' / ?l'}"
    hence φ'_eq: "?φ' x = ?ip' - ?l' * x" using φ_right_support' by auto
    from x have x': "x  {?in' / ?l' .. ?ip' / ?l'}" by (simp add: field_simps)
    show "DERIV Φ_p x :> ?φ2 x" unfolding φ_eq[OF x'] φ'_eq Φ_p_def
      by (auto intro!: derivative_eq_intros simp add: power2_eq_square algebra_simps) }
qed (simp_all add: field_simps power_eq_if[of _ 2] power_eq_if[of _ 3] power_diff[of "2::real", OF _ l < l'[THEN less_imp_le]] )

lemma l2_when_right_child:
  assumes "l < l'"
  and i'_bot: "i' > i * 2^(l' - l)"
  and i'_top: "i' < (i + 1) * 2^(l' - l)"
  shows "l2_φ (l', i') (l, i) = (1 - real_of_int i' / 2^(l' - l) + real_of_int i) / 2^(l' + 1)"
proof (subst l2_φI_DERIV)
  let ?l' = "(2 :: real)^(l' + 1)"
  let ?in' = "real_of_int i' - 1"
  let ?ip' = "real_of_int i' + 1"
  let ?l = "(2 :: real)^(l + 1)"
  let ?i = "real_of_int i + 1"
  let ?φ' = (l',i')"
  let  = (l, i)"
  let ?φ2 = "λx. ?φ' x *  x"
  define Φ_n where "Φ_n x = x^2 / 2 * (?in' * ?l + ?i * ?l') - x^3 / 3 * ?l' * ?l - x * ?i * ?in'" for x
  define Φ_p where "Φ_p x = x^3 / 3 * ?l' * ?l + x * ?i * ?ip' - x^2 / 2 * (?ip' * ?l + ?i * ?l')" for x

  have level_diff: "2^(l' - l) = 2^l' / (2^l :: real)" using power_diff[of "2::real" l l'] l < l' by auto

  { fix x assume x: "x  {?in' / ?l' .. ?ip' / ?l'}"
    have "real_of_int i * 2^(l' - l)  ?in'"
      using i'_bot int_less_real_le by auto
    hence "real_of_int i / ?l  ?in' / ?l'"
      using level_diff by (auto simp: field_simps)
    hence "real_of_int i / ?l  x" using x by auto
    moreover
    have "?ip'  ?i * 2^(l' - l)"
      using i'_top int_less_real_le by auto
    hence ip'_le_i: "?ip' / ?l'  ?i / ?l"
      using level_diff by (auto simp: field_simps)
    hence "x  ?i / ?l" using x by auto
    ultimately have " x = ?i - ?l * x" using φ_right_support' by auto
  } note φ_eq = this

  { fix x assume x: "x  {?in' / ?l' .. real_of_int i' / ?l'}"
    hence φ'_eq: "?φ' x = ?l' * x  - ?in'" using φ_left_support' by auto

    from x have x': "x  {?in' / ?l' .. ?ip' / ?l'}" by (simp add: field_simps)
    show "DERIV Φ_n x :> ?φ2 x" unfolding Φ_n_def φ_eq[OF x'] φ'_eq
      by (auto intro!: derivative_eq_intros simp add: simp add: power2_eq_square algebra_simps) }

  { fix x assume x: "x  {real_of_int i' / ?l' .. ?ip' / ?l'}"
    hence φ'_eq: "?φ' x = ?ip' - ?l' * x" using φ_right_support' by auto
    from x have x': "x  {?in' / ?l' .. ?ip' / ?l'}" by (auto simp: field_simps)
    show "DERIV Φ_p x :> ?φ2 x" unfolding φ_eq[OF x'] φ'_eq Φ_p_def
      by (auto intro!: derivative_eq_intros simp add: power2_eq_square algebra_simps) }
qed (simp_all add: field_simps power_eq_if[of _ 2] power_eq_if[of _ 3] power_diff[of "2::real", OF _ l < l'[THEN less_imp_le]] )

lemma level_shift: "lc > l  (x :: real) / 2 ^ (lc - Suc l) = x * 2 / 2 ^ (lc - l)"
  by (auto simp add: power_diff)

lemma l2_child: assumes "d < length b"
  and p_grid: "p  grid (child b dir d) ds" (is "p  grid ?child ds")
  shows "l2_φ (p ! d) (b ! d) = (1 - real_of_int (sgn dir) * (real_of_int (ix p d) / 2^(lv p d - lv b d) - real_of_int (ix b d))) /
                                 2^(lv p d + 1)"
proof -
  have "lv ?child d  lv p d" using d < length b and p_grid
    using grid_single_level by auto
  hence "lv b d < lv p d" using d < length b and p_grid
    using child_lv by auto

  let ?i_c = "ix ?child d" and ?l_c = "lv ?child d"
  let ?i_p = "ix p d" and ?l_p = "lv p d"
  let ?i_b = "ix b d" and ?l_b = "lv b d"

  have "(2::int) * 2^(?l_p - ?l_c) = 2^Suc (?l_p - ?l_c)" by auto
  also have " = 2^(Suc ?l_p - ?l_c)"
  proof -
    have "Suc (?l_p - ?l_c) = Suc ?l_p - ?l_c"
      using ‹lv ?child d  lv p d by auto
    thus ?thesis by auto
  qed
  also have " = 2^(?l_p - ?l_b)"
    using d < length b and ‹lv b d < lv p d
    by (auto simp add: child_def lv_def)
  finally have level: "2^(?l_p - ?l_b) = (2::int) * 2^(?l_p - ?l_c)" ..

  from d < length b and p_grid
  have range_left: "?i_p > (?i_c - 1) * 2^(?l_p - ?l_c)" and
       range_right: "?i_p < (?i_c + 1) * 2^(?l_p - ?l_c)"
    using grid_estimate by auto

  show ?thesis
  proof (cases dir)
    case left
    with child_ix_left[OF d < length b]
    have "(?i_b - 1) * 2^(?l_p - ?l_b) = (?i_c - 1) * 2^(?l_p - ?l_c)" and
      "?i_b * 2^(?l_p - ?l_b) = (?i_c + 1) * 2^(?l_p - ?l_c)" using level by auto
    hence "?i_p > (?i_b - 1) * 2^(?l_p - ?l_b)" and
      "?i_p < ?i_b * 2^(?l_p - ?l_b)"
      using range_left and range_right by auto
    with ?l_b < ?l_p
    have "l2_φ (?l_p, ?i_p) (?l_b, ?i_b) =
          (1 + real_of_int ?i_p / 2^(?l_p - ?l_b) - real_of_int ?i_b) / 2^(?l_p + 1)"
      by (rule l2_when_left_child)
    thus ?thesis using left by (auto simp add: ix_def lv_def)
  next
    case right
    hence "?i_c = 2 * ?i_b + 1" using child_ix_right and d < length b by auto
    hence "?i_b * 2^(?l_p - ?l_b) = (?i_c - 1) * 2^(?l_p - ?l_c)" and
      "(?i_b + 1) * 2^(?l_p - ?l_b) = (?i_c + 1) * 2^(?l_p - ?l_c)" using level by auto
    hence "?i_p > ?i_b * 2^(?l_p - ?l_b)" and
      "?i_p < (?i_b + 1) * 2^(?l_p - ?l_b)"
      using range_left and range_right by auto
    with ?l_b < ?l_p
    have "l2_φ (?l_p, ?i_p) (?l_b, ?i_b) =
          (1 - real_of_int ?i_p / 2^(?l_p - ?l_b) + real_of_int ?i_b) / 2^(?l_p + 1)"
      by (rule l2_when_right_child)
    thus ?thesis using right by (auto simp add: ix_def lv_def)
  qed
qed

lemma l2_same: "l2_φ (p!d) (p!d) = 1/3 / 2^(lv p d)"
proof -
  have "l2_φ (p!d) (p!d) = l2_φ (lv p d, ix p d) (lv p d, ix p d)"
    by (auto simp add: lv_def ix_def)
  thus ?thesis using l2_when_same by auto
qed

lemma l2_disjoint: assumes "d < length b" and "p  grid b {d}" and "p'  grid b {d}"
  and "p'  grid p {d}" and "lv p' d  lv p d"
  shows "l2_φ (p' ! d) (p ! d) = 0"
proof -
  have range: "ix p' d > (ix p d + 1) * 2^(lv p' d - lv p d)  ix p' d < (ix p d - 1) * 2^(lv p' d - lv p d)"
  proof (rule ccontr)
    assume "¬ ?thesis"
    hence "ix p' d  (ix p d + 1) * 2^(lv p' d - lv p d)" and "ix p' d  (ix p d - 1) * 2^(lv p' d - lv p d)" by auto
    with p'  grid b {d} and p  grid b {d} and ‹lv p' d  lv p d and d < length b
    have "p'  grid p {d}" using grid_part[where p=p and b=b and d=d and p'=p'] by auto
    with p'  grid p {d} show False by auto
  qed

  have "l2_φ (p' ! d) (p ! d) = l2_φ (lv p' d, ix p' d) (lv p d, ix p d)" by (auto simp add: ix_def lv_def)
  also have " = 0" using range and ‹lv p' d  lv p d and l2_when_disjoint by auto
  finally show ?thesis .
qed

lemma l2_down2:
  fixes pc pd p
  assumes "d < length pd"
  assumes pc_in_grid: "pc  grid (child pd dir d) {d}"
  assumes pd_is_child: "pd = child p dir d" (is "pd = ?pd")
  shows "l2_φ (pc ! d) (pd ! d) / 2 = l2_φ (pc ! d) (p ! d)"
proof -
  have "d < length p" using pd_is_child d < length pd by auto

  moreover
  have "pc  grid ?pd {d}" using pd_is_child and grid_child and pc_in_grid by auto
  hence "lv p d < lv pc d" using grid_child_level and d < length pd and pd_is_child by auto

  moreover
  have "real_of_int (sgn dir) * real_of_int (sgn dir) = 1" by (cases dir, auto)

  ultimately show ?thesis
    unfolding l2_child[OF d < length pd pc_in_grid]
              l2_child[OF d < length p pc  grid ?pd {d}]
    using child_lv and child_ix and pd_is_child and level_shift
    by (auto simp add: algebra_simps diff_divide_distrib add_divide_distrib)
qed

lemma l2_zigzag:
  assumes "d < length p" and p_child: "p = child p_p dir d"
  and p'_grid: "p'  grid (child p (inv dir) d) {d}"
  and ps_intro: "child p (inv dir) d = child ps dir d" (is "?c_p = ?c_ps")
  shows "l2_φ (p' ! d) (p_p ! d) = l2_φ (p' ! d) (ps ! d) + l2_φ (p' ! d) (p ! d) / 2"
proof -
  have "length p = length ?c_p" by auto
  also have " = length ?c_ps" using ps_intro by auto
  finally have "length p = length ps" using ps_intro by auto
  hence "d < length p_p" using p_child and d < length p by auto

  moreover
  from ps_intro have "ps = p[d := (lv p d, ix p d - sgn dir)]" by (rule child_neighbour)
  hence "lv ps d = lv p d" and "real_of_int (ix ps d) = real_of_int (ix p d) - real_of_int (sgn dir)"
    using lv_def and ix_def and ‹length p = length ps and d < length p by auto

  moreover
  have "d < length ps" and *: "p'  grid (child ps dir d) {d}"
    using p'_grid ps_intro ‹length p = length ps d < length p by auto

  have "p'  grid p {d}" using p'_grid and grid_child by auto
  hence p_p_grid: "p'  grid (child p_p dir d) {d}" using p_child by auto
  hence "lv p' d > lv p_p d" using grid_child_level and d < length p_p by auto

  moreover
  have "real_of_int (sgn dir) * real_of_int (sgn dir) = 1" by (cases dir, auto)

  ultimately show ?thesis
    unfolding l2_child[OF d < length p p'_grid] l2_child[OF d < length ps *]
              l2_child[OF d < length p_p p_p_grid]
    using child_lv and child_ix and p_child level_shift
    by (auto simp add: add_divide_distrib algebra_simps diff_divide_distrib)
qed

end

Theory UpDown_Scheme

section ‹ UpDown Scheme ›

theory UpDown_Scheme
  imports Grid
begin

fun down' :: "nat  nat  grid_point  real  real  vector  vector"
where
  "down' d 0       p fl fr α = α"
| "down' d (Suc l) p fl fr α = (let
      fm = (fl + fr) / 2 + (α p);
      α = α(p := ((fl + fr) / 4 + (1 / 3) * (α p)) / 2 ^ (lv p d));
      α = down' d l (child p left d) fl fm α;
      α = down' d l (child p right d) fm fr α
    in α)"

definition down :: "nat  nat  nat  vector  vector" where
  "down = lift (λ d l p. down' d l p 0 0)"

fun up' :: "nat  nat  grid_point  vector  (real * real) * vector" where
  "up' d       0 p α = ((0, 0), α)"
| "up' d (Suc l) p α = (let
      ((fl, fml), α) = up' d l (child p left d) α;
      ((fmr, fr), α) = up' d l (child p right d) α;
      result = (fml + fmr + (α p) / 2 ^ (lv p d) / 2) / 2
    in ((fl + result, fr + result), α(p := fml + fmr)))"


definition up :: "nat  nat  nat  vector  vector" where
  "up = lift (λ d lm p α. snd (up' d lm p α))"

fun updown' :: "nat  nat  nat  vector  vector" where
  "updown' dm lm 0 α = α"
| "updown' dm lm (Suc d) α =
    (sum_vector (updown' dm lm d (up dm lm d α)) (down dm lm d (updown' dm lm d α)))"

definition updown :: "nat  nat  vector  vector" where
  "updown dm lm α = updown' dm lm dm α"

end

Theory Up

section ‹ Up Part ›

theory Up
imports UpDown_Scheme Triangular_Function
begin

lemma up'_inplace:
  assumes p'_in: "p'  grid p ds" and "d  ds"
  shows "snd (up' d l p α) p' = α p'"
  using p'_in
proof (induct l arbitrary: p α)
  case (Suc l)
  let "?ch dir" = "child p dir d"
  let "?up dir α" = "up' d l (?ch dir) α"
  let "?upl" = "snd (?up left α)"

  from contrapos_nn[OF p'  grid p ds grid_child[OF d  ds]]
  have left: "p'  grid (?ch left) ds" and
       right: "p'  grid (?ch right) ds" by auto

  have "p  p'" using grid.Start Suc.prems by auto
  with Suc.hyps[OF left, of α] Suc.hyps[OF right, of ?upl]
  show ?case
    by (cases "?up left α", cases "?up right ?upl", auto simp add: Let_def)
qed auto

lemma up'_fl_fr:
      " d < length p ; p = (child p_r right d) ; p = (child p_l left d) 
        fst (up' d lm p α) =
              ( p'  lgrid p {d} (lm + level p). (α p') * l2_φ (p' ! d) (p_r ! d),
                p'  lgrid p {d} (lm + level p). (α p') * l2_φ (p' ! d) (p_l ! d))"
proof (induct lm arbitrary: p p_l p_r α)
  case (Suc lm)
  note d < length p[simp]

  from child_ex_neighbour
  obtain pc_r pc_l
    where pc_r_def: "child p right d = child pc_r (inv right) d"
    and pc_l_def: "child p left d = child pc_l (inv left) d" by blast

  define pc where "pc dir = (case dir of right  pc_r | left  pc_l)" for dir
  { fix dir have "child p (inv dir) d = child (pc (inv dir)) dir d"
      by (cases dir, auto simp add: pc_def pc_r_def pc_l_def) } note pc_child = this
  { fix dir have "child p dir d = child (pc dir) (inv dir) d"
      by (cases dir, auto simp add: pc_def pc_r_def pc_l_def) } note pc_child_inv = this
  hence "!! dir. length (child p dir d) = length (child (pc dir) (inv dir) d)" by auto
  hence "!! dir. length p = length (pc dir)" by auto
  hence [simp]: "!! dir. d < length (pc dir)" by auto

  let ?l = "λs. lm + level s"
  let ?C = "λp p'. (α p) * l2_φ (p ! d) (p' ! d)"
  let ?sum' = "λs p''.  p'  lgrid s {d} (Suc lm + level p). ?C p' p''"
  let ?sum = "λs dir p.  p'  lgrid (child s dir d) {d} (?l (child s dir d)). ?C p' p"
  let ?ch = "λdir. child p dir d"
  let ?f = "λdir. ?sum p dir (pc dir)"
  let ?fm = "λdir. ?sum p dir p"
  let ?result = "(?fm left + ?fm right + (α p) / 2 ^ (lv p d) / 2) / 2"
  let ?up = "λlm p α. up' d lm p α"

  define βl where "βl = snd (?up lm (?ch left) α)"
  define βr where "βr = snd (?up lm (?ch right) βl)"

  define p_d where "p_d dir = (case dir of right  p_r | left  p_l)" for dir
  have p_d_child: "p = child (p_d dir) dir d" for dir
    using Suc.prems p_d_def by (cases dir) auto
  hence " dir. length p = length (child (p_d dir) dir d)" by auto
  hence " dir. d < length (p_d dir)" by auto

  { fix dir

    { fix p' assume "p'  lgrid (?ch (inv dir)) {d} (?l (?ch (inv dir))) "
      hence "?C p' (pc (inv dir)) + (?C p' p) / 2 = ?C p' (p_d dir)"
        using l2_zigzag[OF _ p_d_child[of dir] _ pc_child[of dir]]
        by (cases dir) (auto simp add: algebra_simps) }
    hence inv_dir_sum: "?sum p (inv dir) (pc (inv dir)) + (?sum p (inv dir) p) / 2
      = ?sum p (inv dir) (p_d dir)"
      by (auto simp add: sum.distrib[symmetric] sum_divide_distrib)

    have "?sum p dir p / 2 = ?sum p dir (p_d dir)"
      using l2_down2[OF _ _ p = child (p_d dir) dir d]
      by (force intro!: sum.cong simp add: sum_divide_distrib)
    moreover
    have "?C p (p_d dir) = (α p) / 2 ^ (lv p d) / 4"
      using l2_child[OF d < length (p_d dir), of p dir "{d}"] p_d_child[of dir]
      d < length (p_d dir) child_lv child_ix grid.Start[of p "{d}"]
      by (cases dir) (auto simp add: add_divide_distrib field_simps)
    ultimately
    have "?sum' p (p_d dir) =
      ?sum p (inv dir) (pc (inv dir)) +
      (?sum p (inv dir) p) / 2 + ?sum p dir p / 2 + (α p) / 2 ^ (lv p d) / 4"
      using lgrid_sum[where b=p] and child_level and inv_dir_sum
      by (cases dir) auto
    hence "?sum p (inv dir) (pc (inv dir)) + ?result = ?sum' p (p_d dir)"
      by (cases dir) auto }
  note this[of left] this[of right]
  moreover
  note eq = up'_inplace[OF grid_not_child[OF d < length p], of d "{d}" lm]
  { fix p' assume "p'  lgrid (?ch right) {d} (lm + level (?ch right))"
    with grid_disjunct[of d p] up'_inplace[of p' "?ch left" "{d}" d lm α] βl_def
    have "βl p' = α p'" by auto }
  hence "fst (?up (Suc lm) p α) = (?f left + ?result, ?f right + ?result)"
    using βl_def pc_child_inv[of left] pc_child_inv[of right]
      Suc.hyps[of "?ch left" "pc left" p α] eq[of left α]
      Suc.hyps[of "?ch right" p "pc right" βl] eq[of right βl]
    by (cases "?up lm (?ch left) α", cases "?up lm (?ch right) βl") (simp add: Let_def)
  ultimately show ?case by (auto simp add: p_d_def)
next
  case 0
  show ?case by simp
qed

lemma up'_β:
  " d < length b ; l + level b = lm ; b  sparsegrid' dm ; p  sparsegrid' dm 
   
   (snd (up' d l b α)) p =
     (if p  lgrid b {d} lm
      then  p'  (lgrid p {d} lm) - {p}. α p' * l2_φ (p' ! d) (p ! d)
      else α p)"
  (is " _ ; _ ; _ ; _   (?goal l b p α)")
proof (induct l arbitrary: b p α)
  case (Suc l)

  let ?l = "child b left d" and ?r = "child b right d"
  obtain p_l where p_l_def: "?r = child p_l left d" using child_ex_neighbour[where dir=right] by auto
  obtain p_r where p_r_def: "?l = child p_r right d" using child_ex_neighbour[where dir=left] by auto

  let ?ul = "up' d l ?l α"
  let ?ur = "up' d l ?r (snd ?ul)"

  let "?C p'" = "α p' * l2_φ (p' ! d) (p ! d)"
  let "?s s" = " p'  (lgrid s {d} lm). ?C p'"

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

  { fix p' assume "p'  grid ?r {d}"
    hence "p'  grid ?l {d}"
      using grid_disjunct[OF d < length b] by auto
    hence "snd ?ul p' = α p'" using up'_inplace by auto
  } note eq = this

  show "?goal (Suc l) b p α"
  proof (cases "p = b")
    case True

    let "?C p'" = "α p' * l2_φ (p' ! d) (b ! d)"
    let "?s s" = " p'  (lgrid s {d} lm). ?C p'"

    have "d < length ?l" using d < length b by auto
    from up'_fl_fr[OF this p_r_def]
    have fml: "snd (fst ?ul) = ( p'  lgrid ?l {d} (l + level ?l). ?C p')" by simp

    have "d < length ?r" using d < length b by auto
    from up'_fl_fr[OF this _ p_l_def, where α="snd ?ul"]
    have fmr: "fst (fst ?ur) = ( p'  lgrid ?r {d} (l + level ?r).
                                ((snd ?ul) p') * l2_φ (p' ! d) (b ! d))" by simp

    have "level b < lm" using ‹Suc l + level b = lm by auto
    hence "{ b }  lgrid b {d} lm" unfolding lgrid_def by auto
    from sum_diff[OF lgrid_finite this]
    have "( p'  (lgrid b {d} lm) - {b}. ?C p') = ?s b - ?C b" by simp
    also have " = ?s ?l + ?s ?r"
      using lgrid_sum and ‹level b < lm and d < length b by auto
    also have " = snd (fst ?ul) + fst (fst ?ur)" using fml and fmr
      and ‹Suc l + level b = lm and child_level[OF d < length b]
      using eq unfolding True lgrid_def by auto

    finally show ?thesis unfolding up'.simps Let_def and fun_upd_def lgrid_def
      using p = b and ‹level b < lm
      by (cases ?ul, cases ?ur, auto)
  next
    case False

    have "?r  sparsegrid' dm" and "?l  sparsegrid' dm"
      using b  sparsegrid' dm and d < dm unfolding sparsegrid'_def by auto
    from Suc.hyps[OF _ _ this(1)] Suc.hyps[OF _ _ this(2)]
    have "?goal l ?l p α" and "?goal l ?r p (snd ?ul)"
      using d < length b and ‹Suc l + level b = lm and p  sparsegrid' dm by auto

    show ?thesis
    proof (cases "p  lgrid b {d} lm")
      case True
      hence "level p < lm" and "p  grid b {d}" unfolding lgrid_def by auto
      hence "p  grid ?l {d}  p  grid ?r {d}"
        unfolding grid_partition[of b] using p  b by auto
      thus ?thesis
      proof (rule disjE)
        assume "p  grid (child b left d) {d}"
        hence "p  grid (child b right d) {d}"
          using grid_disjunct[OF d < length b] by auto
        thus ?thesis
          using ?goal l ?l p α and ?goal l ?r p (snd ?ul)
          using p  b p  lgrid b {d} lm
          unfolding lgrid_def grid_partition[of b]
          by (cases ?ul, cases ?ur, auto simp add: Let_def)
      next
        assume *: "p  grid (child b right d) {d}"
        hence "p  grid (child b left d) {d}"
          using grid_disjunct[OF d < length b] by auto
        moreover
        { fix p' assume "p'  grid p {d}"
          from grid_transitive[OF this *] eq[of p']
          have "snd ?ul p' = α p'" by simp
        }
        ultimately show ?thesis
          using ?goal l ?l p α and ?goal l ?r p (snd ?ul)
          using p  b p  lgrid b {d} lm *
          unfolding lgrid_def
          by (cases ?ul, cases ?ur, auto simp add: Let_def)
  qed
next
      case False
      then have "p  lgrid ?l {d} lm" and "p  lgrid ?r {d} lm"
        unfolding lgrid_def and grid_partition[where p=b] by auto
      with False show ?thesis using ?goal l ?l p α and ?goal l ?r p (snd ?ul)
        using p  b p  lgrid b {d} lm
        unfolding lgrid_def
        by (cases ?ul, cases ?ur, auto simp add: Let_def)
    qed
  qed
next
  case 0
  then have "lgrid b {d} lm = {}"
    using lgrid_empty'[where p=b and lm=lm and ds="{d}"] by auto
  with 0 show ?case unfolding up'.simps by auto
qed

lemma up:
  assumes "d < dm" and "p  sparsegrid dm lm"
  shows "(up dm lm d α) p = ( p'  (lgrid p {d} lm) - {p}. α p' * l2_φ (p' ! d) (p ! d))"
proof -
  let ?S = "λ x p p'. if p'  grid p {d} - {p} then x * l2_φ (p'!d) (p!d) else 0"
  let ?F = "λ d lm p α. snd (up' d lm p α)"

  { fix p b assume "p  grid b {d}"
    from grid_transitive[OF _ this subset_refl subset_refl]
    have "lgrid b {d} lm  (grid p {d} - {p}) = lgrid p {d} lm - {p}"
      unfolding lgrid_def by auto
  } note lgrid_eq = this

  { fix l b p α
    assume b: "b  lgrid (start dm) ({0..<dm} - {d}) lm"
    hence "b  sparsegrid' dm" and "d < length b" using sparsegrid'_start d < dm by auto
    assume l: "l + level b = lm" and p: "p  sparsegrid dm lm"
    note sparsegridE[OF p]

    note up' = up'_β[OF d < length b l b  sparsegrid' dm p  sparsegrid' dm]

    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 with baseE(2)[OF p  sparsegrid' dm] ‹level p < lm
      have "p  lgrid b {d} lm" and "p  grid b {d}" by auto
      show ?thesis
        using lgrid_eq[OF p  grid b {d}]
        unfolding up' if_P[OF True] if_P[OF p  lgrid b {d} lm]
        by (intro sum.mono_neutral_cong_left lgrid_finite) auto
    next
      case False
      moreover have "p  lgrid b {d} lm"
      proof (rule ccontr)
        assume "¬ ?thesis"
        hence "base {d} p = b" using b by (auto intro!: baseI)
        thus False using False by auto
      qed
      ultimately show ?thesis unfolding up' by auto
    qed }
  with lift[where F = ?F, OF d < dm p  sparsegrid dm lm]
  have lift_eq: "lift ?F dm lm d α p =
         (p'lgrid (base {d} p) {d} lm. ?S (α p') p p')" by auto
  from lgrid_eq[OF baseE(2)[OF sparsegrid_subset[OF p  sparsegrid dm lm]]]
  show ?thesis
    unfolding up_def lift_eq by (intro sum.mono_neutral_cong_right lgrid_finite) auto
qed

end

Theory Down

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

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"