Axeyum
Get started
Vision
Learn
By fieldSATSMTComputer algebraProof checkingFormal librariesConcept wiki
Components
SAT SolverSMT SolverCASKernelLibrary
Problems
Results
SMT-LIB benchmarksCAS comparisonLean comparisonmathlib comparison
Artifacts
Docs
SearchGet startedGitHub ↗

Artifact · proved

A power series with bounded coefficients converges uniformly on [0,r] once the dominating geometric series is Cauchy

This page records one proposition and the evidence attached to it. Text from the source ledger is shown as record data.

Identifier
F:creal-powerseriesuniformconvergeson
Proof route
kernel-lean
External status
proved
Axiom footprint
Empty

Recorded description

For a coefficient sequence c bounded by M (|c j| <= M for every j), and r with 0 <= r: if the dominating series M*r^j is Cauchy at a stated rational rate (the raw Within bound needed by CReal.weierstrassMTest's own hypothesis), then the partial sums of the power series powerSeriesTerm c j x converge UNIFORMLY on [0, r] to the pointwise limit built at each clamped point. This is CReal.weierstrassMTest specialized to a power series: instantiated at f := powerSeriesTerm c, a := zero, b := r, hab reused directly from the domination hypothesis's own lower bound (choosing [0,r] rather than [-r,r] costs nothing beyond that), hcong := CReal.powerSeriesTerm_congr, and hdom built inline from CReal.powerSeriesTerm_abs_le. The canonical type is large (tens of kilobytes rendered) because -- per this development's own convention, documented at the call site -- it is read off via Kernel::infer rather than hand-rebuilt: weierstrassMTest's own conclusion embeds its limit function G as an explicit expression, which this declaration has no reason to reconstruct by hand a second time.

Formal statement 
theorem CReal.powerSeriesUniformConvergesOn : ((x0 : ((x0 : AxNat) -> CReal)) -> ((x1 : CReal) -> ((x2 : ((x2 : AxNat) -> CReal.le (CReal.abs (x0 x2)) x1)) -> ((x3 : CReal) -> ((x4 : CReal.le CReal.zero x3) -> ((x5 : AxNat) -> ((x6 : ((x6 : AxNat) -> ((x7 : AxNat) -> CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x8 : AxNat) => CReal.mul x1 (CReal.pow x3 x8)) x6) x6) (CReal.seq (CReal.sumRange (fun (x8 : AxNat) => CReal.mul x1 (CReal.pow x3 x8)) x7) x7)) (Rat.add (Rat.natDivSucc x5 x6) (Rat.natDivSucc x5 x7))))) -> CReal.UniformConvergesOn (fun (x7 : AxNat) => fun (x8 : CReal) => CReal.sumRange (fun (x9 : AxNat) => CReal.powerSeriesTerm x0 x9 x8) x7) (fun (x7 : CReal) => CReal.mk (CReal.speedup (fun (x8 : AxNat) => CReal.seq (CReal.sumRange (fun (x9 : AxNat) => CReal.powerSeriesTerm x0 x9 (CReal.max CReal.zero (CReal.min x7 x3))) x8) x8) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) (CReal.regular_of_kregular (fun (x8 : AxNat) => CReal.seq (CReal.sumRange (fun (x9 : AxNat) => CReal.powerSeriesTerm x0 x9 (CReal.max CReal.zero (CReal.min x7 x3))) x8) x8) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) (fun (x8 : AxNat) => fun (x9 : AxNat) => And.intro (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) (Rat.le (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9))) (Rat.le_trans (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9))) (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.neg_le_neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9)) (Rat.add_le_add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) (AxNat.succ AxNat.zero) x8) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) (AxNat.succ AxNat.zero) x9))) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) (Rat.le (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (fun (x10 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) (Rat.le (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x8) ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x9))) (fun (x10 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) => fun (x11 : Rat.le (Rat.sub ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x8) ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) => x10) ((fun (x10 : AxNat) => fun (x11 : AxNat) => Or.rec (AxNat.le x10 x11) (AxNat.le x11 x10) (fun (x12 : Or (AxNat.le x10 x11) (AxNat.le x11 x10)) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11))) (fun (x12 : AxNat.le x10 x11) => Eq.rec.{0, 1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)) (fun (x13 : Rat) => fun (x14 : Eq.{1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)) x13) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => CReal.powerSeriesTerm x0 x15 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => CReal.powerSeriesTerm x0 x15 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11)) x13) (Eq.rec.{0, 1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (fun (x13 : Rat) => fun (x14 : Eq.{1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) x13) => CReal.Within x13 (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.bounds_neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x13 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (fun (x13 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) => fun (x14 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) => x13) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) (fun (x13 : AxNat) => CReal.mul x1 (CReal.pow x3 x13)) x5 x10 x11 (fun (x13 : AxNat) => (fun (x14 : AxNat) => fun (x15 : CReal) => fun (x16 : CReal.le CReal.zero x15) => fun (x17 : CReal.le x15 x3) => CReal.powerSeriesTerm_abs_le x0 x1 x2 x15 x3 x16 x17 x14) x13 (CReal.max CReal.zero (CReal.min x7 x3)) (CReal.le_max_left CReal.zero (CReal.min x7 x3)) (CReal.max_le CReal.zero (CReal.min x7 x3) x3 x4 (CReal.min_le_right x7 x3))) x6 x12)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x13 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)))) => Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x13 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) => fun (x14 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) => x14) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) (fun (x13 : AxNat) => CReal.mul x1 (CReal.pow x3 x13)) x5 x10 x11 (fun (x13 : AxNat) => (fun (x14 : AxNat) => fun (x15 : CReal) => fun (x16 : CReal.le CReal.zero x15) => fun (x17 : CReal.le x15 x3) => CReal.powerSeriesTerm_abs_le x0 x1 x2 x15 x3 x16 x17 x14) x13 (CReal.max CReal.zero (CReal.min x7 x3)) (CReal.le_max_left CReal.zero (CReal.min x7 x3)) (CReal.max_le CReal.zero (CReal.min x7 x3) x3 x4 (CReal.min_le_right x7 x3))) x6 x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11)) (Rat.neg_sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11)) (Rat.add_comm (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x12 : AxNat.le x11 x10) => CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) (fun (x13 : AxNat) => CReal.mul x1 (CReal.pow x3 x13)) x5 x11 x10 (fun (x13 : AxNat) => (fun (x14 : AxNat) => fun (x15 : CReal) => fun (x16 : CReal.le CReal.zero x15) => fun (x17 : CReal.le x15 x3) => CReal.powerSeriesTerm_abs_le x0 x1 x2 x15 x3 x16 x17 x14) x13 (CReal.max CReal.zero (CReal.min x7 x3)) (CReal.le_max_left CReal.zero (CReal.min x7 x3)) (CReal.max_le CReal.zero (CReal.min x7 x3) x3 x4 (CReal.min_le_right x7 x3))) x6 x12) (AxNat.le_total x10 x11)) x8 x9))) (Rat.le_trans (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) (Rat.le (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (fun (x10 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) (Rat.le (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9)))) => Rat.le (Rat.sub ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x8) ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (fun (x10 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) (Rat.sub ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x8) ((fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => CReal.powerSeriesTerm x0 x11 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) x9))) => fun (x11 : Rat.le (Rat.sub ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x8) ((fun (x11 : AxNat) => CReal.seq (CReal.sumRange (fun (x12 : AxNat) => CReal.powerSeriesTerm x0 x12 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) x9)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9))) => x11) ((fun (x10 : AxNat) => fun (x11 : AxNat) => Or.rec (AxNat.le x10 x11) (AxNat.le x11 x10) (fun (x12 : Or (AxNat.le x10 x11) (AxNat.le x11 x10)) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11))) (fun (x12 : AxNat.le x10 x11) => Eq.rec.{0, 1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)) (fun (x13 : Rat) => fun (x14 : Eq.{1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)) x13) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => CReal.powerSeriesTerm x0 x15 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => CReal.powerSeriesTerm x0 x15 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11)) x13) (Eq.rec.{0, 1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (fun (x13 : Rat) => fun (x14 : Eq.{1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) x13) => CReal.Within x13 (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.bounds_neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x13 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (fun (x13 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) => fun (x14 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) => x13) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) (fun (x13 : AxNat) => CReal.mul x1 (CReal.pow x3 x13)) x5 x10 x11 (fun (x13 : AxNat) => (fun (x14 : AxNat) => fun (x15 : CReal) => fun (x16 : CReal.le CReal.zero x15) => fun (x17 : CReal.le x15 x3) => CReal.powerSeriesTerm_abs_le x0 x1 x2 x15 x3 x16 x17 x14) x13 (CReal.max CReal.zero (CReal.min x7 x3)) (CReal.le_max_left CReal.zero (CReal.min x7 x3)) (CReal.max_le CReal.zero (CReal.min x7 x3) x3 x4 (CReal.min_le_right x7 x3))) x6 x12)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x13 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10)))) => Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x13 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) => fun (x14 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x14 : AxNat) => CReal.powerSeriesTerm x0 x14 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) => x14) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) (fun (x13 : AxNat) => CReal.mul x1 (CReal.pow x3 x13)) x5 x10 x11 (fun (x13 : AxNat) => (fun (x14 : AxNat) => fun (x15 : CReal) => fun (x16 : CReal.le CReal.zero x15) => fun (x17 : CReal.le x15 x3) => CReal.powerSeriesTerm_abs_le x0 x1 x2 x15 x3 x16 x17 x14) x13 (CReal.max CReal.zero (CReal.min x7 x3)) (CReal.le_max_left CReal.zero (CReal.min x7 x3)) (CReal.max_le CReal.zero (CReal.min x7 x3) x3 x4 (CReal.min_le_right x7 x3))) x6 x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11)) (Rat.neg_sub (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x11) x11) (CReal.seq (CReal.sumRange (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) x10) x10))) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11)) (Rat.add_comm (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x10))) (fun (x12 : AxNat.le x11 x10) => CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x13 : AxNat) => CReal.powerSeriesTerm x0 x13 (CReal.max CReal.zero (CReal.min x7 x3))) (fun (x13 : AxNat) => CReal.mul x1 (CReal.pow x3 x13)) x5 x11 x10 (fun (x13 : AxNat) => (fun (x14 : AxNat) => fun (x15 : CReal) => fun (x16 : CReal.le CReal.zero x15) => fun (x17 : CReal.le x15 x3) => CReal.powerSeriesTerm_abs_le x0 x1 x2 x15 x3 x16 x17 x14) x13 (CReal.max CReal.zero (CReal.min x7 x3)) (CReal.le_max_left CReal.zero (CReal.min x7 x3)) (CReal.max_le CReal.zero (CReal.min x7 x3) x3 x4 (CReal.min_le_right x7 x3))) x6 x12) (AxNat.le_total x10 x11)) x8 x9)) (Rat.add_le_add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x8) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) x9) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5))))))))) x9) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) (AxNat.succ AxNat.zero) x8) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x5)))))))) (AxNat.succ AxNat.zero) x9)))))) CReal.zero x3)))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

