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 obtain d where "d < length p ∧ (x d < 0 ∨ 1 < x 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 Bochner_Integration.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 Bochner_Integration.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