MATHLIBANNEX / CANONICAL DECLARATION CARD

Boundary agreement determines maximal-minor integrals

MathlibAnnex.NullLagrangian.integral_maximalMinor_eq_of_pointwise_boundary_eq

theorem

Turns pointwise equality on a seminorm sphere into a compactly supported Lipschitz perturbation.

Statement

Fix , and let be a continuous real seminorm on whose closed unit ball is compact. Let be globally Lipschitz and satisfy whenever . For a fixed increasing selection of output coordinates, put and . Then

Assumptions

There are constants for which The other hypotheses are continuity of , compactness of , and pointwise equality on . No smoothness or strict convexity of that sphere, Sobolev trace hypothesis, or separate definiteness assumption on is added.

Conclusion

The integrals of the same signed, increasingly ordered maximal minor agree on . Each integral is finite by the Lipschitz derivative bound on the compact set.

The sphere has measure zero for a specific reason: it is the frontier of the open convex seminorm ball, which is a neighborhood of the origin. Compactness of a general set would not by itself imply that its boundary has measure zero.

Proof route

Extend the boundary-zero difference by zero, prove its Lipschitz bound across the sphere, and apply the compact-perturbation identity to a patched map.

Proof steps

  1. Put and define on , outside. The map is -Lipschitz and vanishes on . If and , continuity of along the segment from to supplies , with , such that . For take . Since , the mixed-side estimate is

    The same-side cases follow from the bound for or from both values being zero; reversing handles the other mixed case. Thus is globally Lipschitz with this constant. Its topological support satisfies , because is closed. It is therefore compact.

  2. Let . Then on and outside. Apply the Lipschitz compact-perturbation theorem with base , perturbation , and the fixed . The hypotheses just verified give

    This difference is integrable: its restriction to the compact support is a difference of integrable Lipschitz minors, and it vanishes outside that support.

  3. To compare derivatives, use local equality, rather than merely equality at one point. On the open set , agrees locally with , hence . On the open complement of , agrees locally with , hence . The excluded set is . The seminorm gauge identity identifies it with the frontier of ; this set is convex and contains a neighborhood of by continuity and the positive radius. The convex-frontier Haar-measure theorem therefore gives . These are the hypotheses used by the linked private sphere-null lemma.

  4. The local identities from Step 3 give

    and on . The integrable difference from Step 2 can therefore be split as

    The last line uses the integrability of each Lipschitz minor on compact . This proves the claimed equality.

Main citations

Lean source signature (exact)

theorem integral_maximalMinor_eq_of_pointwise_boundary_eq
    {m N : ℕ} (p : Seminorm ℝ (Fin (m + 1) → ℝ)) (hp : Continuous p)
    (hK : IsCompact (p.closedBall 0 1))
    (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))
    {F G : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {CF CG : ℝ≥0}
    (hF : LipschitzWith CF F) (hG : LipschitzWith CG G)
    (htrace : ∀ x, p x = 1 → F x = G x) :
    ∫ x in p.closedBall 0 1, maximalMinorIntegrand s F x =
      ∫ x in p.closedBall 0 1, maximalMinorIntegrand s G x
In the source Mathematical meaning
{m N : ℕ} (p : Seminorm ℝ (Fin (m + 1) → ℝ)) (hp : Continuous p) The positive dimension and continuous seminorm on .
(hK : IsCompact (p.closedBall 0 1)) The set is compact; no separate definiteness hypothesis is added.
(s : Matrix.MaximalMinorIndex (m + 1) (Fin N)) The fixed increasing selection of output coordinates, with and signed minor as defined in this Card.
{F G : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {CF CG : ℝ≥0} (hF : LipschitzWith CF F) (hG : LipschitzWith CG G) The maps have the stated global sup-norm Lipschitz bounds with constants .
In the source Mathematical meaning
(htrace : ∀ x, p x = 1 → F x = G x) Pointwise equality at every on the seminorm sphere . This is neither an a.e. condition nor a Sobolev trace.
∫ x in p.closedBall 0 1, maximalMinorIntegrand s F x = ∫ x in p.closedBall 0 1, maximalMinorIntegrand s G x The conclusion : same compact domain, Lebesgue measure, increasing selection and signed minor on both sides.
Exact surrounding binder context (separate excerpt) 
noncomputable section
open Set Function MeasureTheory Filter
open scoped BigOperators Topology NNReal
namespace MathlibAnnex
namespace NullLagrangian

private structure SeminormBall (n : ℕ) where
  p : Seminorm ℝ (Fin n → ℝ)
  continuous_p : Continuous p
  isCompact_closedBall : IsCompact (p.closedBall 0 1)

namespace SeminormBall

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.NullLagrangian.integral_maximalMinor_eq_of_pointwise_boundary_eq

Accepted content SHA-256: 0149c1ed2c440df531b6391bff4bc0fdcadb76b36f1764e2fde5fa3a8cabb6e7

Accepted source guide SHA-256: 526fb4ea936abf392ef576e64ad13117584ddb161fe88cac0343d4032842a630

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