Restricted Lebesgue volume

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This port keeps the common restricted-volume abbreviations and drops domain regularity predicates that are not needed by weak derivatives.

@[reducible, inline]

noncomputable abbrev CKN.volumeOn {d : ℕ} (U : Set (Vec d)) : MeasureTheory.Measure (Vec d)

Lebesgue volume restricted to a native-vector domain.

Equations

• CKN.volumeOn U = MeasureTheory.volume.restrict U

@[reducible, inline]

noncomputable abbrev CKN.volumeMeasureOn {d : ℕ} (U : Set (Vec d)) : MeasureTheory.Measure (Vec d)

Compatibility name for the restricted volume measure.

Equations

• CKN.volumeMeasureOn U = CKN.volumeOn U