Email Gateway (Aug 19 2022 at 16:39): Email Gateway (Aug 19 2022 at 16:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I want to prove that the order of summation of a converging sequence of non-negative reals
does not matter. In Complex_Main, I'd express this as follows;
lemma
fixes f :: "nat => real"
assumes "summable f"
and "bij g"
and "!!x. 0 <= f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex: "suminf (f o g) = suminf f"
My problem is that I have no clue how to prove this in Isabelle, because I am not so
familiar with the details of limits in Isabelle. I expect that I could prove
summable_reindex using the lemma summable_Cauchy, but the proof definitely will not be
elegant. So I wonder:
Thanks in advance for any help,
Andreas
Email Gateway (Aug 19 2022 at 16:40):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Montag, den 17.11.2014, 10:41 +0100 schrieb Andreas Lochbihler:
Dear all,
I want to prove that the order of summation of a converging sequence of non-negative reals
does not matter. In Complex_Main, I'd express this as follows;lemma
fixes f :: "nat => real"
assumes "summable f"
and "bij g"
and "!!x. 0 <= f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex: "suminf (f o g) = suminf f"My problem is that I have no clue how to prove this in Isabelle, because I am not so
familiar with the details of limits in Isabelle. I expect that I could prove
summable_reindex using the lemma summable_Cauchy, but the proof definitely will not be
elegant. So I wonder:
- Is a better way to prove summable_reindex?
summable_reindex depends on the order of reals, it does not work
without. So summable_Cauchy which is about metric is not so well suited.
A better idea may be to use summation on extended reals, here you have
suminf f = (SUP n. setsum f {..n})
and then antisymmetry (or better SUP_eq) to prove:
(SUP n. setsum f {..n}) = (SUP n. setsum (f o g) {..n})
A attached a proof using HOL-Probability, as it uses the non-negative
integral on ereals, which is very easy to proof. (especially with
distr_bij_count_space which I will add to the repository...)
- How can I prove suminf_reindex?
Prove it first on ereal and then reduce it to the reals (see my proof)
- Can I generalise the type real to some type class (which)?
You need order, so maybe:
{ordered_comm_monoid_add, linorder_topology,
conditionally_complete_linorder}
at least that's what I used for summableI_nonneg_bounded.
real_normed_vectors do not work, as you need to state that you somehow
always run in the same direction.
Email Gateway (Aug 19 2022 at 16:40):From: Joachim Breitner <breitner@kit.edu>
Hi,
it’s not so bad, using the sandwich theorem I gave it a shot and did all
real-related proof-steps. There are just two holes related to "nat ⇒
nat" functions left as an exercise for the reader :-)
theory Scratch imports Complex_Main begin
lemma
fixes f :: "nat => real"
assumes "summable f"
and "bij g"
and pos: "!!x. 0 <= f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex: "suminf (f o g) = suminf f"
proof-
obtain m :: "nat ⇒ nat" where "subseq m" and "∀ n n'. n' < m n ⟶ inv g n' < n" sorry
hence m: "⋀ n. {..<m n} ⊆ g ` {..<n}"
by (auto simp add: lessThan_def, metis (mono_tags) assms(2) bij_image_Collect_eq mem_Collect_eq)
obtain M :: "nat ⇒ nat" where "subseq M" and n: "∀ n n'. n' < n ⟶ g n' < M n" sorry
have inj: "⋀ S. inj_on g S" using bij g by (metis bij_is_inj injD inj_onI)
have "(λn. ∑i<n. f (g i)) ----> suminf f"
proof (rule real_tendsto_sandwich[OF eventually_sequentiallyI eventually_sequentiallyI])
fix n
have "(∑i<m n. f i) ≤ setsum f (g {..<n})"
by (rule setsum_mono3) (auto simp add: pos m)
thus "(∑i<m n. f i) ≤ (∑i<n. f (g i))"
by (simp add: setsum.reindex[OF inj])
next
fix n
have "setsum f (g {..<n}) ≤ (∑i<M n. f i)"
by (rule setsum_mono3) (auto simp add: pos n[rule_format])
thus "(∑i<n. f (g i)) ≤ (∑i<M n. f i)"
by (simp add: setsum.reindex[OF inj])
next
from summable f
have "(λx. setsum f {..<x}) ----> suminf f" by (metis summable_LIMSEQ)
from LIMSEQ_subseq_LIMSEQ[OF this subseq m]
show "(λx. setsum f {..<m x}) ----> suminf f"
by (simp add: comp_def)
next
from summable f
have "(λx. setsum f {..<x}) ----> suminf f" by (metis summable_LIMSEQ)
from LIMSEQ_subseq_LIMSEQ[OF this subseq M]
show "(λx. setsum f {..<M x}) ----> suminf f"
by (simp add: comp_def)
qed
hence "(f ∘ g) sums suminf f" by (simp add: sums_def)
thus "summable (f o g)" and "suminf (f o g) = suminf f"
by (auto simp add: sums_iff)
qed
The "subseq" requirement might be a bit too strong, but I did not see a
lemma like LIMSEQ_subseq_LIMSEQ (X ----> L ⟹ subseq f ⟹ (X ∘ f) ----> L)
that would allow repeating elements.
Hope it helps.
Greetings
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:40):From: Joachim Breitner <breitner@kit.edu>
Hi,
yes, it’s possible without, and actually nicer:
theory Scratch imports Complex_Main begin
lemma
fixes f :: "nat => real"
assumes "summable f"
and "inj g"
and pos: "!!x. 0 <= f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex_aux: "suminf (f o g) ≤ suminf f"
proof-
have "∀ n. ∀ n' ∈ (g {..<n}). n' < Suc (Max (g {..<n}))"
by (metis Max_ge finite_imageI finite_lessThan not_le not_less_eq)
hence "∀ n. ∃ m. ∀ n'<n. g n' < m" by auto
then obtain M :: "nat ⇒ nat" where n: "∀ n n'. n' < n ⟶ g n' < M n" by metis
have inj: "⋀ S. inj_on g S" using inj g by (metis injD inj_onI)
have smaller: "⋀n. (∑i<n. f (g i)) ≤ suminf f"
proof-
fix n
have "setsum f (g {..<n}) ≤ (∑i<M n. f i)"
by (rule setsum_mono3) (auto simp add: pos n[rule_format])
hence "(∑i<n. f (g i)) ≤ (∑i<M n. f i)"
by (simp add: setsum.reindex[OF inj])
also have "… ≤ suminf f"
using summable f`
by (rule setsum_le_suminf) (simp add: pos)
finally
show "(∑i<n. f (g i)) ≤ suminf f".
qed
have "incseq (λn. ∑i<n. f (g i))"
by (rule incseq_SucI) (auto simp add: pos)
moreover
have "∀n. (∑i<n. f (g i)) ≤ suminf f" by (auto intro: smaller)
ultimately
obtain L where L: "(λ n. ∑i<n. f (g i)) ----> L" by (rule incseq_convergent)
hence "(f ∘ g) sums L" by (simp add: sums_def)
thus "summable (f o g)" by (auto simp add: sums_iff)
from (f ∘ g) sums L
have "suminf (f ∘ g) = L" by (auto simp add: sums_iff)
from L
have "L ≤ suminf f"
by (rule LIMSEQ_le_const2) (auto intro: smaller)
with _ = L
show "suminf (f o g) ≤ suminf f" by simp
qed
lemma
fixes f :: "nat => real"
assumes "summable f"
and "bij g"
and pos: "!!x. 0 <= f x"
shows suminf_reindex: "suminf (f o g) = suminf f"
proof-
from bij g have "inj g" by (rule bij_is_inj)
from bij g have [simp]: "⋀ x. g (inv g x) = x" by (metis bij_betw_imp_surj surj_f_inv_f)
show "suminf (f o g) = suminf f"
proof (rule antisym)
show "suminf (f ∘ g) ≤ suminf f"
by (rule suminf_reindex_aux[OF summable f inj g pos])
next
have "summable (f ∘ g)" by (rule summable_reindex[OF summable f inj g pos])
moreover
from bij g
have "inj (inv g)" by (metis bij_betw_def surj_imp_inj_inv)
moreover
from pos
have "⋀ x. 0 ≤ (f ∘ g) x" by simp
ultimately
have "suminf ((f ∘ g) ∘ inv g) ≤ suminf (f ∘ g) "
by (rule suminf_reindex_aux)
thus "suminf f ≤ suminf (f ∘ g)" by (simp add:comp_def)
qed
qed
And now I got to run, my colleages are going to watch a movie and I’m
already late. Stupid addictivity of Isabelle :-)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Johannes and Joachim,
Thanks a lot for your efforts. I'll generalise and polish Joachim's proof a bit and
ultimately will add it to the repository. I won't try to abstract from reals to some type
class because both of your proofs rely on lemmas about the reals.
Best,
Andreas
Last updated: Apr 25 2024 at 16:19 UTC