SurfaceMeasure.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic affine-plane measure and orientation invariance

Surface measure is defined by translating canonical volume on a linear subspace. The resulting ambient measure does not depend on the chosen basepoint in the affine plane. In particular reversing a hyperplane equation preserves its measure.

def OAI.Problem358.IntrinsicSurface.planeMeasure line 23
Source documentation
Canonical volume on a subspace, translated into the ambient space.
```
def planeMeasure (W : Submodule ℝ E) (base : E) : Measure E :=
…
```
theorem OAI.Problem358.IntrinsicSurface.planeChart_isClosedEmbedding line 27
theorem OAI.Problem358.IntrinsicSurface.planeMeasure_apply_all line 32
instance OAI.Problem358.IntrinsicSurface.planeMeasure_finiteOnCompacts line 36
theorem OAI.Problem358.IntrinsicSurface.planeMeasure_setIntegral line 42
theorem OAI.Problem358.IntrinsicSurface.planeMeasure_eq_of_sub_mem line 51
Source documentation
Translation of the basepoint within the plane does not change its intrinsic measure. The equality is of ambient measures, not just of total face areas.
```
theorem planeMeasure_eq_of_sub_mem (W : Submodule ℝ E) {p q : E}
    (hpq : q - p ∈ W) : planeMeasure W q = planeMeasure W p := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.planeMeasure
theorem OAI.Problem358.IntrinsicSurface.planeMeasure_apply line 63

theorem OAI.Problem358.IntrinsicSurface.face_volume_eq_of_sub_mem line 70

Source documentation

Explicit basepoint-independence for a measurable face.

theorem face_volume_eq_of_sub_mem (W : Submodule ℝ E) {p q : E}
    (hpq : q - p ∈ W) {s : Set E} (hs : MeasurableSet s) :
    volume {w : W | q + (w : E) ∈ s} =
      volume {w : W | p + (w : E) ∈ s} := by
…

def OAI.Problem358.IntrinsicSurface.normalBase line 78
Source documentation
A canonical basepoint of the affine equation inner n x + c = 0.
```
def normalBase (n : E) (c : ℝ) : E := (-c / ‖n‖ ^ 2) • n
…
```
theorem OAI.Problem358.IntrinsicSurface.inner_normalBase line 81
theorem OAI.Problem358.IntrinsicSurface.normalBase_neg line 87
theorem OAI.Problem358.IntrinsicSurface.orthogonal_span_neg line 92
def OAI.Problem358.IntrinsicSurface.hyperplaneMeasure line 97
Source documentation
Intrinsic measure of a hyperplane, with a fixed canonical basepoint.
```
def hyperplaneMeasure (n : E) (c : ℝ) : Measure E :=
…
```
theorem OAI.Problem358.IntrinsicSurface.hyperplaneMeasure_neg line 101
Source documentation
Reversing the equation of a hyperplane does not change surface measure.
```
@[simp] theorem hyperplaneMeasure_neg (n : E) (c : ℝ) :
    hyperplaneMeasure (-n) (-c) = hyperplaneMeasure n c := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.hyperplaneMeasure
theorem OAI.Problem358.IntrinsicSurface.hyperplaneMeasure_eq_planeMeasure line 107
Source documentation
The canonical hyperplane measure agrees with any parametrization based at a point of its affine equation.
```
theorem hyperplaneMeasure_eq_planeMeasure {n base : E} {c : ℝ}
    (hn : n ≠ 0) (hbase : ⟪n, base⟫ + c = 0) :
    hyperplaneMeasure n c = planeMeasure (ℝ ∙ n)ᗮ base := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.hyperplaneMeasure, OAI.Problem358.IntrinsicSurface.planeMeasure
def OAI.Problem358.IntrinsicSurface.interfaceMeasure line 117
Source documentation
Intrinsic tie-plane measure for a pair of affine scores.
```
def interfaceMeasure (y z : E) (a b : ℝ) : Measure E :=
…
```
theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_swap line 121
Source documentation
The intrinsic measure attached to a cell interface is symmetric in its labels.
```
theorem interfaceMeasure_swap (y z : E) (a b : ℝ) :
    interfaceMeasure z y b a = interfaceMeasure y z a b := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure
theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_eq_planeMeasure line 126
Source documentation
A concrete tie-plane chart computes the canonical interface measure.
```
theorem interfaceMeasure_eq_planeMeasure {y z base : E} {a b : ℝ}
    (hyz : y ≠ z) (htie : ⟪y, base⟫ + a = ⟪z, base⟫ + b) :
    interfaceMeasure y z a b = planeMeasure (ℝ ∙ (y - z))ᗮ base := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure, OAI.Problem358.IntrinsicSurface.planeMeasure
theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_apply_of_tie line 133
theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_setIntegral_of_tie line 140
instance OAI.Problem358.IntrinsicSurface.interfaceMeasure_finiteOnCompacts line 148
theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_lt_top line 153
Source documentation
Compact faces have finite intrinsic surface area.
```
theorem interfaceMeasure_lt_top (y z : E) (a b : ℝ) {s : Set E} (hs : IsCompact s) :
    interfaceMeasure y z a b s < ⊤ := hs.measure_lt_top
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure

