A Missing Lemma Dual to nn_integral_FTC_atLeast

[伊藤洋介]

Dear Isabelle developers,

Could you consider adding the following code
to Equivalence_Lebesgue_Henstock_Integration.thy?
This is the counterpart of the lemma nn_integral_FTC_atLeast.

---------------------------------------------------------------------------
lemma nn_integral_FTC_atMost:
  fixes f :: "real \<Rightarrow> real"
  assumes f_borel: "f \<in> borel_measurable borel"
  assumes f: "\<And>x. x \<le> b \<Longrightarrow> DERIV F x :> f x"
  assumes nonneg: "\<And>x. x \<le> b \<Longrightarrow> 0 \<le> f x"
  assumes lim: "(F \<longlongrightarrow> U) at_bot"
  shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {.. b} x
\<partial>lborel) = F b - U"
proof -
  let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {b -
real i .. b} x"
  let ?fR = "\<lambda>x. ennreal (f x) * indicator {.. b} x"

  have F_mono: "y \<le> b \<Longrightarrow> x \<le> y \<Longrightarrow> F x
\<le> F y" for x y
    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F])
(auto intro: order_trans)
  then have F_ge_U: "x \<le> b \<Longrightarrow> F x \<ge> U" for x
    by (intro tendsto_upperbound[OF lim])
       (auto simp: eventually_at_bot_linorder)

  have "(SUP i. ?f i x) = ?fR x" for x
  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
    obtain n where "b - x < real n"
      using reals_Archimedean2[of "b - x"] ..
    then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
      by (auto simp: frequently_def intro!: eventually_sequentiallyI[where
c=n] split: split_indicator)
    then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
      by (rule tendsto_eventually)
  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i.
?f i x) \<partial>lborel)"
    by simp
  also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x
\<partial>lborel))"
  proof (rule nn_integral_monotone_convergence_SUP)
    show "incseq ?f"
      using nonneg by (auto simp: incseq_def le_fun_def split:
split_indicator)
    show "\<And>i. (?f i) \<in> borel_measurable lborel"
      using f_borel by auto
  qed
  also have "\<dots> = (SUP i. ennreal (F b - F (b - real i)))"
    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
  also have "\<dots> = F b - U"
  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
    have "LIM n sequentially. b - real n :> at_bot"
      by real_asymp
    then have "(\<lambda>n. F (b - real n)) \<longlonglongrightarrow> U"
      using filterlim_compose lim by force
    then show "(\<lambda>n. ennreal (F b - F (b - real n)) )
\<longlonglongrightarrow> ennreal (F b - U)"
      by (simp add: F_mono F_ge_U tendsto_diff)
  qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
  finally show ?thesis .
qed
---------------------------------------------------------------------------

Best regards,

-- 
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345 at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260211/70323aef/attachment.htm>