kdrag.theories.real.seq

Module Attributes

cumsum_smul	cumsum_comm = cumsum(lambda x, cumsum(lammbda y, a[x,y]) ) ???
cauchy_mod	is_convergent = kd.define(

Functions

test()

Classes

Series()

class kdrag.theories.real.seq.Series

Bases: object

powers = powers

kdrag.theories.real.seq.cauchy_mod = cauchy_mod

is_convergent = kd.define(

“is_convergent”, [a], kd.QForAll(

[eps], eps > 0, smt.Exists(

[N], kd.QForAll([m], m > N, smt.Exists([x], real.abs(a[m] - x) < eps))

),

),

)

kdrag.theories.real.seq.cumsum_smul = |= ForAll([a, x],        cumsum(RSeq.smul(x, a)) == RSeq.smul(x, cumsum(a)))

cumsum_comm = cumsum(lambda x, cumsum(lammbda y, a[x,y]) ) ???

# TODO: unstable @kd.Theorem(

“forall (a : RSeq) (x : Real) (n : Int), cumsum (smul x a) n = smul x (cumsum a) n”

) def cumsum_smul(l):

a, x, n = l.fixes() l.induct(n)

# n < 0 # TODO: These induction cases look disgusting with too many lambdas. l.fix() l.simp() l.intros() l.unfold(cumsum, smul) l.simp() l.auto(by=[smul.defn, cumsum.defn])

# n == 0 l.auto(by=[smul.defn, cumsum.defn])

# n > 0 l.fix() l.simp() l.unfold(cumsum, smul) l.simp() l.unfold(cumsum, smul) l.simp() l.auto(by=[smul.defn, cumsum.defn])

Type:

# TODO

Parameters:

args (smt.ExprRef | Proof)

kdrag.theories.real.seq.test()

>>> True
True