theorem OAI.Problem358.IntrinsicSurface.integrableOn_interfaceMeasure line 157

Source documentation

Continuous scalar/vector/tensor weights on compact faces are integrable.

theorem integrableOn_interfaceMeasure
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (y z : E) (a b : ℝ) {s : Set E} (hs : IsCompact s)
    {f : E → F} (hf : ContinuousOn f s) :
    IntegrableOn f s (interfaceMeasure y z a b) := hf.integrableOn_compact hs

Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure

theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_restrict_swap line 164
Source documentation
Common-face restriction is symmetric as a measure.
```
theorem interfaceMeasure_restrict_swap (y z : E) (a b : ℝ) (s t : Set E) :
    (interfaceMeasure z y b a).restrict (t ∩ s) =
      (interfaceMeasure y z a b).restrict (s ∩ t) := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure
theorem OAI.Problem358.IntrinsicSurface.interface_integral_swap line 171
Source documentation
All weighted face integrals, including first and second moments, inherit the same symmetry. The weight need not be integrable for this equality.
```
theorem interface_integral_swap {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (y z : E) (a b : ℝ) (s : Set E) (f : E → F) :
    (∫ x in s, f x ∂interfaceMeasure z y b a) =
      ∫ x in s, f x ∂interfaceMeasure y z a b := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure

theorem OAI.Problem358.IntrinsicSurface.normalized_face_integral_swap line 179

Source documentation

This is the symmetry needed for both mass and moment face coefficients, including the source-volume and normal-length normalization.

theorem normalized_face_integral_swap
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (y z : E) (a b M : ℝ) (s t : Set E) (f : E → F) :
    (M * ‖z - y‖)⁻¹ • (∫ x in t ∩ s, f x ∂interfaceMeasure z y b a) =
      (M * ‖y - z‖)⁻¹ • (∫ x in s ∩ t, f x ∂interfaceMeasure y z a b) := by
…

Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure

theorem OAI.Problem358.IntrinsicSurface.normalized_face_area_swap line 186
theorem OAI.Problem358.IntrinsicSurface.hyperplaneMeasure_smul line 192
Source documentation
Nonzero rescaling of a hyperplane equation does not alter its intrinsic measure.
```
theorem hyperplaneMeasure_smul {n : E} (hn : n ≠ 0) (c : ℝ)
    {r : ℝ} (hr : r ≠ 0) :
    hyperplaneMeasure (r • n) (r * c) = hyperplaneMeasure n c := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.hyperplaneMeasure
theorem OAI.Problem358.IntrinsicSurface.ae_hyperplane_equation line 203
Source documentation
Intrinsic hyperplane measure is concentrated on its defining affine equation.
```
theorem ae_hyperplane_equation {n : E} (hn : n ≠ 0) (c : ℝ) :
    ∀ᵐ x ∂hyperplaneMeasure n c, ⟪n, x⟫ + c = 0 := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.hyperplaneMeasure
theorem OAI.Problem358.IntrinsicSurface.ae_interface_tie line 214
Source documentation
Almost every point for a genuine interface measure satisfies the affine tie.
```
theorem ae_interface_tie {y z : E} (hyz : y ≠ z) (a b : ℝ) :
    ∀ᵐ x ∂interfaceMeasure y z a b, ⟪x, y⟫ + a = ⟪x, z⟫ + b := by
…
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure
theorem OAI.Problem358.IntrinsicSurface.interfaceMeasure_restrict_tie line 221
Source documentation
Restricting intrinsic interface measure to the tie equation is redundant.
```
theorem interfaceMeasure_restrict_tie {y z : E} (hyz : y ≠ z) (a b : ℝ) :
    (interfaceMeasure y z a b).restrict {x | ⟪x, y⟫ + a = ⟪x, z⟫ + b} =
      interfaceMeasure y z a b :=
…
```
Mentions: OAI.Problem358.IntrinsicSurface.interfaceMeasure
def OAI.Problem358.TransverseSurface.height line 240
Source documentation
Height on an affine plane, measured along a fixed transverse direction.
```
def height (n u : V) (c : ℝ) (x : V) : ℝ := (⟪n, x⟫ + c) / ⟪n, u⟫
```
def OAI.Problem358.TransverseSurface.retract line 243
Source documentation
Retraction onto an affine plane along the transverse direction.
```
def retract (n u : V) (c : ℝ) (x : V) : V := x - height n u c x • u
```
Mentions: OAI.Problem358.TransverseSurface.height
lemma OAI.Problem358.TransverseSurface.height_add_transverse line 245
lemma OAI.Problem358.TransverseSurface.retract_add_transverse line 253

theorem OAI.Problem358.TransverseSurface.map_retract_height_eq_prod line 263

Source documentation

A full product disintegration determines its plane measure by applying the common retraction and height. No surface Jacobian theorem is assumed.

theorem map_retract_height_eq_prod
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
    {ρ : Measure V} {n u : V} {c : ℝ} (ha : ⟪n, u⟫ ≠ 0)
    (base : X → V) (hbase : Measurable base)
    (hplane : ∀ x, ⟪n, base x⟫ + c = 0)
    (hchart : MeasurePreserving (fun p : X × ℝ => base p.1 + p.2 • u)
      (μ.prod volume) ρ) :
    Measure.map (fun x => (retract n u c x, height n u c x)) ρ =
      (Measure.map base μ).prod volume := by
…

Mentions: OAI.Problem358.TransverseSurface.retract, OAI.Problem358.TransverseSurface.height

theorem OAI.Problem358.TransverseSurface.map_base_eq_of_charts line 285

Source documentation

Two volume disintegrations along the same transverse direction have exactly the same base measure. The proof cancels the real factor on a unit interval.

theorem map_base_eq_of_charts
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {μ : Measure X} {ν : Measure Y} [SFinite μ] [SFinite ν]
    {ρ : Measure V} {n u : V} {c : ℝ} (ha : ⟪n, u⟫ ≠ 0)
    (base : X → V) (other : Y → V)
    (hb : Measurable base) (ho : Measurable other)
    (hbp : ∀ x, ⟪n, base x⟫ + c = 0)
    (hop : ∀ y, ⟪n, other y⟫ + c = 0)
    (hbc : MeasurePreserving (fun p : X × ℝ => base p.1 + p.2 • u)
      (μ.prod volume) ρ)
    (hoc : MeasurePreserving (fun p : Y × ℝ => other p.1 + p.2 • u)
      (ν.prod volume) ρ) :
…

theorem OAI.Problem358.TransverseSurface.measurePreserving_tangent_shear line 307
theorem OAI.Problem358.TransverseSurface.measurePreserving_oblique_chart line 327
Source documentation
Intrinsic tangent volume, multiplied by the transverse cosine, gives the full ambient-volume disintegration along an arbitrary non-tangential vector. This is proved by a tangential shear and one-dimensional scaling only.
```
theorem measurePreserving_oblique_chart (n u b : V)
    (hn : n ≠ 0) (hu : ⟪n, u⟫ ≠ 0) :
    MeasurePreserving
      (fun p : TangentNormalCoordinates.Tangent n × ℝ => b + (p.1 : V) + p.2 • u)
      ((ENNReal.ofReal |⟪n, u⟫ / ‖n‖| • volume).prod volume) volume := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent

theorem OAI.Problem358.TransverseSurface.map_base_eq_smul_hyperplaneMeasure line 371

Source documentation

Exact intrinsic surface Jacobian for any product-preserving transverse chart. This holds for arbitrary measurable base parameterizations.

theorem map_base_eq_smul_hyperplaneMeasure
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
    {n u : V} {c : ℝ} (hn : n ≠ 0) (hu : ⟪n, u⟫ ≠ 0)
    (base : X → V) (hb : Measurable base)
    (hplane : ∀ x, ⟪n, base x⟫ + c = 0)
    (hchart : MeasurePreserving (fun p : X × ℝ => base p.1 + p.2 • u)
      (μ.prod volume) volume) :
    Measure.map base μ = ENNReal.ofReal |⟪n, u⟫ / ‖n‖| •
      IntrinsicSurface.hyperplaneMeasure n c := by
…

Mentions: OAI.Problem358.IntrinsicSurface.hyperplaneMeasure

theorem OAI.Problem358.TransverseSurface.normalized_integral_eq_intrinsic line 397

Source documentation

Equality of positively oriented normalized face integrals. The theorem includes vector-valued weights and needs neither compact cells nor positivity of their volumes.

theorem normalized_integral_eq_intrinsic
    {X F : Type*} [MeasurableSpace X]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {μ : Measure X} [SFinite μ] {n u : V} {c : ℝ}
    (hn : n ≠ 0) (hu : 0 < ⟪n, u⟫)
    (base : X → V) (hb : Measurable base)
    (hplane : ∀ x, ⟪n, base x⟫ + c = 0)
    (hchart : MeasurePreserving (fun p : X × ℝ => base p.1 + p.2 • u)
      (μ.prod volume) volume)
    (f : V → F) (hf : StronglyMeasurable f) :
    ⟪n, u⟫⁻¹ • (∫ x, f (base x) ∂μ) =
      ‖n‖⁻¹ • (∫ x, f x ∂IntrinsicSurface.hyperplaneMeasure n c) := by
…

Mentions: OAI.Problem358.IntrinsicSurface.hyperplaneMeasure