Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Differentiation under an improper multiple integral under an integrable derivative bound

Statement

Let D⊆Rn be open and I⊆R be an open interval. Suppose f and ∂tf are continuous on D×I, one slice ft∗ is absolutely improperly integrable, and for every compact interval C⊆I there is a nonnegative improperly integrable gC with ∣∂tf(x,t)∣≤gC(x) for x∈D and t∈C. Then every slice is absolutely improperly integrable, the function F(t)=∫Df(x,t) dx is continuously differentiable, and

F′(t)=∫D∂tf(x,t) dx.

The parameter derivative may be passed through the improper multiple integral under an integrable uniform derivative bound.

Facts & Assumptions

Given: The domain, interval, integrand, derivative, base slice, and dominators of the Statement; fix t0∈I.

[L1]

The mean value theorem gives an interior c with h(b)−h(a)=h′(c)(b−a) for a continuous function differentiable inside an interval (The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a)).

[L2]

If locally integrable slices ut satisfy ∣ut∣≤g on a compact parameter set, where g≥0 and ∫Dg<+∞, then their improper-integral tails outside one compact Jordan core are uniformly small (An integrable dominator gives uniform tail control on every compact parameter set).

[L3]

If u:D×I→R is continuous and locally dominated near every parameter by a nonnegative improperly integrable function, then t↦∫Du(x,t) dx is continuous in the relative topology (Locally dominated parameter-dependent improper multiple integrals are continuous).

[L4]

If ∣u∣≤g and g has finite nonnegative improper integral, then u is absolutely improperly integrable (Comparison and absolute comparison tests for improper multiple integrals).

[L5]

A continuous map from a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L6]

Proper multidimensional integrals are linear and satisfy ∣∫u∣≤∫∣u∣ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L7]

If u is absolutely improperly integrable, its proper integrals along every compact Jordan exhaustion converge to ∫Du (Absolute convergence makes signed improper multiple integrals independent of exhaustion).

Proof

technique · direct
1.1L1L4L6L7algebra

On the compact parameter interval between t∗ and any t∈I, [L1] gives ∣f(x,t)−f(x,t∗)∣≤∣t−t∗∣gC(x) pointwise. Fact [L4] makes the difference absolutely improperly integrable. Proper linearity in [L6] along one exhaustion and convergence in [L7] show that a sum of two absolutely improperly integrable functions is again absolutely improperly integrable, so ft=ft∗+(ft−ft∗) is absolutely improperly integrable.

1.2L1L2L5

For nonzero h with t0+h∈I, [L1] bounds the difference quotient qh(x):=(f(x,t0+h)−f(x,t0))/h by one integrable dominator. On a compact Jordan core, [L5] and [L1] make qh→∂tf(⋅,t0) uniformly as h→0.

2.1step 1.2L2L6L7

Use [L2] to make the tails of both qh and ∂tf(⋅,t0) uniformly small, then use the uniform convergence from step 1.2 on the core and [L6]. It follows that ∫Dqh→∫D∂tf(x,t0) dx. On every compact member of one exhaustion, proper linearity in [L6] gives ∫qh=(∫ft0+h−∫ft0)/h; applying [L7] to the three absolutely integrable functions passes this identity to D. Hence the left side is the difference quotient of F, proving the asserted derivative formula.

3.1step 2.1L3L4∎

Apply [L4] to each derivative slice and [L3] to the continuous integrand ∂tf, using the same local dominators, to see that the derivative integral is continuous in t. Thus F is C1 on I.

Depends on

Used by

Dependency tree · two levels

40 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources