Back to Project mathematical routes
Mollification, the Piola identity and determinant telescoping give integral identities for compact perturbations. Strong local convergence then passes to Lipschitz maximal minors, whose integrals are determined by boundary agreement.
10 direct Cards + 1 reused prerequisite = 11 unique Cards. This count is a selected Card closure, not a source-declaration count.
Route reading PDF · Preserved source exploration
Read this route with prerequisites
Direct references: SR025 — Mollification by a normalized smooth kernel · SR032 — Strong local convergence of mollified derivatives · SR036 — A cofactor row by row replacement · SR050 — The divergence-free cofactor identity · SR058 — Zero integral of a compactly supported divergence · SR061 — A component flux gives a determinant difference · SR064 — Smooth compact perturbations preserve the determinant integral difference · SR455 — Determinant integrals under strong convergence · SR464 — Maximal-minor integral differences for Lipschitz perturbations · SR465 — Boundary agreement determines maximal-minor integrals
Reused prerequisites: SR297 — A determinant difference bound in the sup operator norm
Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.
No Cards match this search. Clear search to recover this reading scope.
Defines convolution with a nonnegative smooth kernel of integral one.
MathlibAnnex.Mollification.mollify
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Strong local convergence of mollified derivatives
Fixes the cofactor convention used in the divergence and determinant identities.
MathlibAnnex.Piola.cofactorRow
Immediate Card prerequisites: None in this selected scope
Used by in this scope: The divergence-free cofactor identity
Makes all faces in a box divergence formula vanish by placing the support strictly inside the box.
MathlibAnnex.Piola.integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Smooth compact perturbations preserve the determinant integral difference
Controls determinant variation by replacing one matrix row at a time.
MathlibAnnex.ContinuousLinearMap.abs_det_sub_le_max
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Determinant integrals under strong convergence
Approximates the derivative in local , where is the dimension of the domain.
MathlibAnnex.Mollification.tendsto_eLpNorm_fderiv_mollify_sub
Immediate Card prerequisites: Mollification by a normalized smooth kernel
Used by in this scope: Maximal-minor integral differences for Lipschitz perturbations
Cancels the Hessian terms that arise when differentiating a cofactor row.
MathlibAnnex.Piola.divergence_cofactorRowField_eq_zero
Immediate Card prerequisites: A cofactor row by row replacement
Used by in this scope: A component flux gives a determinant difference
Uses Hölder’s inequality to turn strong convergence of matrix fields into convergence of their determinant integrals.
MathlibAnnex.MeasureTheory.tendsto_integral_det_of_strongLn
Immediate Card prerequisites: A determinant difference bound in the sup operator norm
Used by in this scope: Maximal-minor integral differences for Lipschitz perturbations
Expresses the change from one output-coordinate perturbation as a divergence.
MathlibAnnex.Piola.divergence_componentFlux_eq_det_sub
Immediate Card prerequisites: The divergence-free cofactor identity
Used by in this scope: Smooth compact perturbations preserve the determinant integral difference
Builds a finite telescope from single-output perturbations with compactly supported fluxes.
MathlibAnnex.Piola.integral_det_fderiv_add_sub_eq_zero_of_contDiff
Immediate Card prerequisites: A component flux gives a determinant difference · Zero integral of a compactly supported divergence
Used by in this scope: Maximal-minor integral differences for Lipschitz perturbations
Passes the smooth compact-perturbation identity to Lipschitz maps through local strong convergence.
MathlibAnnex.NullLagrangian.integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith
Immediate Card prerequisites: Determinant integrals under strong convergence · Strong local convergence of mollified derivatives · Smooth compact perturbations preserve the determinant integral difference
Used by in this scope: Boundary agreement determines maximal-minor integrals
Turns pointwise equality on a seminorm sphere into a compactly supported Lipschitz perturbation.
MathlibAnnex.NullLagrangian.integral_maximalMinor_eq_of_pointwise_boundary_eq
Immediate Card prerequisites: Maximal-minor integral differences for Lipschitz perturbations
Used by in this scope: None in this selected scope