Email Gateway (Feb 11 2026 at 12:58): Email Gateway (Feb 11 2026 at 12:58):From: 伊藤洋介 <glacier345@gmail.com>
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@gmail.com
Email Gateway (Feb 14 2026 at 12:02):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Thanks for the suggestion. I did this and I was able to find a proof by symmetry, avoiding a near-repetition of the previous proof.
On 11 Feb 2026, at 12:57, 伊藤洋介 <glacier345@gmail.com> wrote:
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.
Email Gateway (Feb 14 2026 at 12:12):From: 伊藤洋介 <glacier345@gmail.com>
Hello,
Thank you for the reply.
I was surprised since I could not find a proof by symmetry.
I am looking forward to seeing the proof.
2026年2月14日(土) 21:02 Lawrence Paulson <lp15@cam.ac.uk>:
Thanks for the suggestion. I did this and I was able to find a proof by
symmetry, avoiding a near-repetition of the previous proof.On 11 Feb 2026, at 12:57, 伊藤洋介 <glacier345@gmail.com> wrote:
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.
--
伊藤 洋介
080-5057-6931
glacier345@gmail.com
Email Gateway (Feb 14 2026 at 12:15):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
It took a little work to find the right lemmas. But it's worth having these lemmas in the long run.
On 14 Feb 2026, at 12:12, 伊藤洋介 <glacier345@gmail.com> wrote:
Thank you for the reply.
I was surprised since I could not find a proof by symmetry.
I am looking forward to seeing the proof.2026年2月14日(土) 21:02 Lawrence Paulson <lp15@cam.ac.uk>:
Thanks for the suggestion. I did this and I was able to find a proof by symmetry, avoiding a near-repetition of the previous proof.On 11 Feb 2026, at 12:57, 伊藤洋介 <glacier345@gmail.com> wrote:
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.
Email Gateway (Feb 14 2026 at 12:22):From: 伊藤洋介 <glacier345@gmail.com>
:+1:
伊藤洋介 さんが Gmail
<https://www.google.com/gmail/about/?utm_source=gmail-in-product&utm_medium=et&utm_campaign=emojireactionemail#app>
でリアクションしました
2026年2月14日(土) 21:15 Lawrence Paulson <lp15@cam.ac.uk>:
It took a little work to find the right lemmas. But it's worth having
these lemmas in the long run.On 14 Feb 2026, at 12:12, 伊藤洋介 <glacier345@gmail.com> wrote:
Thank you for the reply.
I was surprised since I could not find a proof by symmetry.
I am looking forward to seeing the proof.2026年2月14日(土) 21:02 Lawrence Paulson <lp15@cam.ac.uk>:
Thanks for the suggestion. I did this and I was able to find a proof by
symmetry, avoiding a near-repetition of the previous proof.On 11 Feb 2026, at 12:57, 伊藤洋介 <glacier345@gmail.com> wrote:
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.
--
伊藤 洋介
080-5057-6931
glacier345@gmail.com
Last updated: Feb 25 2026 at 08:53 UTC