Coordinates.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Volume-preserving coordinates adapted to an arbitrary affine hyperplane

def OAI.Problem358.HouseholderCoordinates.alignNormal line 16
Source documentation
A Householder reflection sends the chosen normal to a coordinate normal.
```
def alignNormal (i : ι) (n : EuclideanSpace ℝ ι) :
    EuclideanSpace ℝ ι ≃ₗᵢ[ℝ] EuclideanSpace ℝ ι :=
…
```
lemma OAI.Problem358.HouseholderCoordinates.alignNormal_normal line 20
lemma OAI.Problem358.HouseholderCoordinates.inner_eq_norm_mul_coord line 25
lemma OAI.Problem358.HouseholderCoordinates.alignNormal_coord line 30
lemma OAI.Problem358.HouseholderCoordinates.alignNormal_measurePreserving line 37
def OAI.Problem358.HouseholderCoordinates.affineCoordinates line 42
Source documentation
Translation after the reflection straightens an affine hyperplane.
```
def affineCoordinates (i : ι) (n : EuclideanSpace ℝ ι) (c : ℝ) :
    EuclideanSpace ℝ ι ≃ᵐ EuclideanSpace ℝ ι :=
…
```
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_apply line 47
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_symm_apply line 50
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_coord line 54
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_measurePreserving line 59
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_dist line 64
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_le_iff line 69
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_nonneg_iff line 74
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_eq_iff line 79
lemma OAI.Problem358.HouseholderCoordinates.integral_affineCoordinates line 86
Source documentation
No measurability hypothesis on the integrand is needed for an invertible measure-preserving coordinate change.
```
lemma integral_affineCoordinates (i : ι) (n : EuclideanSpace ℝ ι) (c : ℝ)
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (f : EuclideanSpace ℝ ι → F) :
    (∫ x, f (affineCoordinates i n c x)) = ∫ y, f y :=
…
```
Mentions: OAI.Problem358.HouseholderCoordinates.affineCoordinates
lemma OAI.Problem358.HouseholderCoordinates.alignNormal_symm_single line 93
lemma OAI.Problem358.HouseholderCoordinates.affineCoordinates_symm_add_single line 106
Source documentation
A unit coordinate displacement in straightened coordinates is displacement along the unit normal in the original space.
```
lemma affineCoordinates_symm_add_single (i : ι) {n : EuclideanSpace ℝ ι}
    (hn : n ≠ 0) (c t : ℝ) (y : EuclideanSpace ℝ ι) :
    (affineCoordinates i n c).symm (y + EuclideanSpace.single i t) =
      (affineCoordinates i n c).symm y + (t / ‖n‖) • n := by
…
```
Mentions: OAI.Problem358.HouseholderCoordinates.affineCoordinates
lemma OAI.Problem358.HouseholderCoordinates.affineFunctional_symm line 115
lemma OAI.Problem358.HouseholderCoordinates.setIntegral_affineCoordinates line 123
def OAI.Problem358.HouseholderCoordinates.productCoordinates line 146
Source documentation
First coordinate is signed distance to the chosen affine plane; the others parameterize its orthogonal coordinates.
```
def productCoordinates (i : Fin (d + 1)) (n : EuclideanSpace ℝ (Fin (d + 1)))
    (c : ℝ) : EuclideanSpace ℝ (Fin (d + 1)) ≃ᵐ ℝ × (Fin d → ℝ) :=
…
```
lemma OAI.Problem358.HouseholderCoordinates.productCoordinates_measurePreserving line 152
lemma OAI.Problem358.HouseholderCoordinates.productCoordinates_symm_apply line 159
lemma OAI.Problem358.HouseholderCoordinates.productCoordinates_symm_affineFunctional line 164
lemma OAI.Problem358.HouseholderCoordinates.productCoordinates_symm_line line 171
def OAI.Problem358.HouseholderCoordinates.normalChart line 188
Source documentation
The normal product chart, with the tangential variable first as in a moving-halfspace disintegration.
```
def normalChart (i : Fin (d + 1)) (n : EuclideanSpace ℝ (Fin (d + 1)))
    (c : ℝ) : (Fin d → ℝ) × ℝ ≃ᵐ EuclideanSpace ℝ (Fin (d + 1)) :=
…
```
lemma OAI.Problem358.HouseholderCoordinates.normalChart_measurePreserving line 192
lemma OAI.Problem358.HouseholderCoordinates.normalChart_affineFunctional line 198
lemma OAI.Problem358.HouseholderCoordinates.normalChart_line line 204
lemma OAI.Problem358.HouseholderCoordinates.normalChart_nonneg_iff line 210
lemma OAI.Problem358.HouseholderCoordinates.continuous_normalChart_symm line 216
lemma OAI.Problem358.HouseholderCoordinates.exists_compact_tangential_support line 226
Source documentation
Compact ambient support gives a compact common tangential support for all normal fibers, hence a finite-volume dominator for moving-face integrals.
```
lemma exists_compact_tangential_support (i : Fin (d + 1))
    (n : EuclideanSpace ℝ (Fin (d + 1))) (c : ℝ)
    {K : Set (EuclideanSpace ℝ (Fin (d + 1)))} (hK : IsCompact K) :
    ∃ S : Set (Fin d → ℝ), IsCompact S ∧
      ∀ z t, normalChart i n c (z, t) ∈ K → z ∈ S := by
…
```
Mentions: OAI.Problem358.HouseholderCoordinates.normalChart

theorem OAI.Problem358.HouseholderCoordinates.integral_normal_fubini line 237

Source documentation

Exact ambient Fubini decomposition in fixed affine-normal coordinates.

theorem integral_normal_fubini (i : Fin (d + 1))
    (n : EuclideanSpace ℝ (Fin (d + 1))) (c : ℝ)
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (f : EuclideanSpace ℝ (Fin (d + 1)) → F) (hf : Integrable f) :
    (∫ x, f x) = ∫ z : Fin d → ℝ, ∫ t : ℝ,
      f ((productCoordinates i n c).symm (t, z)) := by
…

Mentions: OAI.Problem358.HouseholderCoordinates.productCoordinates

theorem OAI.Problem358.HouseholderCoordinates.integral_normal_lines line 250

Source documentation

The same formula with the straight normal lines displayed explicitly.

theorem integral_normal_lines (i : Fin (d + 1))
    {n : EuclideanSpace ℝ (Fin (d + 1))} (hn : n ≠ 0) (c : ℝ)
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (f : EuclideanSpace ℝ (Fin (d + 1)) → F) (hf : Integrable f) :
    (∫ x, f x) = ∫ z : Fin d → ℝ, ∫ t : ℝ,
      f ((productCoordinates i n c).symm (0, z) + (t / ‖n‖) • n) := by
…

Mentions: OAI.Problem358.HouseholderCoordinates.productCoordinates