# Separate limits at every infinite endpoint and singularity

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-improper-integral/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-improper-integral-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Compute three explicit power-law improper integrals and distinguish principal value.

Only complete piecewise power laws, not general integrability from finite cutoffs.





## Givens and symbols


- algebra
- epsilon
- FTC
- definition_here
- log_integral_boundary


- G1 — One side: f(x)=3/x^2 for x≥2. Two sides: g(x)=2/|x|^2 for x≤-1, zero for -1<x<1, and 3/x^2 for x≥1.
- G2 — Singularity example: h(x)=(-x)^(-1/2) for -1≤x<0 and 2*x^(-1/2) for 0<x≤1, split at zero.


- A,B,b — independent infinite-end cutoffs
- \delta — one-sided singular cutoff
- \operatorname{PV} — symmetric principal value





## Rules and sources


- mko_definition · cited — A one-sided integral int_a^infinity f, from a to infinity, is the limit of finite-cutoff integrals as b→infinity; this slice declares f(x)=scale/x^p on [lower,infinity). The two-sided exact family declares f(x)=left_scale/|x|^p on x≤−1, f(x)=0 on −1<x<1 and f(x)=right_scale/x^p on x≥1; its tails must converge separately. An interior-singularity family explicitly gives both power-law pieces on [c−1,c+1] and splits at c. A symmetric principal value is insufficient. Absolute convergence is sufficient but not necessary, and apparently stable finite cutoffs do not prove convergence. · mko-improper-integral
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- epsilon · prerequisite — Convergence requires for every positive epsilon an integer N controlling every n≥N by a strict error bound; use the Archimedean property of the reals.
- FTC · prerequisite — For continuous power laws on finite closed intervals use the fundamental theorem of calculus; the derivative of -c/x is c/x^2, and that of 2sqrt(x) is x^(-1/2) for x>0.
- definition_here · prerequisite — An ordinary improper integral requires a finite limit of finite-cutoff integrals separately at each infinite endpoint and each side of an interior singularity, then adds them; principal value separately binds symmetric cutoffs.
- log_integral_boundary · prerequisite — For nonzero reals the derivative of log|x| is 1/x, and log B tends to infinity as B tends to infinity.





## Main derivation

S01 · impliesBefore

b>2

After

\int_2^b3x^{-2}\,dx=[-3/x]_2^b=3/2-3/b

Conditions: b>2

Rule: FTC · Uses: G1

Leaf basis: FTC

First integrate on a qualified finite interval, without directly substituting an infinite endpoint.



S02 · definitionBefore

3/b\to0\quad(b\to\infty)

After

\int_2^\infty3x^{-2}\,dx=3/2

Conditions: none

Rule: definition_here · Uses: S01

Leaf basis: definition_here

For any epsilon, b>3/epsilon controls the entire tail strictly, defining the one-sided integral.



S03 · impliesBefore

A>1,\ B>1

After

\int_{-A}^{-1}g=2-2/A,\quad\int_1^B g=3-3/B

Conditions: none

Rule: FTC · Uses: G1

Leaf basis: FTC

Use u=-x on the left and integrate directly on the right; the two cutoffs are independent.



S04 · definitionBefore

A\to\infty\text{ independently of }B\to\infty

After

\int_{-\infty}^{\infty}g=2+0+3=5

Conditions: none

Rule: definition_here · Uses: S03

Leaf basis: definition_here

Both tails exist separately, and only then are they added to the zero middle part.



S05 · impliesBefore

0<\delta<1

After

\int_{-1}^{-\delta}h=2-2\sqrt\delta,\quad\int_{\delta}^{1}h=4-4\sqrt\delta

Conditions: 0<\delta<1

Rule: FTC · Uses: G2

Leaf basis: FTC

Each side of the singularity has its own finite integral; substitute u=-x on the left and retain scale 2 on the right.



S06 · definitionBefore

\sqrt\delta\to0\quad(\delta\downarrow0)

After

\int_{-1}^{1}h=2+4=6

Conditions: none

Rule: definition_here · Uses: S05

Leaf basis: definition_here

The condition delta<epsilon^2 makes sqrt(delta)<epsilon; add the two finite one-sided limits.



S07 · impliesBefore

j(x)=1/x\quad(|x|\ge1),\qquad j(x)=0\quad(|x|<1)

After

\int_{-A}^{-1}j=-\log A,\quad\int_1^B j=\log B

Conditions: (\log|x|)'=1/x,\quad\log B\to\infty

Rule: log_integral_boundary · Uses: G1, log_integral_boundary

Leaf basis: log_integral_boundary

In this contrast example the two tails diverge; the derivative of log|x| is 1/x, supplying its finite antiderivative.



S08 · impliesBefore

A=B\Longrightarrow-\log A+\log A=0

After

\operatorname{PV}\int j=0\text{ but the ordinary improper integral does not exist}

Conditions: none

Rule: algebra · Uses: S07

Leaf basis: algebra

A zero symmetric principal value does not repair divergent individual tails and is not an ordinary improper integral.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S07 — The ordinary integral is rejected without denying the symmetric limit is zero.
- S07 · premise_audit · G1, log_integral_boundary — Only the stated logarithmic-antiderivative premise for this counterexample is used, not a new exp/log theory.
- S06 · premise_audit · S05 — A missing value at zero is not the obstruction; the one-sided integrability limits are the obligations.
- S05 · premise_audit · G2 — Using one symbol delta is convenient notation; the two one-sided limits must still exist separately.
- S04 · premise_audit · S03 — There is no symmetric cancellation; each side is independently qualified.
- S03 · premise_audit · G1 — Qualification must not rely on tying A and B together.
- S02 · premise_audit · S01 — This is not a conclusion from several close cutoff values.
- S01 · premise_audit · G1 — b>2 keeps the integrand continuous and denominators positive.





## Error controls and negative controls

Separate endpoint accountsRecord each infinite endpoint and singularity side separately.

Principal-value separationSymmetric cutoffs certify principal value, not independent tails.


- Divergent sides cancel into an ordinary integral. → reject — Neither one-sided limit of j is finite.
- Only one side of an interior singularity must converge. → reject — An ordinary improper integral requires both one-sided limits at each singularity.
- Several close large-cutoff values prove convergence. → reject — No bound for every later cutoff is supplied.





## Result and limitations

The three qualified improper integrals are 3/2, 5 and 6; contrast j has only symmetric principal value zero.







## Verification and source binding

1 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: fb00245eacaaeb6218a92f36d27aed6067e63e73e73270089daeadae5933b7f9
- original source SHA-256: fb00245eacaaeb6218a92f36d27aed6067e63e73e73270089daeadae5933b7f9
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-improper-integral-01.json)