Skip to content

An integral across a jump is split at the jumps, never taken through an antiderivative - #1215

Merged
Rafael-SOWNet merged 2 commits into
masterfrom
floor-split
Sep 8, 2026
Merged

Rafael-SOWNet merged 2 commits into
masterfrom
floor-split

Conversation

@Rafael-SOWNet

@Rafael-SOWNet Rafael-SOWNet commented Sep 8, 2026 •

Copy link
Copy Markdown
Member

Part of #1212 — item 3 of the plan in my comment there, generalised on the review here: the mechanism is continuity, not the floor.

The wrong answers

F(b) - F(a) is the integral only where F is continuous on [a, b], and the definite integral evaluated an antiderivative at its bounds whatever the integrand did in between. Measured on master:

master
integral(piecewise(2x provided x <= 1/2, 2 - 2x), x, 0, 1) — the tent map, 1/2 1 — the first case's antiderivative at both ends
integral(piecewise(x provided x < 1, x^2), x, 0, 2) — 17/6 piecewise(2 provided x < 1, 8/3) — the integration variable still in the answer
integral(x - floor(x), x, 0, 3) — 3/2 0
integral((x - floor(x))^2, x, 0, n) (n - floor(n))^3 / 3 — wrong for every whole n but 0

The piecewise ones come from the generic argument expansion in Integralf.InnerSimplify, which distributes the integral into the cases of a piecewise, and under a provided, whether or not their conditions mention the integration variable. The floor ones come from the rules taking the floor for a constant.

What changes

BreakpointIntegration (renamed from the first version's UnitIntervalIntegration): an integrand that can jump never goes through an antiderivative between two bounds.

  • Finitely many breakpoints — a piecewise or a provided whose conditions compare the variable with numbers: the range is cut at the breakpoints inside it; on each piece the case that holds at the piece's midpoint replaces the piecewise (exact, since the condition has no other place to change), and the piece integrates through the antiderivative; the pieces add. A provided whose condition fails on a piece makes the integral undefined there, and it is left as written.
  • Infinitely many, evenly spaced — floor(x) or ceil(x): the same split written as a sum over unit intervals, which the summation's closed forms (A polynomial summand is summed in closed form (#717) #1152, A series in a power over a factorial is summed in closed form #1213) answer; +oo allowed; a numeric bound that is not whole contributes the piece up to the nearest whole number.
  • A condition against a symbol, or a symbolic bound: left as written. The pieces depend on where the jumps fall, and answering across them is what this exists to stop.
  • A piecewise whose conditions do not mention the variable is a constant here and takes the antiderivative as before; sgn and abs have continuous antiderivatives and are untouched.
  • One guard at the integral node: where the integrand can jump and the split declines, the integral stays as written instead of being handed to the expansion that produced the leaking answers.

Two details that cost a round each: the fractional part is substituted as a unit, because written out it arrives as n + t - n, which since #1174 is a conditional zero rather than nothing; and ExponentialSeries sees through the condition a division by a factorial of the index carries, which holds for every whole index in the range.

Measured

Both columns on builds — 4fd6dda5 / 60545afa against this branch:

was is
tent map over [0, 1] 1 1/2
piecewise(x provided x < 1, x^2) over [0, 2]; three cases over [-1, 2] a piecewise in x; a piecewise in x 17/6; 6
piecewise(x provided x < a, 0) over [0, 2]; the tent map over [0, t] piecewises in x left as written
x provided x > 0 over [0, 1]; over [-1, 1] 1/2 provided x > 0; 0 provided x > 0 1/2; left as written
x - floor(x) over [0, 3]; (x - floor(x))^2 over [0, 4]; over [0, n] 0; 0; (n - floor(n))^3 / 3 3/2; 4/3; left as written (2 once n = 6)
(x - floor(x)) / floor(x)! over [1, +oo) — question I.2 left as written (e - 1) / 2
floor(x) over [0, 5], floor(x) * x over [0, 3], floor(x) / (floor(x) + 1)! over [0, +oo) left as written 10, 13/2, 1
floor(x) over [1/2, 2], x - floor(x) over [0, 5/2], ceil(x) - x over [1/2, 2] left as written 1, 9/8, 5/8
sgn(x) over [-1, 2], abs(x - 1) over [0, 3], the rational integral of I.5 1, 5/2, its value the same

What this does not do yet

The same expansion distributes sum, product, derivative and limit into a piecewise's cases with the bound variable in the conditions; a summation over an index-dependent condition is the next one worth measuring. And a piecewise nested inside another's condition (what composing the tent map five times produces, question I.3) is not read as breakpoints yet.

Checks

BreakpointIntegrationTest: seven piecewise integrals, the provided case, the constant-condition case, the two declines, the sheet's integral, five whole-bound and six non-whole-bound step integrals, the symbolic bound, two non-shapes, three unaffected integrands. Full suite in two chunks: 8344 and 1386 pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

@Happypig375

Copy link
Copy Markdown
Member

This is really about continuity, right? Instead of special casing floor and ceil, you should use a generalized approach that also handles piecewises (they can be continuous or not!)

@Rafael-SOWNet

Copy link
Copy Markdown
Member Author

Agreed — the invariant underneath is that F(b) - F(a) needs F continuous on [a, b], and floor and ceil are only the case with infinitely many evenly spaced breakpoints, which is why that one ends in a sum. A piecewise has finitely many, at its case boundaries; sgn has one. I'll generalise this PR to a breakpoint split: collect where the integrand can jump inside the range (piecewise case boundaries, sgn's zero, the integers for a floor or ceiling of the variable), integrate between them with the step known on each piece, and decline where a breakpoint is symbolic rather than answer across it. Measuring what the library does today for piecewise integrals across a boundary first, since I expect the same wrong answer there.

