Original increasing-function endpoint jets

Abstract

The original all-order endpoint-jet assertion, with its monotone input class and one simultaneous smooth witness.

Definition 1.1 (unitInterval).

$$\mathrm{unitInterval}\left(\right)=\mathrm{Icc}\left(0,1\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.unitInterval (✓ std3).

Source. Repository-derived.

Commentary.

PnOriginal.unitInterval: The closed real interval [0,1]. Every endpoint derivative below is iteratedDerivWithin on this interval.

Definition 1.2 (primitive).

$$\forall g\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\forall x\in \mathrm{Real}\left(\right),\mathrm{primitive}\left(g,x\right)={\int }_0^{x}g\left(s\right)\mathrm{ds}\left(\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.primitive (✓ std3).

Source. Repository-derived.

Commentary.

PnOriginal.primitive: The variable s is bound by the interval integral; its orientation is from 0 to x.

Definition 1.3 (repeatedIntegral).

$$\forall k\in \mathrm{Nat}\left(\right),\forall g\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\mathrm{repeatedIntegral}\left(k,g\right)=\mathrm{iterate}\left(\mathrm{primitive}\left(\right),k,g\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.repeatedIntegral (✓ std3).

Source. Repository-derived.

Commentary.

PnOriginal.repeatedIntegral: Function.iterate applies primitive k times; k=0 returns g.

Definition 1.4 (jet).

$$\forall j\in \mathrm{Nat}\left(\right),\forall f\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\mathrm{jet}\left(j,f\right)=\mathrm{iteratedDerivWithin}\left(j,f,\mathrm{unitInterval}\left(\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.jet (✓ std3).

Source. Repository-derived.

Commentary.

PnOriginal.jet: The full one-sided endpoint convention is iteratedDerivWithin j f unitInterval, including j=0.

Definition 1.5 (W).

$$\forall n\in \mathrm{Nat}\left(\right),W\left(n\right)=\{b:\mathrm{Fin}\left(n+1\right)\to \mathrm{Real}\left(\right)\mid \exists f\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\left(\left(\mathrm{ContDiffOn}\left(\mathrm{Real}\left(\right),\mathrm{NatToWithTopNatInfinity}\left(n\right),f,\mathrm{unitInterval}\left(\right)\right)\wedge \mathrm{MonotoneOn}\left(\mathrm{jet}\left(n,f\right),\mathrm{unitInterval}\left(\right)\right)\right)\wedge \left(\exists x\in \mathrm{Real}\left(\right),x\in \mathrm{unitInterval}\left(\right)\wedge \left(\exists y\in \mathrm{Real}\left(\right),y\in \mathrm{unitInterval}\left(\right)\wedge \mathrm{jet}\left(n,f,x\right)\ne \mathrm{jet}\left(n,f,y\right)\right)\right)\right)\wedge \left(\forall j\in \mathrm{Fin}\left(n+1\right),\mathrm{jet}\left(\mathrm{val}\left(j\right),f,0\right)=0\wedge \mathrm{jet}\left(\mathrm{val}\left(j\right),f,1\right)=b\left(j\right)\right)\}$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.W (✓ std3).

Citation. Maxim R. Burke; Maleeha Haris; Madhavendra (2025). Repeated integrals of increasing functions. DOI: 10.48550/arXiv.2512.02151. URL: https://arxiv.org/abs/2512.02151v1.

Commentary.

PnOriginal.W: The source defines W_n using f in C^n[0,1], increasing and nonconstant D^n f, and all endpoint jets from 0 through n. Increasing means nondecreasing. NatToWithTopNatInfinity denotes the actual natural-order coercion in ContDiffOn. No strict input monotonicity or absolute continuity is assumed.

Definition 1.6 (P).

$$\forall n\in \mathrm{Nat}\left(\right),P\left(n\right)=\left(\mathrm{IsOpen}\left(W\left(n\right)\right)\wedge \left(\forall b\in \mathrm{Fin}\left(n+1\right)\to \mathrm{Real}\left(\right),b\in W\left(n\right)\Rightarrow \left(\exists f\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\left(\left(\left(\left(\mathrm{ContDiffOn}\left(\mathrm{Real}\left(\right),\infty ,f,\mathrm{unitInterval}\left(\right)\right)\wedge \left(\forall j\in \mathrm{Fin}\left(n+1\right),\mathrm{jet}\left(\mathrm{val}\left(j\right),f,0\right)=0\wedge \mathrm{jet}\left(\mathrm{val}\left(j\right),f,1\right)=b\left(j\right)\right)\right)\wedge \left(\forall x\in \mathrm{Real}\left(\right),x\in \mathrm{Ioo}\left(0,1\right)\Rightarrow 0<\mathrm{jet}\left(n+1,f,x\right)\right)\right)\wedge \mathrm{jet}\left(n+1,f,0\right)=1\right)\wedge \mathrm{jet}\left(n+1,f,1\right)=1\right)\wedge \left(\forall j\in \mathrm{Nat}\left(\right),n+1<j\Rightarrow \left(\mathrm{jet}\left(j,f,0\right)=0\wedge \mathrm{jet}\left(j,f,1\right)=0\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.P (✓ std3).

Citation. Maxim R. Burke; Maleeha Haris; Madhavendra (2025). Repeated integrals of increasing functions. DOI: 10.48550/arXiv.2512.02151. URL: https://arxiv.org/abs/2512.02151v1.

Commentary.

PnOriginal.P: The source’s (P_n) requires openness of W_n and one C-infinity witness for each b in W_n, with all original finite endpoint jets, positive order n+1 derivative in (0,1), value 1 at both endpoints at that order, and zero at both endpoints at every higher order.

Definition 1.7 (clamp).

$$\forall x\in \mathrm{Real}\left(\right),\mathrm{clamp}\left(x\right)=\max \left(0,\min \left(1,x\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.clamp (✓ std3).

Source. Repository-derived.

Commentary.

PnOriginal.clamp: Clamp to the original closed interval.

Definition 1.8 (extend).

$$\forall g\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\mathrm{extend}\left(g\right)=g\circ \mathrm{clamp}\left(\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.extend (✓ std3).

Source. Repository-derived.

Commentary.

PnOriginal.extend: Compose g with clamp.

Definition 1.9 (Vec).

$$\forall n\in \mathrm{Nat}\left(\right),\mathrm{Vec}\left(n\right)=\left(\mathrm{Fin}\left(n+1\right)\to \mathrm{Real}\left(\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Vec (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.Vec: The actual finite real-coordinate carrier.

Definition 1.10 (Center).

$$\mathrm{Center}\left(\right)=\mathrm{Subtype}\left(\mathrm{Icc}\left(0,1\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Center (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.Center: Center is the subtype of the closed real interval, so endpoints are retained.

Definition 1.11 (Width).

$$\mathrm{Width}\left(\right)=\mathrm{Subtype}\left(\mathrm{Ioi}\left(0\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Width (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.Width: Width is the subtype of positive real numbers.

Definition 1.12 (Param).

$$\mathrm{Param}\left(\right)=\mathrm{Prod}\left(\mathrm{Center}\left(\right),\mathrm{Width}\left(\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Param (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.Param: The center-width product subtype.

Definition 1.13 (gamma).

$$\forall n\in \mathrm{Nat}\left(\right),\forall t\in \mathrm{Real}\left(\right),\mathrm{gamma}\left(n,t\right)=\lambda k:\mathrm{Fin}\left(n+1\right),{\left(1-t\right)}^{\mathrm{val}\left(k\right)}$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.gamma (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.gamma: Every finite index is coerced to its natural value before exponentiation.

Definition 1.14 (raw).

$$\forall xi\in \mathrm{Real}\left(\right),\forall sigma\in \mathrm{Real}\left(\right),\forall t\in \mathrm{Real}\left(\right),\mathrm{raw}\left(xi,sigma,t\right)=\mathrm{expNegInvGlue}\left(t\right)\cdot \mathrm{expNegInvGlue}\left(1-t\right)\cdot \exp \left(-\frac{{\left(t-xi\right)}^2}{sigm{a}^2}\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.raw (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.raw: The explicit flat smooth weight times the Gaussian factor; exp is Real.exp.

Definition 1.15 (z).

$$\forall xi\in \mathrm{Real}\left(\right),\forall sigma\in \mathrm{Real}\left(\right),z\left(xi,sigma\right)={\int }_{t\in \mathrm{Icc}\left(0,1\right)}\mathrm{raw}\left(xi,sigma,t\right)\mathrm{dt}\left(\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.z (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.z: The Lean definition is the interval integral 0..1; the Icc volume integral is equal on these ordered endpoints.

Definition 1.16 (density).

$$\forall xi\in \mathrm{Real}\left(\right),\forall sigma\in \mathrm{Real}\left(\right),\forall t\in \mathrm{Real}\left(\right),\mathrm{density}\left(xi,sigma,t\right)=\frac{\mathrm{raw}\left(xi,sigma,t\right)}{z\left(xi,sigma\right)}$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.density (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.density: Division is real division.

Definition 1.17 (moment).

$$\forall n\in \mathrm{Nat}\left(\right),\forall xi\in \mathrm{Real}\left(\right),\forall sigma\in \mathrm{Real}\left(\right),\mathrm{moment}\left(n,xi,sigma\right)={\int }_{t\in \mathrm{Icc}\left(0,1\right)}\mathrm{smul}\left(\mathrm{density}\left(xi,sigma,t\right),\mathrm{gamma}\left(n,t\right)\right)\mathrm{dt}\left(\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.moment (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.moment: The actual Bochner moment vector over the closed interval.

Definition 1.18 (component).

$$\forall n\in \mathrm{Nat}\left(\right),\forall q\in \mathrm{Param}\left(\right),\mathrm{component}\left(n,q\right)=\mathrm{moment}\left(n,\mathrm{SubtypeToReal}\left(\mathrm{fst}\left(q\right)\right),\mathrm{SubtypeToReal}\left(\mathrm{snd}\left(q\right)\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.component (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.component: Both subtype projections are explicitly coerced to real numbers.

Definition 1.19 (S).

$$\forall n\in \mathrm{Nat}\left(\right),S\left(n\right)=\mathrm{PointedConeHull}\left(\mathrm{Real}\left(\right),\mathrm{range}\left(\lambda t:\mathrm{Center}\left(\right),\mathrm{gamma}\left(n,\mathrm{SubtypeToReal}\left(t\right)\right)\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.S (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.S: PointedConeHull is PointedCone.hull, with nonnegative scalar coefficients.

Definition 1.20 (T).

$$\forall n\in \mathrm{Nat}\left(\right),T\left(n\right)=\mathrm{PointedConeHull}\left(\mathrm{Real}\left(\right),\mathrm{range}\left(\mathrm{component}\left(n\right)\right)\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.T (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.T: The cone generated by the actual density components.

Definition 1.21 (mixture).

$$\forall c\in \mathrm{Finsupp}\left(\mathrm{Param}\left(\right),\mathrm{Subtype}\left(\lambda a:\mathrm{Real}\left(\right),0\le a\right)\right),\forall t\in \mathrm{Real}\left(\right),\mathrm{mixture}\left(c,t\right)=\sum _{q\in \mathrm{support}\left(c\right)}\mathrm{SubtypeToReal}\left(c\left(q\right)\right)\cdot \mathrm{density}\left(\mathrm{SubtypeToReal}\left(\mathrm{fst}\left(q\right)\right),\mathrm{SubtypeToReal}\left(\mathrm{snd}\left(q\right)\right),t\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.mixture (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.mixture: q is bound by the finite support sum; each nonnegative coefficient and parameter subtype is coerced to Real.

Definition 1.22 (endpointCut).

$$\forall delta\in \mathrm{Real}\left(\right),\forall t\in \mathrm{Real}\left(\right),\mathrm{endpointCut}\left(delta,t\right)=\mathrm{smoothTransition}\left(2-\frac{2\cdot t}{delta}\right)+\mathrm{smoothTransition}\left(2-\frac{2\cdot \left(1-t\right)}{delta}\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.endpointCut (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.endpointCut: The two reflected smooth transitions give the endpoint correction.

Definition 1.23 (cutMoment).

$$\forall n\in \mathrm{Nat}\left(\right),\forall delta\in \mathrm{Real}\left(\right),\mathrm{cutMoment}\left(n,delta\right)={\int }_{t\in \mathrm{Icc}\left(0,1\right)}\mathrm{smul}\left(\mathrm{endpointCut}\left(delta,t\right),\mathrm{gamma}\left(n,t\right)\right)\mathrm{dt}\left(\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.cutMoment (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.cutMoment: The moment vector of the endpoint correction.

Definition 1.24 (rho).

$$\forall delta\in \mathrm{Real}\left(\right),\forall c\in \mathrm{Finsupp}\left(\mathrm{Param}\left(\right),\mathrm{Subtype}\left(\lambda a:\mathrm{Real}\left(\right),0\le a\right)\right),\forall t\in \mathrm{Real}\left(\right),\mathrm{rho}\left(delta,c,t\right)=\mathrm{endpointCut}\left(delta,t\right)+\mathrm{mixture}\left(c,t\right)$$

Formalization. D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.rho (✓ std3).

Source. Repository-derived.

Commentary.

PnActualMixtureConsumer.rho: One density combines the endpoint correction with a finite nonnegative mixture.

Theorem 1.25 (The original all-order assertion).

$$\forall n\in \mathrm{Nat}\left(\right),P\left(n\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.result (✓ std3). ∎

Resolves. Problems/burke-haris-madhavendra-increasing-function-jets (proved) by D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.result.

Source. Repository-derived.

Acknowledgement. Maxim R. Burke; Maleeha Haris; Madhavendra (2025). Repeated integrals of increasing functions. DOI: 10.48550/arXiv.2512.02151. URL: https://arxiv.org/abs/2512.02151v1.

Commentary.

Conjecture 1.2, arXiv:2512.02151v1, p. 2: ‘(P_n) is true for all nonnegative integers n.’ The mathematical source proves exactly forall n : Nat, PnOriginal.P n.

The source’s W and P use their original closed-interval derivatives. The Stieltjes argument retains singular continuous and flat input derivatives and arbitrary positive mass. Reversed factorial coordinates connect all endpoint jets to one moment vector. The single witness is repeatedIntegral (n+1) rho; the same rho realizes every coordinate and every endpoint condition.

The coordinate-transform function sends each endpoint-jet vector b to its reversed factorial coordinates:

$\lambda n:\mathrm{Nat}\left(\right),\lambda b:\mathrm{Fin}\left(n+1\right)\to \mathrm{Real}\left(\right),\lambda k:\mathrm{Fin}\left(n+1\right),\mathrm{NatToReal}\left(\mathrm{factorial}\left(\mathrm{val}\left(k\right)\right)\right)\cdot b\left(\mathrm{rev}\left(k\right)\right)$

References

• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Center
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.P
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Param
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.S
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.T
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Vec
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.W
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.Width
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.clamp
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.component
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.cutMoment
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.density
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.endpointCut
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.extend
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.gamma
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.jet
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.mixture
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.moment
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.primitive
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.raw
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.repeatedIntegral
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.result
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.rho
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.unitInterval
• Truth anchor: D5/S3/Analytic/Interpolation/OriginalIncreasingFunctionJets.z