# Theory Triangular_Function

theory Triangular_Function
imports Equivalence_Lebesgue_Henstock_Integration Grid
```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)
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
```