Theory Ordinary_Differential_Equations.Interval_Integral_HK

theory Interval_Integral_HK
imports Vector_Derivative_On
begin

subsection ‹interval integral›
  ― ‹TODO: move to repo ?!›
  ― ‹TODO: replace with Bochner Integral?!
           But FTC for Bochner requires continuity and euclidean space!›

definition has_ivl_integral ::
    "(real ⇒ 'b::real_normed_vector) ⇒ 'b ⇒ real ⇒ real ⇒ bool"― ‹TODO: generalize?›
  (infixr ‹has'_ivl'_integral› 46)
  where "(f has_ivl_integral y) a b ⟷ (if a ≤ b then (f has_integral y) {a .. b} else (f has_integral - y) {b .. a})"

definition ivl_integral::"real ⇒ real ⇒ (real ⇒ 'a) ⇒ 'a::real_normed_vector"
  where "ivl_integral a b f = integral {a .. b} f - integral {b .. a} f"

lemma integral_emptyI[simp]:
  fixes a b::real
  shows  "a ≥ b ⟹ integral {a..b} f = 0" "a > b ⟹ integral {a..b} f = 0"
  by (cases "a = b") auto

lemma ivl_integral_unique: "(f has_ivl_integral y) a b ⟹ ivl_integral a b f = y"
  using integral_unique[of f y "{a .. b}"] integral_unique[of f "- y" "{b .. a}"]
  unfolding ivl_integral_def has_ivl_integral_def
  by (auto split: if_split_asm)

lemma fundamental_theorem_of_calculus_ivl_integral:
  fixes f :: "real ⇒ 'a::banach"
  shows "(f has_vderiv_on f') (closed_segment a b) ⟹ (f' has_ivl_integral f b - f a) a b"
  by (auto simp: has_ivl_integral_def closed_segment_eq_real_ivl intro!: fundamental_theorem_of_calculus')

lemma
  fixes f :: "real ⇒ 'a::banach"
  assumes "f integrable_on (closed_segment a b)"
  shows indefinite_ivl_integral_continuous:
    "continuous_on (closed_segment a b) (λx. ivl_integral a x f)"
    "continuous_on (closed_segment b a) (λx. ivl_integral a x f)"
  using assms
  by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm
    intro!: indefinite_integral_continuous_1 indefinite_integral_continuous_1'
      continuous_intros intro: continuous_on_eq)

lemma
  fixes f :: "real ⇒ 'a::banach"
  assumes "f integrable_on (closed_segment a b)"
  assumes "c ∈ closed_segment a b"
  shows indefinite_ivl_integral_continuous_subset:
    "continuous_on (closed_segment a b) (λx. ivl_integral c x f)"
proof -
  from assms have "f integrable_on (closed_segment c a)" "f integrable_on (closed_segment c b)"
     by (auto simp: closed_segment_eq_real_ivl integrable_on_subinterval
      integrable_on_insert_iff split: if_splits)
  then have "continuous_on (closed_segment a c ∪ closed_segment c b) (λx. ivl_integral c x f)"
    by (auto intro!: indefinite_ivl_integral_continuous continuous_on_closed_Un)
  also have "closed_segment a c ∪ closed_segment c b = closed_segment a b"
    using assms by (auto simp: closed_segment_eq_real_ivl)
  finally show ?thesis .
qed

lemma real_Icc_closed_segment: fixes a b::real shows "a ≤ b ⟹ {a .. b} = closed_segment a b"
  by (auto simp: closed_segment_eq_real_ivl)

lemma ivl_integral_zero[simp]: "ivl_integral a a f = 0"
  by (auto simp: ivl_integral_def)