Theorem	Statement
real.seq.abs_ext	∀a : ℤ → ℝ, n : ℤ, rseq.abs(a)[n] = |a[n]|
real.seq.abs_ge_0	∀a : ℤ → ℝ, n : ℤ, rseq.abs(a)[n] ≥ 0
real.seq.abs_le_finsum_abs	∀a : ℤ → ℝ, N : ℤ,   N ≥ 0 →   ∀n : ℤ,     n ≥ 0 → n ≤ N → rseq.abs(a)[n] ≤ finsum(rseq.abs(a), N)
real.seq.add_assoc	∀A₀ B₀ C₀ : ℤ → ℝ, A₀ + B₀ + C₀ = A₀ + (B₀ + C₀)
real.seq.add_comm	∀A₀ B₀ : ℤ → ℝ, A₀ + B₀ = B₀ + A₀
real.seq.add_mul	∀A₀ B₀ C₀ : ℤ → ℝ, (A₀ + B₀) * C₀ = A₀ * C₀ + B₀ * C₀
real.seq.add_zero	∀A₀ : ℤ → ℝ, A₀ + RSeq.zero = A₀
real.seq.cumsum_add	∀a b : ℤ → ℝ, n : ℤ,   cumsum(a + b)[n] = cumsum(a)[n] + cumsum(b)[n]
real.seq.cumsum_const	∀x : ℝ, n : ℤ,   n ≥ 0 → cumsum(RSeq.const(x))[n] = to_real(n + 1) * x
real.seq.cumsum_mono	∀a b : ℤ → ℝ, m : ℤ,   (∀n : ℤ, n ≥ 0 → a[n] ≤ b[n]) →   m ≥ 0 → cumsum(a)[m] ≤ cumsum(b)[m]
real.seq.cumsum_smul (admitted)	∀a : ℤ → ℝ, x : ℝ,   cumsum(RSeq.smul(x, a)) = RSeq.smul(x, cumsum(a))
real.seq.cumsum_zero	∀n : ℤ, cumsum(RSeq.zero)[n] = 0
real.seq.dot_add	∀a b c : ℤ → ℝ, n : ℤ,   rseq.dot(n, a + b, c) = rseq.dot(n, a, c) + rseq.dot(n,     b,     c)
real.seq.dot_comm	∀a b : ℤ → ℝ, n : ℤ, rseq.dot(n, a, b) = rseq.dot(n, b, a)
real.seq.dot_smul	∀x : ℝ, a b : ℤ → ℝ, n : ℤ,   rseq.dot(n, RSeq.smul(x, a), b) = x * rseq.dot(n, a, b)
real.seq.dot_zero	∀a : ℤ → ℝ, n : ℤ, rseq.dot(n, RSeq.zero, a) = 0
real.seq.finsum_add	∀a b : ℤ → ℝ, n : ℤ,   finsum(a + b, n) = finsum(a, n) + finsum(b, n)
real.seq.finsum_smul	∀a : ℤ → ℝ, x : ℝ, n : ℤ,   finsum(RSeq.smul(x, a), n) = x * finsum(a, n)
real.seq.finsum_succ	∀a : ℤ → ℝ, n : ℤ,   n ≥ 0 → finsum(a, n + 1) = finsum(a, n) + a[n + 1]
real.seq.finsum_zero	∀n : ℤ, finsum(RSeq.zero, n) = 0
real.seq.has_lim_inv	has_lim(λn : ℤ, 1 / to_real(n), 0)
real.seq.kron_diff	∀n m : ℤ, n ≠ m → krondelta(n)[m] = 0
real.seq.kron_same	∀n : ℤ, krondelta(n)[n] = 1
real.seq.lim_const	has_lim(RSeq.const(x), x)
real.seq.lim_defn	is_conv(A₀) → has_lim(A₀, lim(A₀))
real.seq.lim_unique	∀a : ℤ → ℝ, x y : ℝ, has_lim(a, x) → has_lim(a, y) → x = y
real.seq.lim_zero	has_lim(RSeq.zero, 0)
real.seq.max_bound	∀a : ℤ → ℝ, n i : ℤ,   n ≥ 0 → i ≥ 0 → i ≤ n → a[i] ≤ max(a)[n]
real.seq.max_ge_self	∀a : ℤ → ℝ, i : ℤ, max(a)[i] ≥ a[i]
real.seq.max_prefix_bound	∀a : ℤ → ℝ, n : ℤ,   n ≥ 0 → ∀i : ℤ, i ≥ 0 → i ≤ n → a[i] ≤ max(a)[n]
real.seq.max_suffix_bound	∀a : ℤ → ℝ, n : ℤ,   n ≤ 0 → ∀i : ℤ, n ≤ i → i ≤ 0 → a[i] ≤ max(a)[n]
real.seq.mul_add	∀A₀ B₀ C₀ : ℤ → ℝ, A₀ * (B₀ + C₀) = A₀ * B₀ + A₀ * C₀
real.seq.mul_assoc	∀A₀ B₀ C₀ : ℤ → ℝ, A₀ * B₀ * C₀ = A₀ * (B₀ * C₀)
real.seq.mul_comm	∀A₀ B₀ : ℤ → ℝ, A₀ * B₀ = B₀ * A₀
real.seq.mul_one	∀A₀ : ℤ → ℝ, A₀ * RSeq.const(1) = A₀
real.seq.mul_zero	∀A₀ : ℤ → ℝ, A₀ * RSeq.zero = RSeq.zero
real.seq.rev_const	∀x : ℝ, RSeq.rev(RSeq.const(x)) = RSeq.const(x)
real.seq.rev_id	RSeq.rev(RSeq.id) = -RSeq.id
real.seq.rev_rev	∀A₀ : ℤ → ℝ, RSeq.rev(RSeq.rev(A₀)) = A₀
real.seq.rev_shift	∀n : ℤ, a : ℤ → ℝ,   RSeq.rev(RSeq.shift(a, n)) = RSeq.shift(RSeq.rev(a), -n)
real.seq.rev_zero	RSeq.rev(RSeq.zero) = RSeq.zero
real.seq.shift_shit	∀n m : ℤ, a : ℤ → ℝ,   RSeq.shift(RSeq.shift(a, n), m) = RSeq.shift(a, n + m)
real.seq.smul_mul	∀x : ℝ, a b : ℤ → ℝ,   RSeq.smul(x, a) * b = RSeq.smul(x, a * b)