Direct dependencies appear to the left. The current fact is in the center. Facts that depend directly on it appear to the right. The max of two constructed real max is the least upper bound am [generated] kernel theorem CRea A power-series term is dominate The power-series term function [generated] kernel theorem CRea [generated] kernel theorem CRea The Weierstrass M-test: a unifo Current fact
16 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.powerSeriesUniformConvergesOn

Kind
kernel-term
Status
checked

Supports: CReal.powerSeriesUniformConvergesOn is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command 
cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- powerSeriesUniformConvergesOn 2>/dev/null | grep -cE '^CReal\.powerSeriesUniformConvergesOn[[:space:]]'
Evidence notes

build_creal_prelude admits CReal.powerSeriesUniformConvergesOn through the trusted Kernel::add_declaration gate. theorem_dependency_inventory exits non-zero for a named filter matching nothing; grep -c asserts the exact tab-anchored line. Verified with /usr/bin/grep directly (not the ugrep-backed interactive `grep` function) against a freshly built --release binary on this tree, returning count 1. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.powerSeriesUniformConvergesOn

Kind
exhaustive-enumeration
Status
checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.powerSeriesUniformConvergesOn

Checker command 
cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free creal
Evidence notes

Re-measured on this tree: creal: axiom=0 opaque=0 quotient=0 total_trusted=0, exits 0 printing 'ok: creal trusted surface = 0'. That bounds every declaration in the creal environment, including CReal.powerSeriesUniformConvergesOn, since a declaration cannot depend on a trusted declaration the environment does not contain. --require-axiom-free <name> errors for a prelude never built by this run rather than silently passing on zero rows. --release is MANDATORY here.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/uniform_convergence.rs, declare_power_series_uniform_converges)",
  "source": "canonical type read via kernel_declaration_projection's own UNFILTERED emit mode (cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection, no --require-declaration flag), which prints, per constructed prelude, one TSV row per declaration whose last field is kernel.render_lean(declaration.ty()). That output was piped to a scratchpad file and the exact row for this declaration's creal prelude row was extracted and injected here programmatically (a Python script reading the TSV, never hand-transcribed); direct theorem dependencies were cross-read from the same run's direct_theorems column (second-to-last field) and matched against the ledger's own registered facts (by parsing each candidate fact's formal.statement for its declared theorem/def name) to populate depends_on. No new probe binary was written for this batch; crates/ source was not touched to produce this batch."
}