Proof index
Every result used in the receiving lesson has an exact local proof or an earlier proof in this edition. This index gives the precise scope of each use and links its prerequisite proofs in dependency order. Axioms and definitions are labelled explicitly; a dependency contract groups the complete linked arguments.
The human-source excerpts sometimes state broader results. The listed scope identifies exactly the part used here; local supplements supply the used exercises and omitted cases. Notation and definitions explain the common 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
L2.2.1
Squeeze lemma
L2.2.3
Nonstrict inequalities pass to limits
L7.1.4
Real finite-dimensional Cauchy–Schwarz by sum of squares
L7.2.6
Open unions and finite intersections
L7.2.9-open
Only the complete open-ball half; closed-ball half is P6.4-ball
L7.4.2
A convergent metric sequence is Cauchy
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
L3.1.7
Full function/sequential-limit equivalence.
L2.1.17
Subsequences preserve real limits; index induction supplied in P6.1
L7.4.10
Lebesgue covering lemma proved directly from sequential compactness
L2.2.5
Full addition, multiplication and reciprocal proofs; subtraction completed locally
L7.1.5
Euclidean distance satisfies triangle inequality; positivity and symmetry follow from its displayed sum of squares
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
L8.1.13
Uniqueness of basis coordinates.
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
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
L7.3.9
Coordinatewise and Euclidean convergence agree for every finite n
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
L7.4.11
Sequential compactness and the finite-subcover definition are equivalent
L7.3.12
Closed sets contain convergent sequence limits
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
L5.1.2
Darboux sum bounds and existence of their defining finite extrema.
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.
L7.2.22
Every ball about a point of the closure meets the set
L7.5.5
Continuous image of a compact set is compact
L7.5.11
Continuous maps on compact spaces are uniformly continuous
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.
L8.1.16
Inverse linearity, with the other four parts completed locally.
L8.1.17
Determination and extension from basis values, including the omitted linearity check.
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.
L5.1.7
Both refinement inequalities; omitted upper half supplied by P12.2.
L7.6.2
Complete-space contraction principle with finite geometric bound and explicit limit step
L3.3.8
Both strict orientations of the intermediate value theorem.
L7.4.9
Compact sets are closed and bounded, with the empty-set case explicit locally
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.
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.
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
P1
P1. The finite-dimensional step
L5.1.8
Lower Darboux integral <= upper integral, with common-refinement proof.
L5.2.1
Additivity of upper and lower integrals on adjacent intervals.
L7.5.6
Continuous real functions on nonempty compact spaces attain both extrema
L10.1.2
Full Darboux bounds, with the used volume exercise now proved.
L10.4.1
Continuity iff zero oscillation; full proof.
L10.4.2
Closed positive oscillation level sets on a closed domain; full proof.
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
L5.1.10
Integral bound is the just-proved Darboux bound with equal lower/upper integrals, as Definition 5.1.9 specifies.
L5.1.11
Exact constant integral, proved by coinciding upper/lower bounds.
L5.1.13
Arbitrarily small Darboux gaps imply integrability.
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.
L5.2.6
Integral monotonicity via extrema and finite sums.
L5.2.2
Integrability iff both interval restrictions are integrable; interval additivity.
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.
L7.4.4
Euclidean completeness by coordinatewise real completeness
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.
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.
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.
L5.5.4
Complete nonnegative-supremum and divergent-endpoint subsequence proof.
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.
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.
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.
L8.2.4
Source Euclidean proof plus P9.3 for its full stated normed-space generality.
L10.1.13
Restriction to a subrectangle including the locally supplied degenerate cases.
L10.1.15
Complete continuous-integrability argument, with its fine-grid and zero-case omissions supplied.
L10.2.2
Full upper/lower compact-rectangle Fubini theorem, not just its continuous specialization.
L8.2.5
Operator norm sum, scalar and composition inequalities and norm axioms.
L8.2.6
Invertible neighbourhood and continuity of inversion in every finite-dimensional normed space.
L8.2.7
Matrix-coordinate/operator-norm topology equivalence; full preceding Frobenius estimates.
L8.3.2
Uniqueness of the total derivative.
L8.3.5
Differentiability implies continuity.
P10.2-typo
Independent scalar remainder calculation correcting the extra closing parenthesis.
L8.2.8
All seven determinant properties; continuity uses P10.1.
L8.3.3
Full zero-remainder computation for a linear map.
L8.3.9
Partial derivatives as columns of the total derivative.
L8.3.7
Total chain rule, including zero intermediate increment.
L8.3.6
Derivative sum and scalar rules; extra-parenthesis typo explicitly corrected in P10.2.
L8.2.9
Determinant multiplication, transpose invariance and invertibility criterion.
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.
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.
P2
Cofactor identity, smooth inverse and its differential.
L4.2.4
Scalar mean-value theorem by subtraction of the affine secant.
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.
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.
L9.1.1
Compact one-parameter integral derivative with uniform-continuity/MVT proof and explicit integral-error bound.
Q5
Full finite-dimensional real spectral theorem and determinant formula.
L8.4.1
Full vector mean-value inequality with zero case supplied.
L8.4.6
C1 iff all partial derivatives exist and are continuous.
P5
Signature invariance under congruence and the Morse Jacobian determinant factor.
L8.4.2
Derivative bound implies Lipschitz bound on a convex open domain.
L8.5.1
C1 inverse theorem, open image, derivative formula and continuity.
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.
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.
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
Closed rectangle/equal-index cases and the conditional limit argument once the source difference-quotient identities are supplied.
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.
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.
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.
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.
P13.2-mertens
Full complex Mertens theorem with one absolutely convergent factor; human proof retained with hypotheses and error choice explicit.
L10.1.19
Independence of support-containing rectangle, with the exact zero-extension exercise and empty-support case supplied in P17.3.
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.
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.
P19.1
Nonnegative countable sums and double enumeration; monotonicity, finite-cover equivalence, countable subadditivity and null modifications.
P15.2
Binomial induction and retained Mertens proof establish addition; 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.
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.
L10.3.4
Countable union theorem with the nonnegative double-series exercise completed in P19.1.
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.
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.
L10.3.10
Full null-image theorem; the omitted noncompact case and positive ball-bound convention are P19.4.
L10.4.3
Full iff theorem: bounded Riemann integrability equals null discontinuity set; both directions and omitted grid/zero cases supplied.
L11.4.2
Proposition and retained argument completed by P16.1–P16.3, including its actual exercises, first-zero supremum, return-time existence issue and omitted axes. The following arc-length assertion is excluded.
P20.2
All used algebra/max/min/norm, a.e. equality/order, closed-null modification and diffeomorphism composition exercises.
L10.5.1
Jordan measurability iff null boundary, using an interior containing rectangle.
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.
L10.5.9
Full compact Jordan image theorem, with the local inverse theorem already closed; source f|V is the map g|V.
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.
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.
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
Exact closure of Q1–Q9 and E1; preserves the unresolved full original U001 lesson and AN04 course scope.
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
Complete selected quadratic module; the full original stationary-phase lesson and course remain open.
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.