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