Affine planar surface measure

Orthonormal affine frames define plane surface measures as pushforwards of planar volume.

@[reducible, inline]

abbrev LiebThirring.Planar : Type

Euclidean parameter space for an orthonormal plane frame.

Equations

• LiebThirring.Planar = EuclideanSpace ℝ (Fin 2)

noncomputable def LiebThirring.affinePlane (n b : Position) : AffineSubspace ℝ Position

The affine plane through b with normal n, given by its orthogonal direction.

Equations

• LiebThirring.affinePlane n b = AffineSubspace.mk' b (ℝ ∙ n)ᗮ

@[simp]

theorem LiebThirring.mem_affinePlane (n b x : Position) : x ∈ affinePlane n b ↔ inner ℝ n (x - b) = 0

instance LiebThirring.instNonemptySubtypePositionMemAffineSubspaceRealAffinePlane (n b : Position) : Nonempty ↥(affinePlane n b)

@[reducible, inline]

abbrev LiebThirring.PlaneFrame (H : AffineSubspace ℝ Position) [Nonempty ↥H] : Type

An orthonormal affine frame onto the indicated affine subspace.

Equations

• LiebThirring.PlaneFrame H = (LiebThirring.Planar ≃ᵃⁱ[ℝ] ↥H)

noncomputable def LiebThirring.planeFrameOfBasis {H : AffineSubspace ℝ Position} [Nonempty ↥H] (B : OrthonormalBasis (Fin 2) ℝ ↥H.direction) (p : ↥H) : PlaneFrame H

Build a named affine frame from an orthonormal basis and a point on the plane.

Equations

• LiebThirring.planeFrameOfBasis B p = B.repr.symm.toAffineIsometryEquiv.trans (AffineIsometryEquiv.vaddConst ℝ p)

theorem LiebThirring.finrank_affinePlane_direction (n b : Position) (hn : n ≠ 0) : Module.finrank ℝ ↥(affinePlane n b).direction = 2

A nonzero normal gives a two-dimensional affine plane.

theorem LiebThirring.nonempty_planeFrame (n b : Position) (hn : n ≠ 0) : Nonempty (PlaneFrame (affinePlane n b))

An orthonormal affine frame exists for every plane with nonzero normal.

noncomputable def LiebThirring.planeMeasure {H : AffineSubspace ℝ Position} [Nonempty ↥H] (F : PlaneFrame H) : MeasureTheory.Measure Position

Surface measure in a named orthonormal affine frame.

Equations

• LiebThirring.planeMeasure F = MeasureTheory.Measure.map (Subtype.val ∘ ⇑F) MeasureTheory.volume

theorem LiebThirring.measurePreserving_planar_affineIsometry (e : Planar ≃ᵃⁱ[ℝ] Planar) : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume

Affine Euclidean isometries preserve planar Lebesgue measure, including translations.

theorem LiebThirring.planeMeasure_eq {H : AffineSubspace ℝ Position} [Nonempty ↥H] (F G : PlaneFrame H) : planeMeasure F = planeMeasure G

Changing the orthonormal frame and its origin does not change surface measure.

theorem LiebThirring.lintegral_planeMeasure {H : AffineSubspace ℝ Position} [Nonempty ↥H] (F : PlaneFrame H) (h : Position → ENNReal) (hh : Measurable h) : ∫⁻ (x : Position), h x ∂planeMeasure F = ∫⁻ (q : Planar), h ↑(F q)

Integration against the planar surface measure is integration in its frame.