Аналіз I, Глава 7.4

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

namespace Chapter7theorem Series.sum_eq_sum (b: ) {N:} (hN: N 0) : n Finset.Icc 0 N, (if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n := b: N:hN:N 0(∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n b: N:hN:N 0Finset.Icc 0 N = Finset.image (fun n => n) (Finset.Iic N.toNat)b: N:hN:N 0 x Finset.Iic N.toNat, y Finset.Iic N.toNat, (fun n => n) x = (fun n => n) y x = y b: N:hN:N 0Finset.Icc 0 N = Finset.image (fun n => n) (Finset.Iic N.toNat) b: N:hN:N 0x:x Finset.Icc 0 N x Finset.image (fun n => n) (Finset.Iic N.toNat) b: N:hN:N 0x:0 x x N a N.toNat, a = x b: N:hN:N 0x:0 x x N a N.toNat, a = xb: N:hN:N 0x:(∃ a N.toNat, a = x) 0 x x N b: N:hN:N 0x:0 x x N a N.toNat, a = x b: N:hN:N 0x:hpos:0 xhx:x N a N.toNat, a = x b: N:hN:N 0x:hpos:0 xhx:x Nx.toNat N.toNat x.toNat = x All goals completed! 🐙 b: N:hN:N 0x:a:ha:a N.toNathb:a = x0 x x N b: N:hN:N 0x:a:ha:a N.toNathb:a = xa N All goals completed! 🐙 All goals completed! 🐙

Твердження 7.4.1

theorem Series.converges_of_permute_nonneg {a: } (ha: (a:Series).nonneg) (hconv: (a:Series).converges) {f: } (hf: Function.Bijective f) : (fun n a (f n) : Series).converges (a:Series).sum = (fun n a (f n) : Series).sum := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n){ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum have haf : (af:Series).nonneg := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha: (n : ), { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n 0hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n) (n : ), { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.seq n 0 a: ha: (n : ), { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n 0hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)n:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.seq n 0; a: ha: (n : ), { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n 0hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)n:h:n 0{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.seq n 0a: ha: (n : ), { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n 0hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)n:h:¬n 0{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.seq n 0 all_goals All goals completed! 🐙 a: hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)n:h:n 0ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq (f n.toNat) 00 a (f n.toNat) All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone S{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone T{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup S{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup T{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Q{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.suma: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Q(∃ Q, (M : ), T M Q) L = L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum have Ssum : L = (a:Series).sum := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesTo L a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Filter.Tendsto { m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.partial Filter.atTop (nhds (iSup S)) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'IsLUB (Set.range S) (iSup S) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'(Set.range S).Nonemptya: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'BddAbove (Set.range S) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'(Set.range S).Nonempty a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'S 0 Set.range S; All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup Tthis:(∃ Q, (M : ), T M Q) L = L'Q:hQ: (N : ), S N QBddAbove (Set.range S) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup Tthis:(∃ Q, (M : ), T M Q) L = L'Q:hQ: (N : ), S N QQ upperBounds (Set.range S) All goals completed! 🐙 have Tsum : L' = (af:Series).sum := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumFilter.Tendsto { m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial Filter.atTop (nhds (iSup T)) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumIsLUB (Set.range T) (iSup T) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum(Set.range T).Nonemptya: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumBddAbove (Set.range T) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum(Set.range T).Nonempty a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumT 0 Set.range T; All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumQ:hQ: (M : ), T M QBddAbove (Set.range T) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumQ:hQ: (M : ), T M QQ upperBounds (Set.range T) All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumTsum:L' = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.converges L = L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumTsum:L' = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.converges a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumTsum:L' = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum M, (N : ), { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial N M All goals completed! 🐙 have hTL (M:) : T M L := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0T M La: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0T M L a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0T M La: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0T M L a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0T M L have hM' : M < 0 := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0hM':M < 00 L a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0hM':M < 0BddAbove (Set.range S) All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatT M L have hN : N, m Y, f m N := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNat m Y, f m (Finset.image f Y).sup id a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatm:hm:m Yf m (Finset.image f Y).sup id a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatm:hm:m Yf m Finset.image f Y a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatm:hm:m Y a Y, f a = f m; All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NT M L calc _ = m Y, af m := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NT M = m Y, af m a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(∑ n Finset.Icc 0 M, if 0 n then a (f n.toNat) else 0) = n Y, a (f n) All goals completed! 🐙 _ = n f '' Y, a n := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N m Y, af m = n (f '' Y).toFinset, a n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n (f '' Y).toFinset, a n = m Y, af m a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(f '' Y).toFinset = Finset.image f Ya: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NDecidableEq a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N x Y, y Y, f x = f y x = y a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(f '' Y).toFinset = Finset.image f Y All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NDecidableEq All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Nx:hx:x Yy:hy:y Yhxy:f x = f yx = y All goals completed! 🐙 _ n Finset.Iic N, a n := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n (f '' Y).toFinset, a n n Finset.Iic N, a n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(f '' Y).toFinset Finset.Iic Na: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N i Finset.Iic N, i (f '' Y).toFinset 0 a i a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(f '' Y).toFinset Finset.Iic N a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Nn:hn:n (f '' Y).toFinsetn Finset.Iic N a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Nn:hn: a Y, f a = nn N a✝: ha✝:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a✝ (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Na:ha:a Yf a N All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Ni:a✝¹:i Finset.Iic Na✝:i (f '' Y).toFinset0 a i a: hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Ni:a✝¹:i Finset.Iic Na✝:i (f '' Y).toFinsetha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq i 00 a i a: hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Ni:a✝¹:i Finset.Iic Na✝:i (f '' Y).toFinsetha:0 a i0 a i; All goals completed! 🐙 _ = S N := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n Finset.Iic N, a n = S N a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n Finset.Iic N, a n = n Finset.Icc 0 N, if 0 n then a n.toNat else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(∑ n Finset.Icc 0 N, if 0 n then a n.toNat else 0) = n Finset.Iic N, a n exact sum_eq_sum (N:=N) a (a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NN 0 All goals completed! 🐙) _ L := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NS N L a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NBddAbove (Set.range S) All goals completed! 🐙 have hTbound : Q, M, T M Q := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QL = L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LL = L' have hSL' (N:) : S N L' := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0S N L'a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:¬N 0S N L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:¬N 0S N L'a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0S N L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:¬N 0S N L' have hN' : N < 0 := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:¬N 0hN':N < 00 L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:¬N 0hN':N < 0BddAbove (Set.range T) All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatS N L' have hM : M, n X, m, f m = n m M := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNat n X, m, f m = n m (X.preimage f ).sup id a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n X m, f m = n m (X.preimage f ).sup id a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n Xm:hm:f m = n m, f m = n m (X.preimage f ).sup id a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n Xm:hm:f m = nm (X.preimage f ).sup id a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n Xm:hm:f m = nm X.preimage f All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m MS N L' have sum_eq_sum (b: ) {N:} (hN: N 0) : n Finset.Icc 0 N, (if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0Finset.Icc 0 N = Finset.image (fun n => n) (Finset.Iic N.toNat)a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0 x Finset.Iic N.toNat, y Finset.Iic N.toNat, (fun n => n) x = (fun n => n) y x = y a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0Finset.Icc 0 N = Finset.image (fun n => n) (Finset.Iic N.toNat) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:x Finset.Icc 0 N x Finset.image (fun n => n) (Finset.Iic N.toNat); a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:0 x x N a N.toNat, a = x a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:0 x x N a N.toNat, a = xa: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:(∃ a N.toNat, a = x) 0 x x N a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:0 x x N a N.toNat, a = x a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:hpos:0 xhx:x N a N.toNat, a = x a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:hpos:0 xhx:x Nx.toNat N.toNat x.toNat = x; All goals completed! 🐙 a✝: ha✝:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a✝ (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:a:ha:a N.toNathb:a = x0 x x N a✝: ha✝:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a✝ (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN✝:hN✝:N✝ 0X:Finset := Finset.Iic N✝.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:a:ha:a N.toNathb:a = xa N; All goals completed! 🐙 All goals completed! 🐙 calc _ = n X, a n := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nS N = n X, a n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n(∑ n Finset.Icc 0 N, if 0 n then a n.toNat else 0) = n X, a n All goals completed! 🐙 _ = n Finset.image f ((Finset.Iic M).filter (fun m f m X)), a n := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n n X, a n = n Finset.image f ({m Finset.Iic M | f m X}), a n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nX = Finset.image f ({m Finset.Iic M | f m X}); a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:n X n Finset.image f ({m Finset.Iic M | f m X}); a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:n X a, (a M f a X) f a = n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:n X a, (a M f a X) f a = na: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:(∃ a, (a M f a X) f a = n) n X a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:n X a, (a M f a X) f a = n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:h:n X a, (a M f a X) f a = n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:h:n Xm:hm:f m = nhm':m M a, (a M f a X) f a = n a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:h:n Xm:hm:f m = nhm':m M(m M f m X) f m = n; All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nn:m:hm:m MhfmX:f m Xhfm:f m = nn X All goals completed! 🐙 _ m Finset.Iic M, af m := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n n Finset.image f ({m Finset.Iic M | f m X}), a n m Finset.Iic M, af m a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n x Finset.Iic M with f x X, a (f x) m Finset.Iic M, af ma: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n x {m Finset.Iic M | f m X}, y {m Finset.Iic M | f m X}, f x = f y x = y a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n x Finset.Iic M with f x X, a (f x) m Finset.Iic M, af m a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n{m Finset.Iic M | f m X} Finset.Iic Ma: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n i Finset.Iic M, i {m Finset.Iic M | f m X} 0 a (f i) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n{m Finset.Iic M | f m X} Finset.Iic M a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nm:m {m Finset.Iic M | f m X} m Finset.Iic M; a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nm:m M f m X m M; All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b ni:a✝¹:i Finset.Iic Ma✝:i {m Finset.Iic M | f m X}0 a (f i) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)S: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b ni:a✝¹:i Finset.Iic Ma✝:i {m Finset.Iic M | f m X}haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.seq i 00 a (f i) a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)S: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b ni:a✝¹:i Finset.Iic Ma✝:i {m Finset.Iic M | f m X}haf:0 af i0 a (f i) All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nx:a✝¹:x {m Finset.Iic M | f m X}y:a✝:y {m Finset.Iic M | f m X}hxy:f x = f yx = y All goals completed! 🐙 _ = T M := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n m Finset.Iic M, af m = T M a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n n Finset.Iic M, a (f n) = n Finset.Icc 0 M, if 0 n then a (f n.toNat) else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n(∑ n Finset.Icc 0 M, if 0 n then a (f n.toNat) else 0) = n Finset.Iic M, a (f n) apply sum_eq_sum af (a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nM 0 All goals completed! 🐙) _ L' := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nT M L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nBddAbove (Set.range T) All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n => a (f n)haf:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QhL'L:L' LhSL': (N : ), S N L'hLL':L L'L = L' All goals completed! 🐙

Приклад 7.4.2

theorem declaration uses 'sorry'Series.zeta_2_converges : (fun n: 1/(n+1:)^2 : Series).converges := { m := 0, seq := fun n => if n 0 then (fun n => 1 / (n + 1) ^ 2) n.toNat else 0, vanish := }.converges All goals completed! 🐙
theorem declaration uses 'sorry'Series.permuted_zeta_2_converges : (fun n: if Even n then 1/(n+2:)^2 else 1/(n:)^2 : Series).converges := { m := 0, seq := fun n => if n 0 then (fun n => if Even n then 1 / (n + 2) ^ 2 else 1 / n ^ 2) n.toNat else 0, vanish := }.converges All goals completed! 🐙theorem declaration uses 'sorry'Series.permuted_zeta_2_eq_zeta_2 : (fun n: if Even n then 1/(n+2:)^2 else 1/(n:)^2 : Series).sum = (fun n: 1/(n+1:)^2 : Series).sum := { m := 0, seq := fun n => if n 0 then (fun n => if Even n then 1 / (n + 2) ^ 2 else 1 / n ^ 2) n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => 1 / (n + 1) ^ 2) n.toNat else 0, vanish := }.sum All goals completed! 🐙

Твердження 7.4.3 (Rearrangement of series)

theorem declaration uses 'sorry'Series.absConverges_of_permute {a: } (ha : (a:Series).absConverges) {f: } (hf: Function.Bijective f) : (fun n a (f n):Series).absConverges (a:Series).sum = (fun n a (f n) : Series).sum := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sum{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum have habs : (fun n |a (f n)| : Series).converges L = (fun n |a (f n)| : Series).sum := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs = { m := 0, seq := fun n => if n 0 then |a n.toNat| else 0, vanish := }a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.nonnega: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.converges a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs = { m := 0, seq := fun n => if n 0 then |a n.toNat| else 0, vanish := } a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges(fun n => if 0 n then |if 0 n then a n.toNat else 0| else 0) = fun n => if 0 n then |a n.toNat| else 0; a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.nonneg a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.seq n 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.seq n 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.seq n 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.seq n 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0{ m := 0, seq := fun n => if n 0 then (fun n => |a n|) n.toNat else 0, vanish := }.seq n 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:(if n 0 then (fun n => |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0(if n 0 then (fun n => |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0(if n 0 then (fun n => |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0(if n 0 then (fun n => |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0(if n 0 then (fun n => |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n){ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.suma: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n){ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L' a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.abs.converges a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:(if h : n { m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n => |a (f n)|) n.toNat else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h:n 0(if h : n { m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n => |a (f n)|) n.toNat else 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h:¬n 0(if h : n { m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n => |a (f n)|) n.toNat else 0 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h:n 0(if h : n { m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n => |a (f n)|) n.toNat else 0a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)this:{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h:¬n 0(if h : n { m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.m then (fun n => |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n => |a (f n)|) n.toNat else 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n) (ε : ), 0 < ε a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < ε a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: ha: ε > 0, N { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < ε a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εha: N { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2 a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:hN₁:N₁ { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.mha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2 a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁ a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε have : N N₁, |(a:Series).partial N - L'| < ε/2 := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergesTo { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum N N₁, |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv: (ε : ), 0 < ε a_2, (b : ), a_2 b |{ m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.sum| < ε N N₁, |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv: a_1, (b : ), a_1 b |{ m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2 N N₁, |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN: (b : ), N b |{ m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2 N N₁, |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN: (b : ), N b |{ m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial (max N N₁) - L'| < ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:|{ m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.partial (max N N₁) - { m := 0, seq := fun n => if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial (max N N₁) - L'| < ε / 2 All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε have hNpos : N 0 := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε have : M, n N.toNat, finv n M := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: n N.toNat, finv n (Finset.image finv (Finset.Iic N.toNat)).sup id a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: n:hn:n N.toNatfinv n (Finset.image finv (Finset.Iic N.toNat)).sup id a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: n:hn:n N.toNatfinv n Finset.image finv (Finset.Iic N.toNat) a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: n:hn:n N.toNat a N.toNat, finv a = finv n All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n M a, (b : ), a b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n M (b : ), M b |{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'|{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε have hM'_pos : M' 0 := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 have why : Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNat := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat|{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε have claim : m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a n := calc _ = n Finset.image f (Finset.Iic M'.toNat), a n := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat m Finset.Iic M'.toNat, a (f m) = n Finset.image f (Finset.Iic M'.toNat), a n a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat n Finset.image f (Finset.Iic M'.toNat), a n = m Finset.Iic M'.toNat, a (f m) a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat x Finset.Iic M'.toNat, y Finset.Iic M'.toNat, f x = f y x = y a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatx:a✝¹:x Finset.Iic M'.toNaty:a✝:y Finset.Iic M'.toNathxy:f x = f yx = y All goals completed! 🐙 _ = _ := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat n Finset.image f (Finset.Iic M'.toNat), a n = n Finset.Iic N.toNat, a n + n X, a n a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatFinset.image f (Finset.Iic M'.toNat) = Finset.Iic N.toNat Xa: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatDecidableEq a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatDisjoint (Finset.Iic N.toNat) X a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatFinset.image f (Finset.Iic M'.toNat) = Finset.Iic N.toNat X All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatDecidableEq All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat a : ⦄, a X a Finset.Iic N.toNat a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatn:hn:n Xn Finset.Iic N.toNat a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatn:hn:n Finset.image f (Finset.Iic M'.toNat) n Finset.Iic N.toNatn Finset.Iic N.toNat All goals completed! 🐙 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds X|{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNat|{ m := 0, seq := fun n => if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε have why2 : X Finset.Icc (N.toNat+1) q := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 have claim2 : | n X, a n| ε/2 := calc _ n X, |a n| := Finset.abs_sum_le_sum_abs a X _ n Finset.Icc (N.toNat+1) q, |a n| := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n X, |a n| n Finset.Icc (N.toNat + 1) q, |a n| a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q i Finset.Icc (N.toNat + 1) q, i X 0 |a i| All goals completed! 🐙 _ ε/2 := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| ε / 2 convert ha (N.toNat+1) (a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qN.toNat + 1 N₁ All goals completed! 🐙) q (a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qq N₁ All goals completed! 🐙) a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| = | x Finset.Icc (N + 1) q, if 0 x then |if 0 x then a x.toNat else 0| else 0| a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| = x Finset.Icc (N + 1) q, if 0 x then |if 0 x then a x.toNat else 0| else 0 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q(∑ x Finset.Icc (N + 1) q, if 0 x then |if 0 x then a x.toNat else 0| else 0) = n Finset.Icc (N.toNat + 1) q, |a n| a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qFinset.Icc (N + 1) q = Finset.image (fun n => n) (Finset.Icc (N.toNat + 1) q)a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q x Finset.Icc (N.toNat + 1) q, y Finset.Icc (N.toNat + 1) q, (fun n => n) x = (fun n => n) y x = y a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qFinset.Icc (N + 1) q = Finset.image (fun n => n) (Finset.Icc (N.toNat + 1) q) a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:x Finset.Icc (N + 1) q x Finset.image (fun n => n) (Finset.Icc (N.toNat + 1) q); a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:N + 1 x x q a, (N.toNat + 1 a a q) a = x a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:N + 1 x x q a, (N.toNat + 1 a a q) a = xa: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:(∃ a, (N.toNat + 1 a a q) a = x) N + 1 x x q a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:N + 1 x x q a, (N.toNat + 1 a a q) a = x a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:hpos:N + 1 xhx:x q a, (N.toNat + 1 a a q) a = x a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:hpos:N + 1 xhx:x q(N.toNat + 1 x.toNat x.toNat q) x.toNat = x; All goals completed! 🐙 a✝: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a✝ (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a✝ (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.sumaf: := fun n => a✝ (f n)ε::0 < εN₁:ha✝: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a✝ (f m) = n Finset.Iic N.toNat, a✝ n + n X, a✝ nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:a:ha:N.toNat + 1 a a qhb:a = xN + 1 x x q a✝: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a✝ (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a✝ (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.sumaf: := fun n => a✝ (f n)ε::0 < εN₁:ha✝: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a✝ n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a✝ (f m) = n Finset.Iic N.toNat, a✝ n + n X, a✝ nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:a:ha:N.toNat + 1 a a qhb:a = xN + 1 a a q; All goals completed! 🐙 All goals completed! 🐙 calc _ |(af:Series).partial M' - (a:Series).partial N| + |(a:Series).partial N - L'| := abs_sub_le _ _ _ _ < |(af:Series).partial M' - (a:Series).partial N| + ε/2 := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2|{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N| + |{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < |{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N| + ε / 2 All goals completed! 🐙 _ ε/2 + ε/2 := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2|{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N| + ε / 2 ε / 2 + ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2|{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N| ε / 2 a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2{ m := 0, seq := fun n => if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N = n X, a n a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2 n Finset.Iic M'.toNat, af n - n Finset.Iic N.toNat, a n = n X, a n a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2 n Finset.Iic N.toNat, a n + n X, a n - n Finset.Iic N.toNat, a n = n X, a n All goals completed! 🐙 _ = ε := a: f: hf:Function.Bijective fL: := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n => if n 0 then (fun n => |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n => a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: M:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2ε / 2 + ε / 2 = ε All goals completed! 🐙

Приклад 7.4.4

noncomputable abbrev Series.a_7_4_4 : := fun n (-1:)^n / (n+2)
theorem declaration uses 'sorry'Series.ex_7_4_4_conv : (a_7_4_4 : Series).converges := { m := 0, seq := fun n => if n 0 then a_7_4_4 n.toNat else 0, vanish := }.converges All goals completed! 🐙theorem declaration uses 'sorry'Series.ex_7_4_4_sum : (a_7_4_4 : Series).sum > 0 := { m := 0, seq := fun n => if n 0 then a_7_4_4 n.toNat else 0, vanish := }.sum > 0 All goals completed! 🐙abbrev Series.f_7_4_4 : := fun n if n % 3 = 0 then 2 * (n/3) else 2*n - (n/3) - 1theorem declaration uses 'sorry'Series.f_7_4_4_bij : Function.Bijective f_7_4_4 := Function.Bijective f_7_4_4 All goals completed! 🐙theorem declaration uses 'sorry'Series.ex_7_4_4'_conv : (fun n a_7_4_4 (f_7_4_4 n) :Series).converges := { m := 0, seq := fun n => if n 0 then (fun n => a_7_4_4 (f_7_4_4 n)) n.toNat else 0, vanish := }.converges All goals completed! 🐙theorem declaration uses 'sorry'Series.ex_7_4_4'_sum : (fun n a_7_4_4 (f_7_4_4 n) :Series).sum < 0 := { m := 0, seq := fun n => if n 0 then (fun n => a_7_4_4 (f_7_4_4 n)) n.toNat else 0, vanish := }.sum < 0 All goals completed! 🐙

Вправа 7.4.1

theorem declaration uses 'sorry'Series.absConverges_of_subseries {a: } (ha: (a:Series).absConverges) {f: } (hf: StrictMono f) : (fun n a (f n):Series).absConverges := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:StrictMono f{ m := 0, seq := fun n => if n 0 then (fun n => a (f n)) n.toNat else 0, vanish := }.absConverges All goals completed! 🐙
end Chapter7