Theory CLMM_Misc

theory CLMM_Misc imports "HOL-Analysis.Analysis"


(* Author: Mnacho Echenim. Grenoble INP - UGA, Kaiko *)
(* This research is part of the ANR project BlockFI - 2024-CES38 *)

begin
section ‹Preliminary definitions and results›

subsection ‹Misc›


lemma diff_min_le:
  assumes "(a::real) ≤ b"
and "x ≤ y"
shows "min x b - min x a ≤ min y b - min y a"
  using assms by linarith

lemma sum_ex_strict_pos: 
fixes f g :: "'i ⇒ 'a::ordered_cancel_comm_monoid_add"
  assumes "finite A"
    and "∀x∈A. 0 ≤ f x"
    and "∃a∈A. 0 < f a"
  shows "0 < sum f A"
proof -
  obtain a where "0 < f a" and "a∈ A" using assms by auto note aprop = this
  define B where "B = A - {a}"
  hence "A = insert a B" using aprop by auto
  have "0 < f a" using aprop by simp
  also have "... ≤ f a + sum f B"
  proof -
    have "0 ≤ sum f B"
    proof (rule sum_nonneg)
      fix x
      assume "x∈ B"
      thus "0 ≤ f x" using B_def assms by simp
    qed
    thus ?thesis by (simp add: add_increasing2) 
  qed
  also have "... = sum f (insert a B)"
  proof (rule sum.insert[symmetric])
    show "finite B" using assms B_def by simp
    show "a∉ B" using B_def by simp
  qed
  also have "... = sum f A" using ‹A = insert a B› by simp
  finally show ?thesis .
qed

lemma diff_inv_max_le:
  assumes "0 < a"
  and "(a::real) ≤ b"
  and "x ≤ y"
shows "inverse (max y a) - inverse (max y b) ≤ 
  inverse (max x a) - inverse (max x b)"
proof (cases "b ≤ y")
  case True
  thus ?thesis using assms by auto
next
  case False
  hence "max y b = b" by simp
  have "max x b = b" using False assms by auto
  show ?thesis using ‹max y b = b› assms by fastforce 
qed

lemma int_interval_insert:
  fixes a::int
  assumes "a ≤ b"
  shows "{a..< (b+1)} = insert b {a..< b}"
proof
  show "{a..<b + 1} ⊆ insert b {a..<b}"
  proof
    fix x
    assume "x ∈ {a..<b + 1}"
    show "x ∈ insert b {a..<b}"
    proof (cases "x = b")
      case True
      then show ?thesis by simp
    next
      case False
      hence "x < b" using ‹x ∈ {a..<b + 1}› by simp
      then show ?thesis using ‹x ∈ {a..<b + 1}› by simp
    qed
  qed
next
  show "insert b {a..<b} ⊆ {a..<b + 1}" by (simp add: assms)
qed

lemma int_telescoping_sum:
  fixes f::"int ⇒ 'a::ab_group_add"
  assumes "a ≤ b"
  shows "(∑i ∈{a..<b}. (f i - f (i+1))) = f a - (f b)" using ‹a ≤ b›
proof (induct rule: int_ge_induct )
  case base
  then show ?case by simp
next
  case (step i)
  have "{a..<i + 1} = insert i {a..<i}" 
    using int_interval_insert ‹a ≤ i› by simp
  hence "(∑i ∈ {a..<i + 1}. f i - f (i + 1)) = 
    (∑i ∈ (insert i {a..<i}). f i - f (i + 1))" by simp
  also have "... = f i - f (i+1) + (∑i = a..<i. f i - f (i + 1))" 
    by (rule sum.insert, auto)
  also have "... = f i - f (i+1) + f a - f i" using step by simp
  also have "... = f a - f (i+1)" by simp
  finally show ?case .
qed

lemma int_telescoping_sum':
  fixes f::"int ⇒ 'a::ab_group_add"
  assumes "a ≤ b"
  shows "(∑i ∈{a..<b}. (f (i+1) - f i)) = f b - (f a)"
proof -
  define g where "g = (λx. - f x)"
  have "(∑i ∈{a..<b}. (f (i+1) - f i)) = (∑i ∈{a..<b}. (g i - g (i+1)))"
    by (rule sum.cong, auto simp add: g_def)
  also have "... = g a - g b" using assms int_telescoping_sum[of a b] by simp
  also have "... = f b - f a" using g_def by simp
  finally show ?thesis .