lemma ivl_integral_cong:
  assumes "⋀x. x ∈ closed_segment a b ⟹ g x = f x"
  assumes "a = c" "b = d"
  shows "ivl_integral a b f = ivl_integral c d g"
  using assms integral_spike[of "{}" "closed_segment a b" f g]
  by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma ivl_integral_diff:
  "f integrable_on (closed_segment s t) ⟹ g integrable_on (closed_segment s t) ⟹
    ivl_integral s t (λx. f x - g x) = ivl_integral s t f - ivl_integral s t g"
  using Henstock_Kurzweil_Integration.integral_diff[of f "closed_segment s t" g]
  by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma ivl_integral_norm_bound_ivl_integral:
  fixes f :: "real ⇒ 'a::banach"
  assumes "f integrable_on (closed_segment a b)"
    and "g integrable_on (closed_segment a b)"
    and "⋀x. x ∈ closed_segment a b ⟹ norm (f x) ≤ g x"
  shows "norm (ivl_integral a b f) ≤ abs (ivl_integral a b g)"
  using integral_norm_bound_integral[OF assms]
  by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma ivl_integral_norm_bound_integral:
  fixes f :: "real ⇒ 'a::banach"
  assumes "f integrable_on (closed_segment a b)"
    and "g integrable_on (closed_segment a b)"
    and "⋀x. x ∈ closed_segment a b ⟹ norm (f x) ≤ g x"
  shows "norm (ivl_integral a b f) ≤ integral (closed_segment a b) g"
  using integral_norm_bound_integral[OF assms]
  by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma norm_ivl_integral_le:
  fixes f :: "real ⇒ real"
  assumes "f integrable_on (closed_segment a b)"
    and "g integrable_on (closed_segment a b)"
    and "⋀x. x ∈ closed_segment a b ⟹ f x ≤ g x"
    and "⋀x. x ∈ closed_segment a b ⟹ 0 ≤ f x"
  shows "abs (ivl_integral a b f) ≤ abs (ivl_integral a b g)"
proof (cases "a = b")
  case True then show ?thesis
    by simp
next
  case False
  have "0 ≤ integral {a..b} f" "0 ≤ integral {b..a} f"
    by (metis le_cases Henstock_Kurzweil_Integration.integral_nonneg assms(1) assms(4) closed_segment_eq_real_ivl integral_emptyI(1))+
  then show ?thesis
    using integral_le[OF assms(1-3)]
    unfolding ivl_integral_def closed_segment_eq_real_ivl
    by (simp split: if_split_asm)
qed

lemma ivl_integral_const [simp]:
  shows "ivl_integral a b (λx. c) = (b - a) *⇩R c"
  by (auto simp: ivl_integral_def algebra_simps)

lemma ivl_integral_has_vector_derivative:
  fixes f :: "real ⇒ 'a::banach"
  assumes "continuous_on (closed_segment a b) f"
    and "x ∈ closed_segment a b"
  shows "((λu. ivl_integral a u f) has_vector_derivative f x) (at x within closed_segment a b)"
