Proof index
The elementary proof providers have exact earlier-programme routes in C10/C20, with public PDF destinations and editable TeX passages. The author English edition remains available. Human source text and figures stay external to this CC0 export and retain their own terms.
Each entry gives a mathematical scope, source and prerequisites. Local companions provide the finite-dimensional and calculus arguments. Notation and definitions explain the conventions.
A0
Ordered real field with least-upper-bound axiom, natural-number induction, finite arithmetic, sets/functions/sequences and metric/open/closed/compact definitions. No unproved construction/uniqueness theorem for R is used.
P6.0
P6.0. The Archimedean argument
P6.1
P6.1. Subsequence indices
P6.3-tail
First paragraph only: tail extrema bounds and increasing infima
P6.3-subtract
Last paragraph only: subtraction of convergent sequences
P6.4-ball
First paragraph: closed balls
P8-root
Existence, uniqueness, monotonicity and continuity only; smoothness still imports the calculus chain/product rules
L2.1.10-inc
The fully written increasing half only; decreasing half is P6.2
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 61 · Exact editable TeX passage
L2.2.1
Squeeze lemma
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 67 · Exact editable TeX passage
L2.2.3
Nonstrict inequalities pass to limits
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 68 · Exact editable TeX passage
L7.1.4
Real finite-dimensional Cauchy–Schwarz by sum of squares
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 275 · Exact editable TeX passage
L7.2.6
Open unions and finite intersections
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 283 · Exact editable TeX passage
L7.2.9-open
Only the complete open-ball half; closed-ball half is P6.4-ball
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 284 · Exact editable TeX passage
L7.4.2
A convergent metric sequence is Cauchy
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 298 · Exact editable TeX passage
D0
Vector-space, norm, derivative, matrix and higher-regularity definitions; zero-dimensional conventions.
P6.2
P6.2. Decreasing limits
L7.5.2
Metric continuity and preservation of sequence limits
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 308 · Exact editable TeX passage
L3.1.7
Full function/sequential-limit equivalence.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 124 · Exact editable TeX passage
L2.1.17
Subsequences preserve real limits; index induction supplied in P6.1
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
L7.4.10
Lebesgue covering lemma proved directly from sequential compactness
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 301 · Exact editable TeX passage
L2.2.5
Full addition, multiplication and reciprocal proofs; subtraction completed locally
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 69 · Exact editable TeX passage
L7.1.5
Euclidean distance satisfies triangle inequality; positivity and symmetry follow from its displayed sum of squares
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 276 · Exact editable TeX passage
P6.6
Closed-set complement rules and empty compactness case, plus the full metric-majorant convergence equivalence used by Theorem 7.4.11.
L7.3.11
Metric and neighbourhood definitions of convergence agree
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 295 · Exact editable TeX passage
L8.1.13
Uniqueness of basis coordinates.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 12 · Exact editable TeX passage
P7
Well-defined determinant permutation parity and sign multiplication.
P10.6-zero
Trivial inverse and implicit cases in zero dimensions, without undefined norm reciprocals.
I0
Darboux/Riemann definitions, vector integrals and orientation; finite-interval scope.
L2.3.2
Existence and bounds of liminf/limsup, with explicit local omitted steps
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 79 · Exact editable TeX passage
P12.1
Supremum/infimum order, scaling, sums and cofinal-subset operations used in integral proofs.
L2.2.11
For 0<c<1, c^n tends to zero; the c>1 part is not needed
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 74 · Exact editable TeX passage
L7.3.9
Coordinatewise and Euclidean convergence agree for every finite n
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 295 · Exact editable TeX passage
P9.2
Norm metric, reverse triangle, convex balls and R-to-R^m operator norm.
P10.1
Scalar and finite-coordinate limit laws, order and squeeze; explicit Fermat sequences.
L7.2.19
Closure is closed and contains the set
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 288 · Exact editable TeX passage
L7.4.11
Sequential compactness and the finite-subcover definition are equivalent
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 302 · Exact editable TeX passage
L7.3.12
Closed sets contain convergent sequence limits
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 296 · Exact editable TeX passage
P9.1
Subspaces, linearity, extension, matrix units, corrected denominator and empty lists.
E0
Complex coordinate operations, series and factorial definitions.
L2.3.4-upper
Fully written limsup subsequence proof; no assumption of the omitted liminf proof
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 81 · Exact editable TeX passage
L5.1.2
Darboux sum bounds and existence of their defining finite extrema.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 194 · Exact editable TeX passage
P12.2-upper
Upper-refinement proof and correction of the q=0 interval-length index.
P6.5
Finite geometric bound, Cauchy threshold and direct limit at the fixed point
L3.3.7
Complete bisection proof of a zero between strictly signed endpoints.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 141 · Exact editable TeX passage
L7.2.22
Every ball about a point of the closure meets the set
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 289 · Exact editable TeX passage
L7.5.5
Continuous image of a compact set is compact
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 309 · Exact editable TeX passage
L7.5.11
Continuous maps on compact spaces are uniformly continuous
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 311 · Exact editable TeX passage
P6.4-complete
Second paragraph: a closed subset of a complete metric space is complete
L8.1.14
All six finite-dimensional exchange, basis and subspace assertions.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 13 · Exact editable TeX passage
L8.1.16
Inverse linearity, with the other four parts completed locally.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 15 · Exact editable TeX passage
L8.1.17
Determination and extension from basis values, including the omitted linearity check.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
R0
Coordinate rectangles, volume and Darboux definitions; finite-vector/complex integral definitions.
P6.3-inf
Second paragraph only: reflection proves the omitted liminf subsequence assertion
L2.3.8
Bolzano–Weierstrass via the first complete proof. Alternate bisection proof also read, but not needed by this graph.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 84 · Exact editable TeX passage
L5.1.7
Both refinement inequalities; omitted upper half supplied by P12.2.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 196 · Exact editable TeX passage
L7.6.2
Complete-space contraction principle with finite geometric bound and explicit limit step
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 317 · Exact editable TeX passage
L3.3.8
Both strict orientations of the intermediate value theorem.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 142 · Exact editable TeX passage
L7.4.9
Compact subsets of every metric space are closed and pairwise bounded, including the empty ambient space; equivalence with the author ball-centre definition whenever the ambient space is nonempty.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
P9.4
Gram-Schmidt and orthonormal coordinates on the invariant complement in Q5.
P9.5
Injective dimension bound, nonzero projection kernel and invariance under bijections.
L8.1.18
Injectivity iff surjectivity for finite-dimensional endomorphisms.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 17 · Exact editable TeX passage
P17.1
Grid coverage and volume additivity, singleton-side and dimension-zero cases, and the omitted upper refinement.
L10.1.14
Full rectangle-diameter inequality.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 108 · Exact editable TeX passage
J0
Outer measure, null sets, Jordan sets and zero extensions are explicit definitions; dimension-zero convention.
L2.3.5
Convergence iff the two tail limits agree
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 83 · Exact editable TeX passage
P1
P1. The finite-dimensional step
L5.1.8
Lower Darboux integral <= upper integral, with common-refinement proof.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 197 · Exact editable TeX passage
L5.2.1
Additivity of upper and lower integrals on adjacent intervals.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 204 · Exact editable TeX passage
L7.5.6
Continuous real functions on nonempty compact spaces attain both extrema
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 310 · Exact editable TeX passage
L10.1.2
Full Darboux bounds, with the used volume exercise now proved.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 103 · Exact editable TeX passage
L10.4.1
Continuity iff zero oscillation; full proof.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 131 · Exact editable TeX passage
L10.4.2
Closed positive oscillation level sets on a closed domain; full proof.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 132 · Exact editable TeX passage
U001-DEF
Uniform supports, parameter compacta, Fourier convention, symbols, ordinary densities, chart definition and dimension-zero conventions.
L2.4.5
Cauchy sequences are bounded and real Cauchy sequences converge
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 91 · Exact editable TeX passage
L5.1.10
Integral bound is the just-proved Darboux bound with equal lower/upper integrals, as Definition 5.1.9 specifies.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 198 · Exact editable TeX passage
L5.1.11
Exact constant integral, proved by coinciding upper/lower bounds.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 198 · Exact editable TeX passage
L5.1.13
Arbitrarily small Darboux gaps imply integrability.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 200 · Exact editable TeX passage
P12.2-criterion
Necessary small-gap criterion and common partition for finitely many integrable functions.
L5.2.4-positive
The actually written nonnegative-scalar proof only; omitted negative and sum cases are supplied locally.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 206 · Exact editable TeX passage
L5.2.6
Integral monotonicity via extrema and finite sums.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 207 · Exact editable TeX passage
L5.2.2
Integrability iff both interval restrictions are integrable; interval additivity.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 205 · Exact editable TeX passage
F0-COMP
Closed bounded Euclidean sets are compact; continuous real functions attain extrema on nonempty compact sets; continuous maps on compact sets are uniformly continuous.
L10.1.5
Both refinement inequalities; upper half is P17.1.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 103 · Exact editable TeX passage
L7.4.4
Euclidean completeness by coordinatewise real completeness
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 298 · Exact editable TeX passage
P12.3
Full scalar linearity and finite sums, restriction exercise, arbitrary orientation and base-point identity.
P9.3
Norm equivalence and boundedness from any finite-dimensional normed domain into any normed target.
L5.2.7
Continuous functions on compact intervals are Riemann integrable.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 208 · Exact editable TeX passage
P17.4-grid
Construction of fine grids and handling the zero-volume/dimension cases in the continuous-integrability proof.
L10.1.6
Complete common-refinement proof of lower <= upper integral and volume bounds.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 104 · Exact editable TeX passage
CLOSED-BALL-CONTRACTION
Unique fixed point of a contraction mapping a nonempty closed Euclidean ball into itself.
P12.4
Finite-vector norm integrability, norm bound, and convergence of integrals under a uniform error with integrable limit.
P12.5-endpoints
One-sided endpoint interpretation, strict-limit error and arbitrary-base-point details.
L5.5.3
Complete scalar tail identity for an infinite right endpoint.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 230 · Exact editable TeX passage
L5.5.4
Complete nonnegative-supremum and divergent-endpoint subsequence proof.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 230 · Exact editable TeX passage
P9.2-operator
Positivity, scaling bound and Lipschitz continuity after the finite norm is established.
L10.1.12
Both directions of the small-gap criterion with supremum/infimum operations explicitly available.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 106 · Exact editable TeX passage
P17.5-upper
Upper-sum inequality in Fubini A, boundedness of upper/lower section integrals.
L7.5.12
Continuity of a compact integral in one parameter.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 312 · Exact editable TeX passage
COMPACT-INTERVAL-INTEGRAL
Bounded-interval real/vector Riemann construction, linearity, restriction, orientation, norm bound, continuous integrability and uniform-error passage.
L5.3.3
Primitive is Lipschitz; derivative equals f at every point of continuity, one-sided at endpoints.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 216 · Exact editable TeX passage
L8.2.4
Every linear map from a finite-dimensional normed domain into any normed target is bounded and continuous; the zero-domain case, actual norm equivalence and continuity are proved in P9.3 and P9.2-operator.
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
L10.1.13
Restriction to a subrectangle including the locally supplied degenerate cases.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 107 · Exact editable TeX passage
L10.1.15
Complete continuous-integrability argument, with its fine-grid and zero-case omissions supplied.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 108 · Exact editable TeX passage
L10.2.2
Full upper/lower compact-rectangle Fubini theorem, not just its continuous specialization.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 115 · Exact editable TeX passage
L8.2.5
Operator norm sum, scalar and composition inequalities and norm axioms.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 25 · Exact editable TeX passage
L8.2.6
Invertible neighbourhood and continuity of inversion in every finite-dimensional normed space.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 26 · Exact editable TeX passage
L8.2.7
Matrix-coordinate/operator-norm topology equivalence; full preceding Frobenius estimates.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 29 · Exact editable TeX passage
L8.3.2
Uniqueness of the total derivative.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 39 · Exact editable TeX passage
L8.3.5
Differentiability implies continuity.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 40 · Exact editable TeX passage
P10.2-typo
Independent scalar remainder calculation correcting the extra closing parenthesis.
L8.2.8
All seven determinant properties; continuity uses P10.1.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 30 · Exact editable TeX passage
L8.3.3
Full zero-remainder computation for a linear map.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 39 · Exact editable TeX passage
L8.3.9
Partial derivatives as columns of the total derivative.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 42 · Exact editable TeX passage
L8.3.7
Total chain rule, including zero intermediate increment.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 41 · Exact editable TeX passage
L8.3.6
Derivative sum and scalar rules; extra-parenthesis typo explicitly corrected in P10.2.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 40 · Exact editable TeX passage
L8.2.9
Determinant multiplication, transpose invariance and invertibility criterion.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 31 · Exact editable TeX passage
P12.5-extension
Continuous constant endpoint extension supplies an open-domain primitive for the chain rule.
P10.2
Product and quotient rules, reciprocal derivative and scalar-multiple typo correction.
L4.2.2
Scalar Fermat theorem at an interior extremum.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 174 · Exact editable TeX passage
P10.5-rules
Induction proving finite C^k sum/product/composition closure, smooth reciprocal and polynomials; excludes its later P2/IFT applications.
L4.2.3
Rolle theorem on a nondegenerate closed interval.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 175 · Exact editable TeX passage
P2
Cofactor identity, smooth inverse and its differential.
L4.2.4
Scalar mean-value theorem by subtraction of the affine secant.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 176 · Exact editable TeX passage
P8-smooth
Positive square-root derivative and smoothness; existence/continuity imported separately.
F0-ALG
Determinant multiplication, cofactor inversion and smooth matrix dependence.
L4.2.6
Zero derivative implies constant on an interval.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 177 · Exact editable TeX passage
P10.4
Zero endpoint-difference and equal-point cases for vector mean value.
P10.3
Vector-valued n=1 base case and domain/zero increments in continuous-partials induction.
L5.3.1
Integral of an integrable derivative equals the endpoint difference; full stated generality.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 214 · Exact editable TeX passage
L9.1.1
Compact one-parameter integral derivative with uniform-continuity/MVT proof and explicit integral-error bound.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 71 · Exact editable TeX passage
Q5
Full finite-dimensional real spectral theorem and determinant formula.
L8.4.1
Full vector mean-value inequality with zero case supplied.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 50 · Exact editable TeX passage
L8.4.6
C1 iff all partial derivatives exist and are continuous.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 52 · Exact editable TeX passage
P5
Signature invariance under congruence and the Morse Jacobian determinant factor.
L8.4.2
Derivative bound implies Lipschitz bound on a convex open domain.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 50 · Exact editable TeX passage
L8.5.1
C1 inverse theorem, open image, derivative formula and continuity.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 56 · Exact editable TeX passage
P10.6
Explicit slice/product-neighbourhood restriction and uniqueness in the implicit proof.
L8.5.6
C1 implicit theorem on a genuine product neighbourhood, with P10.6 domain correction.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 60 · Exact editable TeX passage
P3
Inverse and implicit C^r upgrade for all finite r>=1 and smooth maps, jointly in parameters.
F0-DIFF
Finite-dimensional differential rules, mean value, smooth roots and C^r inverse/implicit maps; excludes integration/Taylor/exponential/COV.
P11.1
Recursive total-derivative C^r agrees with continuous ordered partials, including vector-valued maps.
L5.3.5
Oriented one-variable substitution, including noninjective g and endpoint range values.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 218 · Exact editable TeX passage
P12.6
Integration by parts, finite integral Taylor remainder for every N>=1, norm estimate and all-sign scaled Morse identity.
P13.1
Complex field, multiplicative modulus, all sequence limit laws and real-parameter smooth algebraic rules.
P11.2-bridge
Full two-order mixed-partial identity from two coordinate mean-value calculations, including closed-rectangle domains, the common limit and equal indices.
L5.4.1
Parts (i)–(iv) only: logarithm integral, derivative, strict increase, full range, endpoint limits, product law and uniqueness. Rational powers in (v) excluded.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 221 · Exact editable TeX passage
P13.2-series
Complex Cauchy criterion, absolute convergence, null series terms and bounded convergent sequences.
P17.2
Full omitted linearity and monotonicity; product/modulus closure; all finite-vector/complex norm and uniform-error bounds.
L8.6.2
Full two-order mixed-partial identity, with explicit definition/domain/limit bridges.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
P14.1
Exact IVT/logarithm binding with endpoint values and orientation explained; no unused rational-root import.
P14.2-inverse
Use the already proved P3 inverse theorem at each point and identify each smooth local inverse with the global inverse of L.
L2.6.5
Full written Mertens proof; real comparisons only on moduli, with the complex extension stated explicitly in P13.2.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
P17.3
Finite-grid integral additivity, null coordinate faces, full extension-by-zero exercise and independence of the containing rectangle.
P17.4
Continuous/smooth compact-support extension, support of derivatives, and finite-parameter continuity of compact rectangle integrals.
P11.2-orders
Every permutation of a finite derivative list up to the stated regularity, by adjacent swaps.
P4
Schur-complement Hessian and determinant identity with smooth mixed-partial symmetry.
L5.4.2
Parts (i)–(iv) and full uniqueness proof, with smooth inverse supplied by P3. Rational-power part (v) excluded.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 223 · Exact editable TeX passage
P13.2-mertens
Complex Mertens theorem with one absolutely convergent factor; finite-sum error estimate and either choice of the absolute factor.
L10.1.19
Independence of support-containing rectangle, with the exact zero-extension exercise and empty-support case supplied in P17.3.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
P18.1
Absolute improper integral in every finite dimension, vector Cauchy limit, all real radii, vanishing tails, rectangle-exhaustion independence and half-lines.
P17.5-order
Full version B by exact grid relabelling; continuous vector/complex iteration in every order and product factorization.
P12.7
Full joint finite-parameter C^r/C-infinity compact integral rule, with vector values and zero cases.
P14.2-powers
All real derivatives, positive real powers and falling-product derivative formula.
P15.1
Absolute and compact-uniform exponential series; all real partials via compact FTC; equality with real exponential and path chain rule.
L5.5.5
Full scalar comparison proof, with Cauchy-to-arbitrary-endpoint passage explicitly supplied in P18.1.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 231 · Exact editable TeX passage
COMPACT-RECTANGLE-FUBINI
Full compact rectangle construction, properties and upper/lower-integral Fubini in both orders.
M1
Full smooth parameter Morse normal form, local signed chart, signature and critical-point Jacobian, including dimension zero.
FTC-TAYLOR-COMPACT-PARAMETERS
Both fundamental-theorem forms, one-variable substitution, integral Taylor remainder and full smooth parameter integration on a compact interval.
P14.3
Polynomial/exponential and Gaussian boundary decay; complete smooth flat-cutoff exercise. No improper-integral existence claim.
L5.5.2-gt1
The actually written p>1 infinite-right-endpoint case only; other p-test cases excluded.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C10 · Indonesian proof, PDF page 229 · Exact editable TeX passage
P19.1
Nonnegative countable sums and double enumeration; monotonicity, finite-cover equivalence, countable subadditivity and null modifications.
P15.2
Exponential addition from finite binomial identities and absolute Mertens products; conjugation, nonvanishing, reciprocal and exact modulus.
M2
Finite precompact parameter cover and derivative bounds for charts and inverses on their compact images.
M3
Exact curved family, global chart and inverse, critical point, Hessian, Jacobian and degeneration example.
M4. A zero-diagonal pivot and a determinant bound
Read the complete worked exercise: exact signed Morse coordinates, inverse and Jacobian, a lower bound for every chart and the Euclidean operator norm of the displayed chart. Editable source and figure font notice.
P19.2
Outer measure of closed/open rectangles and finite disjoint open rectangle unions; exact finite-cover/grid argument.
L10.3.2
Full small-ball characterization of null sets, with finite subdivision and countable regrouping supplied.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 121 · Exact editable TeX passage
L10.3.4
Countable union theorem with the nonnegative double-series exercise completed in P19.1.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 122 · Exact editable TeX passage
P16.1
All complex sine/cosine series and squared/addition identities, real derivatives and norm bounds; all used exercises completed.
PARAMETER-MORSE
Complete M1/M2/M3 proof chain, relative to explicit axioms; no Fourier or improper-integral closure.
P19.3
Compact small-ball subcover exercise; coordinate hyperplane and rectangle-face nullity with all union inputs proved.
P16.2
First-zero supremum argument, pi, all return times, and the least positive period of each individual trigonometric function.
L10.3.7
Finite open rectangle and small-ball covers of compact null sets; omitted ball case supplied.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 124 · Exact editable TeX passage
P19.4
Complete C1 image theorem for arbitrary null subsets of open sets, including nonclosed relatively compact sets and compact exhaustion.
P20.1
Finite-grid assignments, face covers, Archimedean countable levels and zero-side cases for the full Riemann integrability criterion.
P16.3
All quadrants and axes; bijective angle, smooth arctangent, unique smooth right-half-plane root and both signed boundary phases. Explicit uniform Gaussian-factor error away from zero and failure of uniformity near a zero eigenvalue.
L10.3.10
Full null-image theorem; the omitted noncompact case and positive ball-bound convention are P19.4.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
L10.4.3
Full iff theorem: bounded Riemann integrability equals null discontinuity set; both directions and omitted grid/zero cases supplied.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 133 · Exact editable TeX passage
L11.4.2
The full trigonometric proposition is proved by P16.1–P16.3: series, identities, derivatives, first zero, all periods and return times, quadrants and axes. The following unused arc-length assertion is excluded.
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
P20.2
Riemann algebra, almost-everywhere equality/order, closed-null modification, dense-null counterexample and diffeomorphism composition.
L10.5.1
Jordan measurability iff null boundary, using an interior containing rectangle.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 138 · Exact editable TeX passage
EXPONENTIAL-TRIGONOMETRIC
Real and complex exponential, trigonometric functions, pi and the exact Gaussian root phase.
P20.3
All Jordan closure/interior/union/intersection/difference exercises, null-boundary volume equality, and zero-cell case in volume/outer measure.
L10.5.5
Every bounded continuous function on a bounded Jordan set is Riemann integrable; full proof.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 140 · Exact editable TeX passage
L10.5.9
Full compact Jordan image theorem, with the local inverse theorem already closed; source f|V is the map g|V.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
F0-CALC
The exact elementary differential/FTC/Taylor/exponential/root inputs of Q1–Q9 and the smooth flat cutoff, relative to declared axioms.
L10.5.3
Full equality of Jordan volume and outer measure, with the finite-disjoint-rectangle and empty-family steps supplied.
Read the author’s statement and proof · External dependency; Jiří Lebl, Basic Analysis. Author’s licence retained.
Earlier programme: C20 · Indonesian proof, PDF page 139 · Exact editable TeX passage
P21.2
Restrict to nonzero-Jacobian neighbourhood before covers; glue inverse charts; prove compact Jordan covers, norm-open sets and balanced refinements.
P20.4
Complete Jordan-integral properties, finite additivity including null overlaps, and compact-Jordan pullback version of Exercise 10.5.7.
P20.5
Boundary-image inclusion and translation invariance of Jordan volume directly from translated Darboux grids.
P18.2
Global linearity, norm/comparison bounds, exact compact-uniform limit rule and the full stated differentiation rule of Q1.
U001-A4
Flat bump, subordinate finite partition, zero extension and product-parameter localization, without a partition theorem import.
U001-4.1
Smooth critical branch, signed full parameter Morse coordinates, determinant relation and compact inverse-image bounds.
P21.1
Full determinant-volume exercise: shear and dilation sections, permutations, elementary matrix factorization, singular maps and all rectangle boundary conventions.
P18.3
Product weights, sharp s>n rectangular-shell decay, Schwartz and Gaussian majorants; no annulus volume formula assumed.
Q1
The entire compact-uniform dominated limit and parameter-differentiation argument, with all used global integral inputs closed.
L10.7.2
Full compact Jordan change-of-variables theorem for Riemann-integrable amplitudes. The neighbourhood restriction and every used exercise are supplied by P19–P21.2.
Read the local proof · Editable source
Mathematical source: Jiří Lebl, Basic Analysis. Author’s statement and proof. The independent programme proof is linked above; the author’s text retains its own terms.
P18.4
Global continuous Fubini with an explicit integrable product majorant, all section integrals, both orders and actual Gaussian/Schwartz applications.
U001-E9.3
Uniform compact convergence at t=lambda^-2 and contradiction to an unqualified uniform bound.
P21.3
Complete retained substitution argument with exact normalized error-box estimate, null-overlap summation, reverse inequality and complex/vector extension.
P18.5
Exact Fourier differentiation/one-coordinate integration-by-parts passages and compact-support nonstationary integrations.
F0-INT
The compact and absolutely convergent improper integral/norm/tail/iteration inputs used by Q1–Q9. Global interchanges have the exact product-majorant hypotheses in P18.4, not an unsupported all-sections assertion.
P21.4
Absolute-improper Jordan exhaustion, all invertible affine changes, and compact chart substitution with zero extension outside the chosen chart.
P21.5
Polar injectivity/Jacobian, sector substitution, missing-ray/origin/infinity exhaustion and positive Gaussian normalization.
JORDAN-SUBSTITUTION
Full compact Jordan C1 substitution with arbitrary Riemann-integrable amplitudes and all used null-set/Jordan prerequisites.
Q3
Full Schwartz Fourier estimates, signs, seminorm continuity and sharp stated weighted L1 threshold.
Q9
Full nonstationary integration-by-parts estimate, support, finite-order family bounds and parameter costs.
U001-A5
Critical Hessian and quotient form, ordinary density algebra, exact-sequence lift/frame invariance, chart-independent integration and Euclidean normal formula.
Q2
Full right-half-plane complex Gaussian by path and real-frequency differential identities, without an analytic-continuation import.
F0-COV
All actual affine, orthogonal, dilation, compact-chart and polar changes used by the reconstruction.
GLOBAL-INTEGRAL-Q1-Q3-Q9
Exact selected chain for Q1, Q3 and Q9; Q5 was closed earlier.
U001-2.1
Full transpose with divergence, all M,r estimates and M+2r amplitude derivative count.
Q4
Full Schwartz Fourier inversion, including Gaussian approximate identity, first moment, affine substitutions and derivatives.
U001-E9.5
Noncritical extra variable and all-order compact integration-by-parts estimate.
Q6
Exact quadratic Fourier identity with both regularization limits, all root phases, orthogonal changes and absolute majorants.
U001-A1
Monomial and radial Schwartz seminorm equivalence, Gaussian normalization, Fourier Schwartz bounds, full inversion and all actual Fubini/tail justifications.
Q7
Every stated coefficient and finite-order remainder with the original sharp M>N+n/2 threshold.
U001-A2
Plancherel on Schwartz space, damped Gaussian pairing, continuous transposed Fourier transform and exact tempered identity.
Q8
Full normalized smooth parameter/Hessian family and fixed-order differentiated remainder scope.
E1
Exact Gaussian model, branch identity, complete moment/derivative inductions and all stated normalized error bounds.
U001-A3
Integral Cauchy–Schwarz including zero-norm case, sharp 2N+ell derivative bound, compact outer-measure support factor and all parameter derivatives.
U001-3.1
Full regularized Fresnel identity, nonvanishing-candidate ODE argument, both signs, distributional limit and every determinant factor.
P21.6
Substitution and absolute-tail inputs to Gaussian normalization, Schwartz inversion and quadratic stationary phase.
U001-3.2
All N>=0 coefficients and sharp 2N+ell amplitude-derivative remainder, ell>d/2, exact inverse-Hessian power and fixed compact support.
QUADRATIC-Q1-Q9-E1
Gaussian regularization, Schwartz Fourier calculus, quadratic stationary phase Q1–Q9 and exact model E1, with their named earlier proof inputs.
U001-5.1
Full isolated stationary expansion, C_j derivative order, normalized all-parameter remainders, finite local coordinate gluing and coefficient uniqueness.
U001-6.1
All real symbol orders, all scale/parameter derivatives, explicit differentiated exponential remainder, far-part control and coefficient convolution.
U001-E9.1
Quartic perturbation, inverse Taylor coefficients and first correction including negative kappa support restriction.
U001-E9.2
Exact parameter derivative of the critical-value factor and normalized remainder comparison.
U001-A6
Finite critical components on compact support, constant phase/signature, cutoffs after Morse refinement, tangential integration, zero-normal case and uniform parameter/symbol bounds.
U001-7.2
Full clean expansion on each component, intrinsic arbitrary-density leading term, normal-dimension exponent, finite sum and differentiated normalized uniform estimates.
U001-MODELS
Indefinite critical point, stationary line, two approaching critical points, exact signs/constants and loss of uniformity.
U001-E9.4
Positive normal family leading density, exact coordinate Jacobian and lambda^-3/2 remainder.
U001-FULL-STATIONARY
Entire receiving lesson Sections 1–9 and Appendices A.1–A.6, including all stated sharp, parameter, symbol and clean-density results and solved examples/exercises, relative to declared axioms and the exact selected earlier programme proofs.