qed

lemma int_telescoping_sum_le':
  fixes f::"int ⇒ 'a::ab_group_add"
  assumes "a ≤ b"
  shows "(∑i ∈{a..b}. (f (i+1) - f i)) = f (b+1) - (f a)"
proof -
  have "{a..b} = {a..< b+1}" by auto
  thus ?thesis using assms int_telescoping_sum'[of a "b+1"] by simp
qed

lemma diff_sum_dcomp:
  fixes f::"'a ⇒ real"
  assumes "finite A"
  and "A = B ∪ C"
  and "B ∩ C = {}"  
shows "x + sum f A - (y + sum f B) = x + sum f C - y"
proof -
  have "sum f A = sum f (B ∪ C)" using assms by simp
  also have "... = sum f B + sum f C" 
  proof (rule sum.union_inter_neutral)
    show "finite B" using assms by simp
    show "finite C" using assms by simp
    show "∀x∈B ∩ C. f x = 0" using assms by simp
  qed
  finally have "sum f A = sum f B + sum f C" .
  thus ?thesis by simp
qed

lemma sum_remove_el:
  assumes "finite A"
  and "x∈ A"
  and "B = A - {x}"
  shows "sum f A = f x + sum f B"
proof -
  have "A = insert x B" using assms by auto
  hence "sum f A = sum f (insert x B)" by simp
  also have "... = f x + sum f B"
  proof (rule sum.insert)
    show "finite B" using assms by simp
    show "x∉ B" using assms by simp
  qed
  finally show ?thesis .
qed

lemma int_set_bdd_above:
  fixes X::"int set"
  assumes "X ≠ {}"
    and "bdd_above X"
  shows "Sup X ∈ X" "∀x ∈ X. x ≤ Sup X"