proof -
  have "((λx. integral {x..a} f) has_vector_derivative 0) (at x within {a..b})" if "a ≤ x" "x ≤ b"
    by (rule has_vector_derivative_transform) (auto simp: that)
  moreover
  have "((λx. integral {a..x} f) has_vector_derivative 0) (at x within {b..a})" if "b ≤ x" "x ≤ a"
    by (rule has_vector_derivative_transform) (auto simp: that)
  ultimately
  show ?thesis
    using assms
    by (auto simp: ivl_integral_def closed_segment_eq_real_ivl
        intro!: derivative_eq_intros
        integral_has_vector_derivative[of a b f] integral_has_vector_derivative[of b a "-f"]
        integral_has_vector_derivative'[of b a f])
qed

lemma ivl_integral_has_vderiv_on:
  fixes f :: "real ⇒ 'a::banach"
  assumes "continuous_on (closed_segment a b) f"
  shows "((λu. ivl_integral a u f) has_vderiv_on f) (closed_segment a b)"
  using ivl_integral_has_vector_derivative[OF assms]
  by (auto simp: has_vderiv_on_def)

lemma ivl_integral_has_vderiv_on_subset_segment:
  fixes f :: "real ⇒ 'a::banach"
  assumes "continuous_on (closed_segment a b) f"
    and "c ∈ closed_segment a b"
  shows "((λu. ivl_integral c u f) has_vderiv_on f) (closed_segment a b)"
proof -
  have "(closed_segment c a) ⊆ (closed_segment a b)" "(closed_segment c b) ⊆ (closed_segment a b)"
    using assms by (auto simp: closed_segment_eq_real_ivl split: if_splits)
  then have "((λu. ivl_integral c u f) has_vderiv_on f) ((closed_segment c a) ∪ (closed_segment c b))"
    by (auto intro!: has_vderiv_on_union_closed ivl_integral_has_vderiv_on assms
      intro: continuous_on_subset)
  also have "(closed_segment c a) ∪ (closed_segment c b) = (closed_segment a b)"
    using assms by (auto simp: closed_segment_eq_real_ivl split: if_splits)
  finally show ?thesis .
qed

lemma ivl_integral_has_vector_derivative_subset:
  fixes f :: "real ⇒ 'a::banach"
  assumes "continuous_on (closed_segment a b) f"
    and "x ∈ closed_segment a b"
    and "c ∈ closed_segment a b"
  shows "((λu. ivl_integral c u f) has_vector_derivative f x) (at x within closed_segment a b)"
  using ivl_integral_has_vderiv_on_subset_segment[OF assms(1)] assms(2-)
  by (auto simp: has_vderiv_on_def)

lemma
  compact_interval_eq_Inf_Sup:
  fixes A::"real set"
  assumes "is_interval A" "compact A" "A ≠ {}"
  shows "A = {Inf A .. Sup A}"
  apply (auto simp: closed_segment_eq_real_ivl
      intro!: cInf_lower cSup_upper bounded_imp_bdd_below bounded_imp_bdd_above
      compact_imp_bounded assms)
  by (metis assms(1) assms(2) assms(3) cInf_eq_minimum cSup_eq_maximum compact_attains_inf
      compact_attains_sup mem_is_interval_1_I)

lemma ivl_integral_has_vderiv_on_compact_interval:
  fixes f :: "real ⇒ 'a::banach"
  assumes "continuous_on A f"
    and "c ∈ A" "is_interval A" "compact A"
  shows "((λu. ivl_integral c u f) has_vderiv_on f) A"
proof -
  have "A = {Inf A .. Sup A}"
    by (rule compact_interval_eq_Inf_Sup) (use assms in auto)
  also have "… = closed_segment (Inf A) (Sup A)" using assms
    by (auto simp add: closed_segment_eq_real_ivl
        intro!: cInf_le_cSup bounded_imp_bdd_below bounded_imp_bdd_above compact_imp_bounded)
  finally have *: "A = closed_segment (Inf A) (Sup A)" .
  show ?thesis
    apply (subst *)
    apply (rule ivl_integral_has_vderiv_on_subset_segment)
    unfolding *[symmetric]
    by fact+
qed

lemma ivl_integral_has_vector_derivative_compact_interval:
  fixes f :: "real ⇒ 'a::banach"
  assumes "continuous_on A f"
    and "is_interval A" "compact A" "x ∈ A" "c ∈ A"
  shows "((λu. ivl_integral c u f) has_vector_derivative f x) (at x within A)"
  using ivl_integral_has_vderiv_on_compact_interval[OF assms(1)] assms(2-)
  by (auto simp: has_vderiv_on_def)

lemma ivl_integral_combine:
  fixes f::"real ⇒ 'a::banach"
  assumes "f integrable_on (closed_segment a b)"
  assumes "f integrable_on (closed_segment b c)"
  assumes "f integrable_on (closed_segment a c)"
  shows "ivl_integral a b f + ivl_integral b c f = ivl_integral a c f"
proof -
  show ?thesis
    using assms
      Henstock_Kurzweil_Integration.integral_combine[of a b c f]
      Henstock_Kurzweil_Integration.integral_combine[of a c b f]
      Henstock_Kurzweil_Integration.integral_combine[of b a c f]
      Henstock_Kurzweil_Integration.integral_combine[of b c a f]
      Henstock_Kurzweil_Integration.integral_combine[of c a b f]
      Henstock_Kurzweil_Integration.integral_combine[of c b a f]
    by (cases "a ≤ b"; cases "b ≤ c"; cases "a ≤ c")
       (auto simp: algebra_simps ivl_integral_def closed_segment_eq_real_ivl)
qed

lemma integral_equation_swap_initial_value:
  fixes x::"real⇒'a::banach"
  assumes "⋀t. t ∈ closed_segment t0 t1 ⟹ x t = x t0 + ivl_integral t0 t (λt. f t (x t))"
  assumes t: "t ∈ closed_segment t0 t1"
  assumes int: "(λt. f t (x t)) integrable_on closed_segment t0 t1"
  shows "x t = x t1 + ivl_integral t1 t (λt. f t (x t))"
proof -
  from t int have "(λt. f t (x t)) integrable_on closed_segment t0 t"
    "(λt. f t (x t)) integrable_on closed_segment t t1"
    by (auto intro: integrable_on_subinterval simp: closed_segment_eq_real_ivl split: if_split_asm)
  with assms(1)[of t] assms(2-)
  have "x t - x t0 = ivl_integral t0 t1 (λt. f t (x t)) + ivl_integral t1 t (λt. f t (x t))"
    by (subst ivl_integral_combine) (auto simp: closed_segment_commute)
  then have "x t + x t1 - (x t0 + ivl_integral t0 t1 (λt. f t (x t))) =
    x t1 + ivl_integral t1 t (λt. f t (x t))"
    by (simp add: algebra_simps)
  also have "x t0 + ivl_integral t0 t1 (λt. f t (x t)) = x t1"
    by (auto simp: assms(1)[symmetric])
  finally show ?thesis  by simp
qed

lemma has_integral_nonpos:
  fixes f :: "'n::euclidean_space ⇒ real"
  assumes "(f has_integral i) s"
    and "∀x∈s. f x ≤ 0"
  shows "i ≤ 0"
  by (rule has_integral_nonneg[of "-f" "-i" s, simplified])
    (auto intro!: has_integral_neg simp: fun_Compl_def assms)

lemma has_ivl_integral_nonneg:
  fixes f :: "real ⇒ real"
  assumes "(f has_ivl_integral i) a b"
    and "⋀x. a ≤ x ⟹ x ≤ b ⟹ 0 ≤ f x"
    and "⋀x. b ≤ x ⟹ x ≤ a ⟹ f x ≤ 0"
  shows "0 ≤ i"
  using assms has_integral_nonneg[of f i "{a .. b}"] has_integral_nonpos[of f "-i" "{b .. a}"]
  by (auto simp: has_ivl_integral_def Ball_def not_le split: if_split_asm)

lemma has_ivl_integral_ivl_integral:
  "f integrable_on (closed_segment a b) ⟷ (f has_ivl_integral (ivl_integral a b f)) a b"
  by (auto simp: closed_segment_eq_real_ivl has_ivl_integral_def ivl_integral_def)

lemma ivl_integral_nonneg:
  fixes f :: "real ⇒ real"
  assumes "f integrable_on (closed_segment a b)"
    and "⋀x. a ≤ x ⟹ x ≤ b ⟹ 0 ≤ f x"
    and "⋀x. b ≤ x ⟹ x ≤ a ⟹ f x ≤ 0"
  shows "0 ≤ ivl_integral a b f"
  by (rule has_ivl_integral_nonneg[OF assms(1)[unfolded has_ivl_integral_ivl_integral] assms(2-3)])

lemma ivl_integral_bound:
  fixes f::"real ⇒ 'a::banach"
  assumes "continuous_on (closed_segment a b) f"
  assumes "⋀t. t ∈ (closed_segment a b) ⟹ norm (f t) ≤ B"
  shows "norm (ivl_integral a b f) ≤ B * abs (b - a)"
  using integral_bound[of a b f B]
    integral_bound[of b a f B]
    assms
  by (auto simp: closed_segment_eq_real_ivl has_ivl_integral_def ivl_integral_def split: if_splits)

lemma ivl_integral_minus_sets:
  fixes f::"real ⇒ 'a::banach"
  shows "f integrable_on (closed_segment c a) ⟹ f integrable_on (closed_segment c b) ⟹ f integrable_on (closed_segment a b) ⟹
    ivl_integral c a f - ivl_integral c b f = ivl_integral b a f"
  using ivl_integral_combine[of f c b a]
  by (auto simp: algebra_simps closed_segment_commute)

lemma ivl_integral_minus_sets':
  fixes f::"real ⇒ 'a::banach"
  shows "f integrable_on (closed_segment a c) ⟹ f integrable_on (closed_segment b c) ⟹ f integrable_on (closed_segment a b) ⟹
    ivl_integral a c f - ivl_integral b c f = ivl_integral a b f"
  using ivl_integral_combine[of f a b c]
  by (auto simp: algebra_simps closed_segment_commute)

end