21.6. The volume element of a region (item 3-4)🔗

The volume item carries the analogous remark — the volume element dV = √g for the 3 × 3 metric tensor of a three-parameter region. It is the three-dimensional analogue of the area construction, the same Gram-determinant raised one rank, and it is formalized the same way.

Definition21.6.1

groupuses 0used by 0✓L∃∀N

The volume element dV = √g is the volume-element density of a three-parameter region, and the volume is its integral over the parameter region (V = ∭ √g du dv dw). It squares back to g, is positive exactly at regular points, and (the correctness anchor) equals |det A| for a flat region — so it integrates to the actual Euclidean volume.

Lean code for Definition21.6.1●1 definition

defdefined in PropertyKindCalculus/Iso80000/Part3/VolumeElement.lean

complete

def PropertyKindCalculus.Iso80000.Part3.VolumeElement.volumeElement.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (t : Fin 3 → E) : ℝ

def PropertyKindCalculus.Iso80000.Part3.VolumeElement.volumeElement.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (t : Fin 3 → E) : ℝ

The **volume element** `dV = √g`: the volume-element density at the point. The
square root is what makes a flat region recover its Euclidean volume
(`volumeElement_eq_abs_det`).

Proof for Definition 21.6.1

uses 0

volumeElement t := Real.sqrt (metricDet t) over the 3 × 3 metricTensor t := Matrix.gram ℝ t for t : Fin 3 → E; regionVolume t s := ∫ x in s, volumeElement (t x) with regionVolume_const the constant-frame case. The proofs mirror AreaElement at one higher rank.

Theorem21.6.2

groupuses 0used by 0✓L∃∀N

EffortmediumTagsproved

A flat region recovers its Euclidean volume. For a region in Euclidean 3-space the element equals |det A|, the change-of-variables volume density — the three-dimensional correctness anchor, confirming the √g reading against the volume it must reproduce.

Lean code for Theorem21.6.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3/VolumeElement.lean

complete

theorem PropertyKindCalculus.Iso80000.Part3.VolumeElement.volumeElement_eq_abs_det
  (t : Fin 3 → EuclideanSpace ℝ (Fin 3)) :
  PropertyKindCalculus.Iso80000.Part3.VolumeElement.volumeElement t =
    |(Matrix.of fun i j => (t j).ofLp i).det|

theorem PropertyKindCalculus.Iso80000.Part3.VolumeElement.volumeElement_eq_abs_det
  (t : Fin 3 → EuclideanSpace ℝ (Fin 3)) :
  PropertyKindCalculus.Iso80000.Part3.VolumeElement.volumeElement
      t =
    |(Matrix.of fun i j =>
          (t j).ofLp i).det|

**The element is the change-of-variables volume density.** For a flat region the
volume element equals `|det A|` — so `dV = |det A| du dv dw` integrates to the
*actual* Euclidean volume, confirming the `√g` reading.

Proof for Theorem 21.6.2

uses 0

volumeElement_eq_abs_det : volumeElement t = |(Matrix.of fun i j => t j i).det| for t : Fin 3 → EuclideanSpace ℝ (Fin 3), via gram_eq_conjTranspose_mul and Real.sqrt_sq_eq_abs. The companion volumeElement_sq gives (dV)² = g.