Back to Project mathematical routes
Metric inverse bounds and the absolute Jacobian formula provide signed transfer. A weak Piola identity shows that the transported sign has zero weak gradient; on a preconnected target the sign is almost everywhere constant and the signed integral is that sign times target volume.
7 direct Cards + 19 reused prerequisites = 26 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: SR001 — Inverse maps on open sets with global metric bounds · SR006 — A positive lower metric bound passes to the derivative · SR015 — Signed transfer from the absolute Jacobian formula · SR020 — Weak Piola identity for a compactly supported test field · SR021 — The transported Jacobian sign has zero weak gradient · SR017 — Almost-everywhere constancy of the sign on a preconnected target · SR019 — The signed Jacobian integral is a sign times target volume
Reused prerequisites: SR455 — Determinant integrals under strong convergence · SR032 — Strong local convergence of mollified derivatives · SR444 — Gluing one almost-everywhere constant over a countable cover · SR050 — The divergence-free cofactor identity · SR157 — Zero weak gradient gives zero derivatives of local mollifications · SR099 — Divergence as the trace of a derivative · SR118 — Global almost-everywhere constancy on a preconnected domain · SR120 — Vanishing weak gradient tested by divergence · SR064 — Smooth compact perturbations preserve the determinant integral difference · SR117 — Local almost-everywhere constancy from the weak equation · SR297 — A determinant difference bound in the sup operator norm · SR155 — Differentiating a local mollification through its kernel · SR449 — Identifying constants on an open overlap · SR464 — Maximal-minor integral differences for Lipschitz perturbations · SR036 — A cofactor row by row replacement · SR061 — A component flux gives a determinant difference · SR058 — Zero integral of a compactly supported divergence · SR025 — Mollification by a normalized smooth kernel · SR452 — From local to global almost-everywhere constancy
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.
Records the maps, their inverse relations, and the quantitative bounds used in the orientation argument.
MathlibAnnex.BilipschitzOrientation.BiLipschitzOpenData
Immediate Card prerequisites: None in this selected scope
Used by in this scope: A positive lower metric bound passes to the derivative · Weak Piola identity for a compactly supported test field
Combines local exceptional sets using an inequality between restricted measures.
MathlibAnnex.aeConstantOn_of_countableCover
Immediate Card prerequisites: None in this selected scope
Used by in this scope: From local to global almost-everywhere constancy
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
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
Defines divergence without choosing coordinates.
MathlibAnnex.divergence
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Vanishing weak gradient tested by divergence · Weak Piola identity for a compactly supported test field
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
Uses positive measure to find a point where both almost-everywhere equalities hold.
MathlibAnnex.aeConstants_eq_of_open_overlap
Immediate Card prerequisites: None in this selected scope
Used by in this scope: From local to global almost-everywhere constancy
Writes a directional derivative without differentiating the locally integrable input.
MathlibAnnex.WeakGradient.localMollification_fderiv_apply
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Zero weak gradient gives zero derivatives of local mollifications
Preserves the same lower constant in the difference-quotient limit.
MathlibAnnex.BilipschitzOrientation.fderiv_lower_bound
Immediate Card prerequisites: Inverse maps on open sets with global metric bounds
Used by in this scope: Signed transfer from the absolute Jacobian formula
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
Expresses a weak equation through compactly supported continuously differentiable vector fields.
MathlibAnnex.WeakDivergenceZero
Immediate Card prerequisites: Divergence as the trace of a derivative
Used by in this scope: Zero weak gradient gives zero derivatives of local mollifications · The transported Jacobian sign has zero weak gradient
Separates agreement of constants by connectedness from countable measure-theoretic gluing.
MathlibAnnex.exists_aeConstantOn_of_local
Immediate Card prerequisites: Gluing one almost-everywhere constant over a countable cover · Identifying constants on an open overlap
Used by in this scope: Global almost-everywhere constancy on a preconnected domain
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
Transfers an integrable function without first assuming that the Jacobian sign is constant.
MathlibAnnex.BilipschitzOrientation.signed_area_transfer
Immediate Card prerequisites: A positive lower metric bound passes to the derivative
Used by in this scope: The transported Jacobian sign has zero weak gradient
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
Substitutes a translated smooth kernel into the weak equation and tracks the reflection sign.
MathlibAnnex.WeakGradient.localMollification_fderiv_apply_eq_zero
Immediate Card prerequisites: Vanishing weak gradient tested by divergence · Differentiating a local mollification through its kernel
Used by in this scope: Local almost-everywhere constancy from the weak equation
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
Turns constant mollifications into one almost-everywhere constant by choosing a common convergence point.
MathlibAnnex.WeakDivergenceZero.nonempty_localAEConstantAt
Immediate Card prerequisites: Zero weak gradient gives zero derivatives of local mollifications
Used by in this scope: Global almost-everywhere constancy on a preconnected domain
Combines local weak-gradient rigidity with topological and countable gluing.
MathlibAnnex.WeakDivergenceZero.exists_aeConstantOn
Immediate Card prerequisites: Local almost-everywhere constancy from the weak equation · From local to global almost-everywhere constancy
Used by in this scope: Almost-everywhere constancy of the sign on a preconnected target
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: Weak Piola identity for a compactly supported test field
Uses coordinate perturbations to show that the signed pullback of a test-field divergence has zero integral.
MathlibAnnex.BilipschitzOrientation.weak_piola
Immediate Card prerequisites: Divergence as the trace of a derivative · Maximal-minor integral differences for Lipschitz perturbations · Inverse maps on open sets with global metric bounds
Used by in this scope: The transported Jacobian sign has zero weak gradient
Uses signed transfer and weak Piola with the same test field to obtain the weak equation on the target.
MathlibAnnex.BilipschitzOrientation.weakDivergenceZero_targetJacobianSign
Immediate Card prerequisites: Vanishing weak gradient tested by divergence · Signed transfer from the absolute Jacobian formula · Weak Piola identity for a compactly supported test field
Used by in this scope: Almost-everywhere constancy of the sign on a preconnected target
Obtains one constant from the weak equation and preconnectedness of the target.
MathlibAnnex.BilipschitzOrientation.targetJacobianSign_ae_const
Immediate Card prerequisites: Global almost-everywhere constancy on a preconnected domain · The transported Jacobian sign has zero weak gradient
Used by in this scope: The signed Jacobian integral is a sign times target volume
Uses preconnectedness to obtain a constant, positive measure to identify its sign, and finite measure to integrate it.
MathlibAnnex.BilipschitzOrientation.integral_det_fderiv_eq_signed_volume
Immediate Card prerequisites: Almost-everywhere constancy of the sign on a preconnected target
Used by in this scope: None in this selected scope