proof -
  from assms obtain x y where "x ∈ X" and "X ⊆ {..y}"
    by (auto simp: bdd_above_def)
  hence *: "finite (X ∩ {x..y})" "X ∩ {x..y} ≠ {}" and "x ≤ y"
    by (auto simp: subset_eq)
  have "∃!x∈X. (∀y∈X. y ≤ x)"
  proof
    { fix z assume "z ∈ X"
      have "z ≤ Max (X ∩ {x..y})"
      proof cases
        assume "x ≤ z" with ‹z ∈ X› ‹X ⊆ {..y}› *(1) show ?thesis
          by (auto intro!: Max_ge)
      next
        assume "¬ x ≤ z"
        then have "z < x" by simp
        also have "x ≤ Max (X ∩ {x..y})"
          using ‹x ∈ X› *(1) ‹x ≤ y› by (intro Max_ge) auto
        finally show ?thesis by simp
      qed }
    note le = this
    with Max_in[OF *] show 
        ex: "Max (X ∩ {x..y}) ∈ X ∧ (∀z∈X. z ≤ Max (X ∩ {x..y}))" 
      by auto    
      fix z assume *: "z ∈ X ∧ (∀y∈X. y ≤ z)"
      with le have "z ≤ Max (X ∩ {x..y})"
        by auto
      moreover have "Max (X ∩ {x..y}) ≤ z"
        using * ex by auto
      ultimately show "z = Max (X ∩ {x..y})"
        by auto
    qed
    hence "Sup X ∈ X ∧ (∀y∈X. y ≤ Sup X)"
    unfolding Sup_int_def by (rule theI')
  thus "Sup X ∈ X" "∀x ∈ X. x ≤ Sup X" by auto
qed

definition wedge where
"wedge f (i::int) sqp = (λn. if n ≤ i then f n else f (n-1))(i+1:=sqp)"

lemma wedge_arg_lt[simp]:
  assumes "n ≤ i"
  shows "wedge f i sqp n = f n" using assms unfolding wedge_def by simp

lemma wedge_arg_gt[simp]:
  assumes "i+1 < n"
  shows "wedge f i sqp n = f (n-1)" using assms unfolding wedge_def by simp

lemma wedge_arg_eq[simp]:
  shows "wedge f i sqp (i+1) = sqp" unfolding wedge_def by simp

lemma wedge_strict_mono:
  assumes "strict_mono f"
  and "f i < sqp"
  and "sqp < f (i+1)"
  and "g = wedge f i sqp"
shows "strict_mono g" unfolding strict_mono_def
proof (intro allI impI)
  fix x y
  assume "(x::int) < y"
  show "g x < g y" 
  proof (cases "y < i+1")
    case True
    then show ?thesis
      using ‹x < y› assms strict_mono_less by fastforce
  next
    case False
    show ?thesis
    proof (cases "y = i+1")
      case True
      hence "wedge f i sqp y = sqp" by simp
      have "x ≤ i" using True ‹x < y› by simp
      hence "wedge f i sqp x = f x" by simp
      then show ?thesis using ‹wedge f i sqp y = sqp› assms
        by (metis ‹x ≤ i› monoE order_le_less_trans strict_mono_mono)
    next
      case False
      hence "i+1 < y" using ‹¬ y < i+1› by simp
      hence "wedge f i sqp y = f (y - 1)" by simp
      show ?thesis
      proof (cases "x = i+1")
        case True
        then show ?thesis
          by (metis (mono_tags, lifting) ‹wedge f i sqp y = f (y - 1)› 
              ‹x < y› assms(1) assms(3) assms(4) monoD order_less_le_subst1 
              strict_mono_on_imp_mono_on wedge_arg_eq zle_diff1_eq) 
      next
        case False
        then show ?thesis
          by (metis ‹i + 1 < y› ‹x < y› assms(1) assms(4) diff_strict_right_mono 
              linorder_le_less_linear order_le_imp_less_or_eq strict_monoD 
              wedge_arg_gt wedge_arg_lt zle_diff1_eq zless_imp_add1_zle) 
      qed
    qed
  qed
qed

lemma wedge_gt:
  assumes "∀i. x < f i"
  and "x < sqp"
  shows "∀i. x < wedge f j sqp i"
  by (smt (verit) assms wedge_arg_eq wedge_arg_gt wedge_arg_lt)

lemma wedge_ge:
  assumes "∀i. x ≤ f i"
  and "x ≤ sqp"
  shows "∀i. x ≤ wedge f j sqp i"
  by (smt (verit) assms wedge_arg_eq wedge_arg_gt wedge_arg_lt)

lemma wedge_lt:
  assumes "∀i. f i < x"
  and "sqp < x"
  shows "∀i. wedge f j sqp i < x"
  by (smt (verit) assms wedge_arg_eq wedge_arg_gt wedge_arg_lt)

lemma wedge_le:
  assumes "∀i. f i ≤ x"
  and "sqp ≤ x"
  shows "∀i. wedge f j sqp i ≤ x"
  by (smt (verit) assms wedge_arg_eq wedge_arg_gt wedge_arg_lt)

lemma wedge_images:
  shows "∀j. ∃k. f j = wedge f i sqp k"
proof
  fix j
  show "∃k. f j = wedge f i sqp k"
  proof (cases "j ≤ i")
    case True
    hence "wedge f i sqp j = f j" by simp
    then show ?thesis by metis
  next
    case False
    hence "i+1 ≤ j" by simp
    hence "wedge f i sqp (j+1) = f j" by simp
    then show ?thesis by metis
  qed
qed

lemma wedge_images':
  assumes "A = {j. j ≤ i}"
  and "B = {j. i+1 < j}" 
shows "wedge f i sqp k ∈ f`A ∪ (f`((λi. i-1)`B)) ∪ {sqp}"
proof (cases "k ≤ i")
  case True
  hence "wedge f i sqp k = f k" by simp
  hence "wedge f i sqp k ∈ f`A" using assms True by simp
  then show ?thesis by simp 
next
  case False
  show ?thesis 
  proof (cases "k = i+1")
    case True
    then show ?thesis by simp
  next
    case False
    hence "i+1 < k" using ‹¬ k ≤ i› by simp
    then show ?thesis by (simp add: ‹i + 1 < k› assms(2))
  qed
qed

lemma wedge_as_ubound:
  assumes "∀(r::real). ∃(i::int). r < f i"
  shows "∀r. ∃k. r < wedge f i sqp k" using assms 
  by (metis wedge_images) 

lemma wedge_as_lbound:
  assumes "∀(r::real) > 0. ∃(i::int). f i < r"
  shows "∀r > 0. ∃k. wedge f i sqp k < r" using assms 
  by (metis wedge_images) 

lemma wedge_arg_prop:
  shows "{j. P (wedge f i sqp j)} ⊆ {j. j ≤ i ∧ P (f j)} ∪ 
    {j. i+1 < j ∧ P (f (j-1))} ∪ {i+1}"
proof
  fix j
  assume "j∈ {j. P (wedge f i sqp j)}"
  hence pr: "P (wedge f i sqp j)" by auto
  show "j ∈ {j. j ≤ i ∧ P (f j)} ∪ {j. i+1 < j ∧ P (f (j-1))} ∪ {i+1}"
  proof (cases "j ≤ i")
    case True
    hence "wedge f i sqp j = f j" by simp
    then show ?thesis using pr True by simp
  next
    case False
    show ?thesis
    proof (cases "j = i+1")
      case True
      then show ?thesis using pr by simp
    next
      case False
      hence "i+1 < j" using ‹¬ j ≤ i› by simp
      hence "wedge f i sqp j = f (j-1)" by simp
      then show ?thesis using pr ‹i+1 < j› by simp
    qed
  qed
qed

definition one_cpl where
"one_cpl phi = (λ(i::int). (1::real) - (phi i))"

definition gross_fct where
"gross_fct f phi = (λi. f i / (one_cpl phi i))"

lemma gross_fct_sgn:
  assumes "phi i < (1::real)"
  shows "((0::real) ≤ f i) ⟷ (0 ≤ gross_fct f phi i)" unfolding gross_fct_def
  by (metis assms diff_ge_0_iff_ge eucl_less_le_not_le le_iff_diff_le_0 
      one_cpl_def zero_le_divide_iff)

lemma gross_fct_nz_eq:
  assumes "phi i ≠ (1::real)"
  shows "f i = 0 ⟷ gross_fct f phi i = 0" using assms unfolding gross_fct_def
  by (simp add: one_cpl_def)

lemma gross_fct_cong:
  assumes "f a = f' b"
  and "phi a = phi' b"
shows "gross_fct f phi a = gross_fct f' phi' b" using assms 
  unfolding gross_fct_def by (simp add: one_cpl_def)

lemma gross_fct_zero_if:
  assumes "f a = 0"
  shows "gross_fct f phi a = 0" using assms unfolding gross_fct_def by simp

definition fee_union where
"fee_union (l1::real) l2 f1 f2 = (l1*f1*(1-f2) + l2*f2*(1-f1))/
  (l1*(1-f2) + l2*(1-f1))"

lemma fee_union_pos:
  assumes "0 ≤ l1"
  and "0 ≤ l2"
  and "0 ≤ f1"
  and "0 ≤ f2"
  and "f1 < 1"
  and "f2 < 1"
shows "0 ≤ fee_union l1 l2 f1 f2" using assms unfolding fee_union_def by simp

lemma fee_union_lt_1:
  assumes "0 ≤ l1"
  and "0 ≤ l2"
  and "0 ≤ f1"
  and "0 ≤ f2"
  and "f1 < 1"
  and "f2 < 1"
shows "fee_union l1 l2 f1 f2 < 1" 
proof (cases "l1 = 0")
  case True
  thus ?thesis unfolding fee_union_def by (simp add: assms(6))
next
  case False
  show ?thesis 
  proof (cases "l2 = 0")
    case True
    then show ?thesis unfolding fee_union_def by (simp add: assms(5))
  next
    case False
    hence "0 < l1*(1-f2) + l2*(1-f1)" using assms ‹¬ l1 = 0›
      by (simp add: less_eq_real_def pos_add_strict) 
    moreover have "l1*f1*(1-f2) + l2*f2*(1-f1) < l1*(1-f2) + l2*(1-f1)"
      using assms False ‹¬ l1 = 0›
      by (smt (verit, best) mult_less_cancel_left2 mult_less_cancel_right)
    ultimately show ?thesis unfolding fee_union_def by simp
  qed
qed

lemma diff_inv_le:
  assumes "0 < (x::real)"
  and "x ≤ y"
  and "y ≤ z"
shows "(y - x)/(z*z) ≤ inverse x - inverse y"
proof -
  have "0 < y" using assms by simp
  hence "0 < z" using assms by simp
  have "(y - x)/(z*z) ≤ (y - x) / (x * y)" using assms
    by (simp add: frac_le mult_mono)
  also have "... = inverse x - inverse y"
    using ‹0 < x› ‹0 < y›
    by (simp add: divide_real_def division_ring_inverse_diff)
  finally show ?thesis .
qed

lemma diff_inv_le':
  assumes "0 < (x::real)"
  and "x ≤ y"
  and "y ≤ z"
  and "0 ≤ a"
shows " a * (y - x)/(z*z) ≤ a * (inverse x - inverse y)"
proof -
  have "0 < y" using assms by simp
  hence "0 < z" using assms by simp
  have "(y - x)/(z*z) ≤ (y - x) / (x * y)" using assms
    by (simp add: frac_le mult_mono)
  also have "... = inverse x - inverse y"
    using ‹0 < x› ‹0 < y›
    by (simp add: divide_real_def division_ring_inverse_diff)
  finally show ?thesis
    by (metis assms(4) mult_left_mono times_divide_eq_right) 
qed

lemma diff_inv_sum_le':
  assumes "∀i ∈ I. (0::real) < f i"
  and "∀i ∈ I. f i ≤ f (i+1)"
  and "∀i∈ I. f (i+1) ≤ z"
  and "∀i ∈ I. 0 ≤ g i"
  shows  "sum (λi. g i * (f (i+1) - f i)) I / (z * z) ≤ 
    sum (λi. g i * (inverse (f i) - inverse (f (i+1)))) I"
proof -
  have "sum (λi. g i * (f (i+1) - f i)) I / (z * z) = 
      sum (λi. g i * (f (i+1) - f i)/ (z * z)) I"
    by (rule sum_divide_distrib)
  also have "... ≤ sum (λi. g i * (inverse (f i) - inverse (f (i+1)))) I"
  proof (rule sum_mono)
    fix i 
    assume "i ∈ I"
    show "g i * (f (i + 1) - f i) / (z * z) ≤ 
        g i * (inverse (f i) - inverse (f (i + 1)))"
      by (rule diff_inv_le', (auto simp add: assms ‹i ∈ I›))
  qed
  finally show ?thesis .
qed

lemma diff_inv_ge:
  assumes "0 < (x::real)"
  and "x ≤ y"
  and "y ≤ z"
shows "inverse y - inverse z ≤ (z - y)/(x*x)"
proof -
  have "0 < y" using assms by simp
  hence "0 < z" using assms by simp
  hence "inverse y - inverse z = (z - y) / (y * z)"
    using ‹0 < y› by (simp add: divide_real_def division_ring_inverse_diff)
  also have "... ≤ (z - y)/(x*x)" using assms
    by (simp add: frac_le mult_mono)
  finally show ?thesis .
qed

lemma diff_inv_ge':
  assumes "0 < (x::real)"
  and "x ≤ y"
  and "y ≤ z"
  and "0 ≤ a"
shows "a * (inverse y - inverse z) ≤ a * (z - y)/(x*x)"
proof -
  have "0 < y" using assms by simp
  hence "0 < z" using assms by simp
  hence "inverse y - inverse z = (z - y) / (y * z)"
    using ‹0 < y› by (simp add: divide_real_def division_ring_inverse_diff)
  also have "... ≤ (z - y)/(x*x)" using assms
    by (simp add: frac_le mult_mono)
  finally show ?thesis
    by (metis assms(4) mult_left_mono times_divide_eq_right) 
qed

lemma diff_inv_sum_ge':
  assumes "(0::real) < z"
  and "∀i ∈ I. f i ≤ f (i+1)"
  and "∀i∈ I. z ≤ f i"
  and "∀i ∈ I. 0 ≤ g i"
shows  "sum (λi. g i * (inverse (f i) - inverse (f (i+1)))) I ≤ 
  sum (λi. g i * (f (i+1) - f i)) I / (z * z)"
proof -
  have "sum (λi. g i * (inverse (f i) - inverse (f (i+1)))) I ≤ 
      sum (λi. g i * (f (i+1) - f i)/ (z * z)) I"
  proof (rule sum_mono)
    fix i
    assume "i ∈ I"
    show "g i * (inverse (f i) - inverse (f (i + 1))) ≤ 
        g i * (f (i + 1) - f i) / (z * z)"
      by (rule diff_inv_ge', (auto simp add: assms ‹i ∈ I›))
  qed
  also have "... = sum (λi. g i * (f (i+1) - f i)) I / (z * z)"
    by (rule sum_divide_distrib[symmetric])
  finally show ?thesis .
qed

subsection ‹Support of a discrete function›

definition nz_support where
"nz_support f = {i. f i ≠ 0}"

lemma nz_supportD:
  assumes "i∈ nz_support f"
  shows "f i ≠ 0" using assms unfolding nz_support_def by simp

lemma wedge_finite_nz_support:
  assumes "finite (nz_support f)"
  shows "finite (nz_support (wedge f i sqp))" 
proof -
  define A where "A = {j. j ≤ i ∧ f j ≠ 0}"
  define B where  "B = {j. i+1 < j ∧ f (j-1) ≠ 0}" 
  have inc: "nz_support (wedge f i sqp) ⊆ A ∪ B ∪ {i+1}" 
    using wedge_arg_prop[of "λx. x ≠ 0"] 
    unfolding nz_support_def A_def B_def by auto
  have "finite A" using assms unfolding nz_support_def A_def by auto
  have "B⊆ (λj. j+1)`{j. f j ≠ 0}"
  proof
    fix j
    assume "j∈ B"
    hence "i+1 < j" and "f (j-1) ≠ 0" unfolding B_def by auto note asm = this
    define k where "k = j-1"
    hence "f k ≠ 0" using asm by simp
    hence "k ∈ {j. f j≠ 0}" by simp
    thus "j ∈ (λj. j+1)`{j. f j ≠ 0}" using ‹k = j-1› by force
  qed
  hence "finite B" using assms finite_surj unfolding nz_support_def by auto
  thus ?thesis using assms ‹finite A› inc
    by (meson finite.simps finite_UnI finite_subset)
qed

lemma gross_nz_support_eq:
  assumes "∀i ∈ nz_support f. phi i ≠ 1"
  shows "nz_support f = nz_support (gross_fct f phi)" 
  using assms gross_fct_nz_eq gross_fct_zero_if unfolding nz_support_def
  by blast

definition idx_min where
"idx_min f = Inf (nz_support f)"

definition idx_max where
"idx_max f = Sup (nz_support f)"

lemma idx_max_bdd_above_ge:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "f i ≠ 0"
  and "bdd_above (nz_support f)"
shows "i ≤ idx_max f" 
proof -
  have "i ∈ nz_support f" unfolding nz_support_def using assms by simp
  thus ?thesis unfolding idx_max_def
    by (simp add: assms cSup_upper)
qed

lemma idx_min_bdd_below_le:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "f i ≠ 0"
  and "bdd_below (nz_support f)"
shows "idx_min f ≤ i" 
proof -
  have "i ∈ nz_support f" unfolding nz_support_def using assms by simp
  thus ?thesis unfolding idx_min_def
    by (simp add: assms cInf_lower)
qed

lemma idx_max_finite_ge:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "f i ≠ 0"
  and "finite (nz_support f)"
shows "i ≤ idx_max f" using assms
  by (simp add: idx_max_bdd_above_ge)

lemma idx_min_finite_le:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "f i ≠ 0"
  and "finite (nz_support f)"
shows "idx_min f ≤ i" using assms
  by (simp add: idx_min_bdd_below_le)

lemma idx_max_finite:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "nz_support f ≠ {}"
  and "finite (nz_support f)"
shows "idx_max f = Max (nz_support f)" using assms unfolding idx_max_def 
  by (simp add: cSup_eq_Max)

lemma idx_min_finite:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "nz_support f ≠ {}"
  and "finite (nz_support f)"
shows "idx_min f = Min (nz_support f)" using assms unfolding idx_min_def 
  by (simp add: cInf_eq_Min)

lemma idx_max_finite_in:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "nz_support f ≠ {}"
  and "finite (nz_support f)"
shows "f (idx_max f) ≠ 0" using assms idx_max_finite 
  by (metis Max_in nz_supportD)

lemma idx_min_finite_in:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "nz_support f ≠ {}"
  and "finite (nz_support f)"
shows "f (idx_min f) ≠ 0" using assms idx_min_finite
  by (metis Min_in nz_supportD)

lemma idx_max_finite_gt:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "finite (nz_support f)"
and "idx_max f < i"
shows "f i = 0" 
proof -
  have "i ∉ nz_support f" using assms idx_max_finite
    by (metis Max_ge emptyE linorder_not_less)
  thus ?thesis by (simp add: nz_support_def) 
qed

lemma idx_min_finite_lt:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "finite (nz_support f)"
and "i < idx_min f"
shows "f i = 0" 
proof -
  have "i ∉ nz_support f" using assms idx_min_finite
    by (metis Min_le emptyE linorder_not_less)
  thus ?thesis by (simp add: nz_support_def) 
qed

lemma idx_min_finite_max:
fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
assumes "nz_support f ≠ {}"
and "finite (nz_support f)"
and "⋀j. j < i ⟹ f j = 0"
shows "i ≤ idx_min f" 
proof (rule ccontr)
  assume "¬ i ≤ idx_min f"
  hence "idx_min f < i" by simp
  hence "f (idx_min f) = 0" using assms by simp
  thus False using idx_min_finite_in assms by metis
qed

lemma idx_min_max_finite:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "nz_support f ≠ {}"
  and "finite (nz_support f)"
shows "idx_min f≤ idx_max f" 
proof -
  have "idx_max f ∈ nz_support f" 
    using idx_max_finite_in assms unfolding nz_support_def by simp  
  thus "idx_min f ≤ idx_max f" 
    using idx_min_finite_le assms unfolding nz_support_def by simp
qed

lemma idx_min_finiteI:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "finite (nz_support f)"
  and "f i ≠ 0"
  and "⋀j. j < i⟹ f j = 0"
shows "i = idx_min f"
proof -
  have "nz_support f ≠ {}" using assms unfolding nz_support_def by auto
  thus ?thesis
    using assms idx_min_finite_le nless_le by (metis idx_min_finite_in)
qed

lemma idx_min_finite_ge:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "finite (nz_support f)"
  and "nz_support f ≠ {}"
  and "⋀j. j ≤ i⟹ f j = 0"
shows "i ≤ idx_min f"
  by (meson assms idx_min_finite_in nle_le)

lemma idx_max_finiteI:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "finite (nz_support f)"
  and "f i ≠ 0"
  and "⋀j. j > i ⟹ f j = 0"
shows "i = idx_max f"
proof -
  have "nz_support f ≠ {}" using assms unfolding nz_support_def by auto
  thus ?thesis using assms
    by (meson idx_max_finite_gt idx_max_finite_in linorder_less_linear)
qed

lemma idx_max_finite_le:
  fixes f::"'a::conditionally_complete_linorder ⇒ 'b::zero"
  assumes "finite (nz_support f)"
  and "nz_support f ≠ {}"
  and "⋀j. i≤ j ⟹ f j = 0"
shows "idx_max f ≤ i"
  using assms idx_max_finite_in linorder_linear by auto

definition idx_min_img where
"idx_min_img g f = g (idx_min f)"

lemma idx_min_img_eq:
  assumes "∀x. f x = 0 ⟷ f' x = 0"
  shows "idx_min_img g f = idx_min_img g f'" unfolding idx_min_img_def using assms
  by (simp add: idx_min_def nz_support_def) 

definition idx_max_img where
"idx_max_img g f = g (idx_max f + 1)"

lemma idx_max_img_eq:
  assumes "∀x. f x = 0 ⟷ f' x = 0"
  shows "idx_max_img g f = idx_max_img g f'" unfolding idx_max_img_def using assms
  by (simp add: idx_max_def nz_support_def) 

lemma non_zero_liq_interv:
  fixes i::"'a::conditionally_complete_linorder"
  assumes "finite (nz_support L)"
  and "L i ≠ 0"
  shows "i ∈ {idx_min L .. idx_max L}"
  using assms idx_max_finite_ge idx_min_finite_le by auto

end