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