Rafael-SOWNet and others added 2 commits September 8, 2026 12:13
…an antiderivative

integral(x - floor(x), x, 0, 3) answered 0: the rules find an
antiderivative of an integrand with floor(x) in it by taking the floor
for a constant, right between two of its jumps and wrong across one, and
the definite integral evaluated that at the bounds. (x - floor(x))^2 from
0 to 4 was 0 where it is 4/3, and from 0 to a symbolic n was
(n - floor(n))^3 / 3, wrong for every whole n but 0.

An integrand with floor(x) or ceil(x) of the variable no longer goes
through an antiderivative between two bounds. Between whole bounds it is
split into unit intervals -- on each the floor is n, the ceiling n + 1
and x is n + t -- and the integral is a sum over n of an integral over t
with no step in it, which the summation's closed forms then answer; a
numeric bound that is not whole contributes the piece up to the nearest
whole number, on which the step is one known constant; a symbolic bound
is left as written. Offered only where every piece resolves. The
fractional part is substituted as a unit, since written out it arrives
as n + t - n, which is a conditional zero and not nothing (#1174); and
the series reader accepts the condition a division by a factorial of the
index carries, which holds for every whole index in range.

Question I.2 of #1212: integral((x - floor(x)) / floor(x)!, x, 1, +oo)
is (e - 1) / 2. BREAKING-CHANGES.md has the rows, measured on both
builds.

Part of #1212.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
…an antiderivative

F(b) - F(a) is the integral only where F is continuous on [a, b], and
the definite integral evaluated an antiderivative at its bounds whatever
the integrand did in between. Three shapes jump. A piecewise whose
conditions mention the variable: the generic argument expansion built
the antiderivative case by case and handed it back with the integration
variable still inside it -- the tent map over [0, 1] answered 1, and
piecewise(x provided x < 1, x^2) over [0, 2] answered piecewise(2
provided x < 1, 8/3). A provided on the variable, distributed the same
way. And floor(x) or ceil(x), taken for constants across their jumps:
x - floor(x) from 0 to 3 answered 0, (x - floor(x))^2 from 0 to 4
answered 0 where it is 4/3, and from 0 to a symbolic n answered
(n - floor(n))^3 / 3.

An integrand that can jump never goes through an antiderivative between
two bounds now (BreakpointIntegration, and a guard at the integral node
so that a declined split stays an integral rather than being handed to
the expansion). Finitely many breakpoints -- a piecewise or a provided
whose conditions compare the variable with numbers -- cut the range, and
on each piece the case that holds at the midpoint is integrated through
the antiderivative and added; a provided that fails on a piece leaves
the integral as written. Infinitely many, evenly spaced -- a floor or a
ceiling -- are the same split as a sum over unit intervals, which the
summation's closed forms answer, with the pieces up to the nearest whole
number for a numeric bound that is not whole. A condition against a
symbol or a symbolic bound is left as written. Offered only where every
piece resolves.

The fractional part is substituted as a unit, since written out it
arrives as n + t - n, which is a conditional zero and not nothing
(#1174); and the series reader accepts the condition a division by a
factorial of the index carries, which holds for every whole index in
range.

Question I.2 of #1212 -- integral((x - floor(x)) / floor(x)!, x, 1, +oo)
is (e - 1) / 2 -- generalised on the review of #1215. BREAKING-CHANGES.md
has the rows, measured on both builds.

Part of #1212.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet Rafael-SOWNet changed the title An integral across a step is split at the jumps, never taken through an antiderivative An integral across a jump is split at the jumps, never taken through an antiderivative Sep 8, 2026
@Rafael-SOWNet

Copy link
Copy Markdown
Member Author

Generalised, and retitled: the PR is now the breakpoint split, with the floor as one instance of it.

What it reads as a break, in BreakpointIntegration (renamed from UnitIntervalIntegration): a piecewise whose conditions mention the variable, a provided whose condition does, and floor/ceil of the variable. Finitely many breakpoints (the piecewise and provided cases, conditions comparing the variable with numbers) cut the range; on each piece the case that holds at the piece's midpoint replaces the piecewise — exact, since the condition has no other place to change — and the piece goes through the antiderivative; the pieces add. The floor and ceiling have infinitely many evenly spaced ones, so they are the same split written as a sum over unit intervals, which the closed forms answer. A condition against a symbol, or a symbolic bound, is left as written.

What it fixed beyond the floor, measured on master: the tent map piecewise(2x provided x <= 1/2, 2 - 2x) over [0, 1] answered 1 (the first case's antiderivative at both ends), and piecewise(x provided x < 1, x^2) over [0, 2] answered piecewise(2 provided x < 1, 8/3), with the integration variable still in the answer. Both come from the generic argument expansion in Integralf.InnerSimplify, which distributes the integral into a piecewise's cases and under a provided whatever their conditions say — so there is also a guard at the node: an integrand that can jump is never handed to that expansion, and a declined split stays an integral. sgn and abs are untouched, since their antiderivatives are continuous.

Not in this PR: the same expansion distributes sum, product, derivative and limit the same way; a summation with an index-dependent condition is the next one to measure. And a piecewise inside another piecewise's condition (what composing the tent map produces, I.3) is not read as breakpoints yet.

Rebased onto master with #1216 and #1217; one expectation moved with the perfect-power rule (ln(16/9) for the I.5 integral). Full suite in two chunks: 8344 and 1386 pass; rows in BREAKING-CHANGES.md measured on both builds.

@Rafael-SOWNet

Copy link
Copy Markdown
Member Author

Measured the summation side I said was next, on this branch. It is not wrong: a numeric range expands term by term before the argument expansion sees it, so sum(piecewise(k provided k < 3, 0), k, 0, 5) is 3, sum(piecewise(1 provided k <= 2, 2), k, 1, 4) is 6, product(piecewise(k provided k <= 2, 1), k, 1, 4) is 2, and a symbolic bound stays a sum. The limits are right too — limit(piecewise(1 provided x < 0, 2), x, 0) is NaN since the sides disagree, and 0 for piecewise(x provided x < 0, x^2). So the integral was the one binder that went through an antiderivative of the cases, and this PR is the whole of that defect.

One thing the measurement did turn up, a size rather than a value: sum(piecewise(k provided k < a, 0), k, 0, 5) answers a piecewise of 32 cases — every subset of {1 < a, …, 5 < a} as a conjunction, including the impossible ones — where it is six: 0 provided a <= 1, 1 provided a <= 2, 3, 6, 10, 15. The product of n two-case terms is 2^n cases and the conditions are never collapsed. That is the piecewise-flattening question (I.3 of #1212) and not this PR; noting it there.

@Rafael-SOWNet
Rafael-SOWNet merged commit fb7fe27 into master Sep 8, 2026
31 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the floor-split branch September 8, 2026 12:52
Rafael-SOWNet added a commit that referenced this pull request Sep 8, 2026
* A geometric series is summed in closed form

sum(x^k, k, 0, +oo) was left as written, and so was every other sum of
a power with the index in the exponent: sum(2^(-k), k, 0, +oo),
sum(x^k, k, 0, n), and sum(2^k, k, 0, 200), whose range is past the
hundred terms that are expanded one by one.

A summand that is C * b^(m k + s) -- a base free of the index, an
exponent that is the index times a whole number plus something free of
it, every other factor free of the index -- is summed as a geometric
series with the ratio b^m. Between two bounds the sum is
C b^s (r^a - r^(b + 1)) / (1 - r) where the range is not empty and the
ratio is not 1, the number of terms times the constant where the ratio
is 1, and 0 for an empty range; a numeric ratio picks its branch and a
symbolic one is offered all three as a piecewise, the way a polynomial
summand is offered the empty range. To +oo the series converges exactly
when |r| < 1: a numeric ratio outside that is left as written, and a
symbolic ratio carries provided abs(r) < 1. A polynomial factor in the
index is not this family and stays as written.

r^0 is written as 1 rather than built, since a power carries
`provided not r = 0` and the sum at r = 0 is its first term. Three
tests that pinned sum(2^k, k, 1, n) as an example of a sum without a
closed form now use k^k; the step integral of 2^(-floor(x)) over
[0, +oo), which #1215 left as written for want of this sum, is 2.

The sum question I.2 of #1212 leaves. BREAKING-CHANGES.md has the rows,
measured on both builds.

Part of #1212.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

* The declined step integral is a TODO, not a verdict: sum(n^n) diverges to +oo

The test pinned integral(floor(x)^floor(x), x, 1, +oo) staying as written
with a comment that said the sum cannot be answered. It can: its terms
do not tend to zero, so the series diverges, and with positive terms
the answer is +oo. What is missing is a divergence test, and the
comment now says so. From the review of #1218.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

---------

Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants