SurfaceCoordinates.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem358.TangentNormalCoordinates.Tangent line 16
Source documentation
Tangential directions to the normal v.
```
abbrev Tangent (v : V) := (ℝ ∙ v)ᗮ
```
def OAI.Problem358.TangentNormalCoordinates.unitEquiv line 19
Source documentation
An orthogonal, unit-normal coordinate system, before forgetting the product L² norm.
```
def unitEquiv (v : V) (hv : ‖v‖ = 1) :
    WithLp 2 (ℝ × Tangent v) ≃ₗᵢ[ℝ] V :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
theorem OAI.Problem358.TangentNormalCoordinates.unitEquiv_apply line 28
def OAI.Problem358.TangentNormalCoordinates.unitMap line 34
Source documentation
Normal coordinate followed by tangential displacement.
```
def unitMap (v : V) (p : ℝ × Tangent v) : V := p.1 • v + (p.2 : V)
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
theorem OAI.Problem358.TangentNormalCoordinates.measurePreserving_unitMap line 37
Source documentation
Unit normal/tangent coordinates preserve the canonical Lebesgue measures.
```
theorem measurePreserving_unitMap (v : V) (hv : ‖v‖ = 1) :
    MeasurePreserving (unitMap v) (volume.prod volume) volume := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.unitMap
theorem OAI.Problem358.TangentNormalCoordinates.inner_unitMap line 45
def OAI.Problem358.TangentNormalCoordinates.normalLineEquiv line 53
Source documentation
The unit-speed isometry from the real line to the span of a nonzero normal.
```
def normalLineEquiv (n : V) (hn : n ≠ 0) : ℝ ≃ₗᵢ[ℝ] (ℝ ∙ n) :=
…
```
theorem OAI.Problem358.TangentNormalCoordinates.normalLineEquiv_coe line 62
def OAI.Problem358.TangentNormalCoordinates.normalEquiv line 68
Source documentation
Full orthogonal normal/tangent coordinates for an arbitrary nonzero normal.
```
def normalEquiv (n : V) (hn : n ≠ 0) :
    WithLp 2 (ℝ × Tangent n) ≃ₗᵢ[ℝ] V :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
def OAI.Problem358.TangentNormalCoordinates.normalMap line 75
Source documentation
Unit-speed normal displacement plus a tangential vector.
```
def normalMap (n : V) (p : ℝ × Tangent n) : V :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
theorem OAI.Problem358.TangentNormalCoordinates.normalEquiv_apply line 79
theorem OAI.Problem358.TangentNormalCoordinates.measurePreserving_normalMap line 84
Source documentation
Canonical product volume is transported to ambient volume by normal coordinates.
```
theorem measurePreserving_normalMap (n : V) (hn : n ≠ 0) :
    MeasurePreserving (normalMap n) (volume.prod volume) volume := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.normalMap
theorem OAI.Problem358.TangentNormalCoordinates.inner_normalMap line 92
def OAI.Problem358.TangentNormalCoordinates.affineMap line 103
Source documentation
Translated coordinates for a hyperplane through base.
```
def affineMap (n base : V) (p : ℝ × Tangent n) : V :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
theorem OAI.Problem358.TangentNormalCoordinates.measurePreserving_affineMap line 106
theorem OAI.Problem358.TangentNormalCoordinates.inner_affineMap line 111
theorem OAI.Problem358.TangentNormalCoordinates.affine_value line 116
Source documentation
An affine defining function is exactly normal distance times the normal length.
```
theorem affine_value (n : V) (hn : n ≠ 0) (base : V) (a : ℝ)
    (hface : ⟪n, base⟫_ℝ + a = 0) (p : ℝ × Tangent n) :
    ⟪n, affineMap n base p⟫_ℝ + a = p.1 * ‖n‖ := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.affineMap
def OAI.Problem358.TangentNormalCoordinates.tangentMap line 123
Source documentation
Tangent-first affine coordinates, convenient for iterated strip integrals.
```
def tangentMap (n base : V) (p : Tangent n × ℝ) : V :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
theorem OAI.Problem358.TangentNormalCoordinates.measurePreserving_tangentMap line 126
theorem OAI.Problem358.TangentNormalCoordinates.measurableEmbedding_normalMap line 131
Source documentation
The full normal coordinate map is a Borel embedding.
```
theorem measurableEmbedding_normalMap (n : V) (hn : n ≠ 0) :
    MeasurableEmbedding (normalMap n) := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.normalMap
theorem OAI.Problem358.TangentNormalCoordinates.measurableEmbedding_affineMap line 137
theorem OAI.Problem358.TangentNormalCoordinates.measurableEmbedding_tangentMap line 142
theorem OAI.Problem358.TangentNormalCoordinates.integral_tangentMap line 148
Source documentation
Change of variables into normal coordinates for any Bochner integrand.
```
theorem integral_tangentMap {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    (n : V) (hn : n ≠ 0) (base : V) (f : V → G) :
    (∫ p, f (tangentMap n base p) ∂(volume.prod volume)) = ∫ x, f x :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.tangentMap

theorem OAI.Problem358.TangentNormalCoordinates.integral_eq_iterated line 155

Source documentation

The ambient integral is an iterated tangential/normal slice integral.

theorem integral_eq_iterated {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    (n : V) (hn : n ≠ 0) (base : V) (f : V → G) (hf : Integrable f) :
    (∫ x, f x) = ∫ z : Tangent n, ∫ s : ℝ, f (base + s • ((‖n‖⁻¹ : ℝ) • n) + (z : V)) := by
…

Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent

theorem OAI.Problem358.TangentNormalCoordinates.moving_affine_value line 165

Source documentation

Exact affine-algebra expansion when both normal and intercept move linearly.

theorem moving_affine_value (n : V) (hn : n ≠ 0) (base w : V) (a r t s : ℝ)
    (hface : ⟪n, base⟫_ℝ + a = 0) (z : Tangent n) :
    ⟪n + t • w, tangentMap n base (z, s)⟫_ℝ + (a + t * r) =
      (‖n‖ + t * ⟪w, (‖n‖⁻¹ : ℝ) • n⟫_ℝ) * s +
        t * (⟪w, base + (z : V)⟫_ℝ + r) := by
…

Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.tangentMap

theorem OAI.Problem358.TangentNormalCoordinates.moving_halfspace_iff line 176

Source documentation

A tilted moving halfspace becomes a variable endpoint in the normal coordinate.

theorem moving_halfspace_iff (n : V) (hn : n ≠ 0) (base w : V) (a r t s : ℝ)
    (hface : ⟪n, base⟫_ℝ + a = 0) (z : Tangent n)
    (hden : 0 < ‖n‖ + t * ⟪w, (‖n‖⁻¹ : ℝ) • n⟫_ℝ) :
    0 ≤ ⟪n + t • w, tangentMap n base (z, s)⟫_ℝ + (a + t * r) ↔
      -(t * (⟪w, base + (z : V)⟫_ℝ + r)) /
          (‖n‖ + t * ⟪w, (‖n‖⁻¹ : ℝ) • n⟫_ℝ) ≤ s := by
…

Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.tangentMap

theorem OAI.Problem358.TangentNormalCoordinates.continuousAt_moving_speed line 187

Source documentation

The first-order moving-face speed is continuous at zero perturbation.

theorem continuousAt_moving_speed [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
    (n : V) (hn : n ≠ 0) (base w : V)
    (r : ℝ) (z : Tangent n) :
    ContinuousAt (fun t : ℝ => -(⟪w, base + (z : V)⟫_ℝ + r) /
      (‖n‖ + t * ⟪w, (‖n‖⁻¹ : ℝ) • n⟫_ℝ)) 0 := by
…

Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent

theorem OAI.Problem358.TangentNormalCoordinates.eventually_moving_denominator_pos line 198

Source documentation

A sufficiently small tilt keeps the normal-coordinate denominator positive.

theorem eventually_moving_denominator_pos [FiniteDimensional ℝ V] [MeasurableSpace V]
    [BorelSpace V] (n : V) (hn : n ≠ 0) (w : V) :
    ∀ᶠ t : ℝ in nhds 0, 0 < ‖n‖ + t * ⟪w, (‖n‖⁻¹ : ℝ) • n⟫_ℝ := by
…

theorem OAI.Problem358.TangentNormalCoordinates.norm_normalMap_sq line 206
Source documentation
Pythagoras in normal coordinates, useful for compact-support majorants.
```
theorem norm_normalMap_sq (n : V) (hn : n ≠ 0) (p : ℝ × Tangent n) :
    ‖normalMap n p‖ ^ 2 = p.1 ^ 2 + ‖p.2‖ ^ 2 := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.normalMap
theorem OAI.Problem358.TangentNormalCoordinates.norm_tangent_le line 213
Source documentation
A point in a bounded ambient set has a bounded tangential coordinate.
```
theorem norm_tangent_le (n : V) (hn : n ≠ 0) (p : ℝ × Tangent n) :
    ‖p.2‖ ≤ ‖normalMap n p‖ := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.normalMap
theorem OAI.Problem358.TangentNormalCoordinates.abs_normal_le line 219
Source documentation
A point in a bounded ambient set has a bounded normal coordinate.
```
theorem abs_normal_le (n : V) (hn : n ≠ 0) (p : ℝ × Tangent n) :
    |p.1| ≤ ‖normalMap n p‖ := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.normalMap
def OAI.Problem358.AffinePlaneGraph.graph line 239
Source documentation
A nearby affine plane written as a graph in one fixed transverse direction. The denominator is nonzero precisely when the direction remains transverse.
```
def graph (base : X → V) (u n : V) (c : ℝ) (x : X) : V :=
…
```
theorem OAI.Problem358.AffinePlaneGraph.graph_eq_base line 242
theorem OAI.Problem358.AffinePlaneGraph.inner_graph_add line 247
theorem OAI.Problem358.AffinePlaneGraph.projection_graph line 254
theorem OAI.Problem358.AffinePlaneGraph.projection_graph_add line 260
theorem OAI.Problem358.AffinePlaneGraph.continuous_graph line 271
theorem OAI.Problem358.AffinePlaneGraph.tendsto_graph line 276
theorem OAI.Problem358.AffinePlaneGraph.tendsto_graph_base line 287
theorem OAI.Problem358.AffinePlaneGraph.measurable_graph line 300

theorem OAI.Problem358.AffinePlaneGraph.measurePreserving_graph_chart line 308

Source documentation

Replacing the base plane by any transverse graph preserves the full product disintegration. This is a fiberwise translation, so no surface Jacobian calculation is needed.

theorem measurePreserving_graph_chart
    {μ : Measure X} [SFinite μ] {ρ : Measure V}
    (base : X → V) (hbase : Measurable base) (u n : V) (c : ℝ)
    (hchart : MeasurePreserving
      (fun p : X × ℝ => base p.1 + p.2 • u) (μ.prod volume) ρ) :
    MeasurePreserving
      (fun p : X × ℝ => graph base u n c p.1 + p.2 • u) (μ.prod volume) ρ := by
…

Mentions: OAI.Problem358.AffinePlaneGraph.graph

def OAI.Problem358.TangentNormalCoordinates.affineBase line 344
Source documentation
The canonical point of the affine hyperplane with normal n and intercept a.
```
def affineBase (n : V) (a : ℝ) : V := (-a / ‖n‖ ^ 2) • n
…
```
theorem OAI.Problem358.TangentNormalCoordinates.inner_affineBase line 348
def OAI.Problem358.TangentNormalCoordinates.faceBase line 355
Source documentation
Canonical tangential parametrization of an affine hyperplane.
```
def faceBase (n : V) (a : ℝ) (z : Tangent n) : V := affineBase n a + (z : V)
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.affineBase
theorem OAI.Problem358.TangentNormalCoordinates.inner_faceBase line 358
theorem OAI.Problem358.TangentNormalCoordinates.continuous_faceBase line 365
theorem OAI.Problem358.TangentNormalCoordinates.faceBase_injective line 371
theorem OAI.Problem358.TangentNormalCoordinates.exists_faceBase_eq line 378
Source documentation
Every point of the affine hyperplane occurs in the canonical parametrization.
```
theorem exists_faceBase_eq (n : V) (hn : n ≠ 0) (a : ℝ) (x : V)
    (hx : ⟪n, x⟫_ℝ + a = 0) : ∃ z : Tangent n, faceBase n a z = x := by
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent, OAI.Problem358.TangentNormalCoordinates.faceBase
def OAI.Problem358.TangentNormalCoordinates.faceChart line 388
Source documentation
Unit-normal displacement from the canonical hyperplane parametrization.
```
def faceChart (n : V) (a : ℝ) (p : Tangent n × ℝ) : V :=
…
```
Mentions: OAI.Problem358.TangentNormalCoordinates.Tangent
theorem OAI.Problem358.TangentNormalCoordinates.faceChart_eq_tangentMap line 392
theorem OAI.Problem358.TangentNormalCoordinates.measurePreserving_faceChart line 398
theorem OAI.Problem358.TangentNormalCoordinates.measurableEmbedding_faceChart line 403
theorem OAI.Problem358.TangentNormalCoordinates.inner_unitNormal line 410
theorem OAI.Problem358.TangentNormalCoordinates.inner_unitNormal_pos line 417