Shifting an affine subspace towards a point

This file introduces a "shift" transformation of affine subspace, where the subspace is translated relatively to a point c. This is equivalent to AffineSubspace.map (AffineEquiv.constVAdd ..), but hides the detail of arbitrarily choosing a point in the subspace.

Shifting is controlled by a parameter r, indicating how far the output space is to c. We set r = 0 to mean the output space passes through c (See AffineSubspace.shift_zero), while r = 1 means not moving the input space at all (See AffineSubspace.shift_one). With this convention, this transformation is also equivalent to AffineSubspace.map (homothety c r) when r is a unit.

Main declarations

• AffineSubspace.shift defines the shift transformation.
• AffineSubspace.shift_eq shows the shift transformation is equivalent to translation.
• AffineSubspace.shift_eq_map_homothety shows the shift transformation is equivalent to homothety.

noncomputable def AffineSubspace.shift {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) (r : k) : AffineSubspace k P

AffineSubspace.shift s c r is an affine subspace parallel to s, where an arbitrary point on s is moved towards c with linear interpolation by r. When r = 0, that point is moved onto c. When r = 1, that point stays at the original position. A different choice of the point will not affect the output (See AffineSubspace.shift_eq).

We define AffineSubspace.shift ⊥ c r = ⊥ (See AffineSubspace.shift_bot).

Equations

• s.shift c r = if h : Nonempty ↥s then AffineSubspace.map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑h.some)))) s else ⊥

@[simp]

theorem AffineSubspace.direction_shift {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) (r : k) : (s.shift c r).direction = s.direction

@[simp]

theorem AffineSubspace.shift_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (c : P) (r : k) : ⊤.shift c r = ⊤

@[simp]

theorem AffineSubspace.shift_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (c : P) (r : k) : ⊥.shift c r = ⊥

theorem AffineSubspace.shift_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] {s : AffineSubspace k P} (p : ↥s) (c : P) (r : k) : s.shift c r = map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑p)))) s

AffineSubspace.shift s c r can be represented by moving a point in the subspace towards c.

@[simp]

theorem AffineSubspace.shift_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) [h : Nonempty ↥s] (c : P) : s.shift c 0 = mk' c s.direction

@[simp]

theorem AffineSubspace.shift_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) : s.shift c 1 = s

theorem AffineSubspace.affineCombination_mem_shift {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] {ι : Type u_4} [Fintype ι] [Nontrivial ι] (p : ι → P) (i : ι) {w : ι → k} (hw : ∑ i : ι, w i = 1) : (Finset.affineCombination k Finset.univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

Consider a point A with barycentric coordinates associated to a collection of points P. If the coordinate associated to one of the points Pᵢ is r, then the point A is on the span of P \ {Pᵢ} shifted towards Pᵢ with parameter 1 - r.

theorem AffineIndependent.affineCombination_mem_shift_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [AddTorsor V P] [Module k V] {ι : Type u_4} [Fintype ι] [Nontrivial ι] {p : ι → P} (h : AffineIndependent k p) (i : ι) {w : ι → k} (hw : ∑ i : ι, w i = 1) (c : k) : (Finset.affineCombination k Finset.univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c ↔ w i = 1 - c

The iff version of affineCombination_mem_shift for affine independent points.

theorem AffineSubspace.shift_eq_map_homothety {k : Type u_1} {V : Type u_2} {P : Type u_3} [CommRing k] [AddCommGroup V] [AddTorsor V P] [Module k V] (s : AffineSubspace k P) (c : P) {r : k} (hr : IsUnit r) : s.shift c r = map (AffineMap.homothety c r) s

For a unit parameter, shifting is the same as mapping by homothety.

theorem Affine.Simplex.closedInterior_inter_shift_zero {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [IsOrderedAddMonoid k] [AddCommGroup V] [AddTorsor V P] [Module k V] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) [ZeroLEOneClass k] : s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0) = {s.points i}

The base of a simplex shifted with parameter 0 intersects the closed interior only at the vertex.

theorem Affine.Simplex.disjoint_closedInterior_shift {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [PartialOrder k] [IsOrderedAddMonoid k] [AddCommGroup V] [AddTorsor V P] [Module k V] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) {x : k} (hx : x < 0 ∨ 1 < x) : Disjoint s.closedInterior ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x)

The base of a simplex shifted with parameter outside $[0, 1]$ does not intersect the closed interior.

theorem Affine.Simplex.closedInterior_inter_shift_eq_homothety {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [LinearOrder k] [IsOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) {x : k} (hx : x ∈ Set.Icc 0 1) : s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) = ⇑(AffineMap.homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

A parallel cross-section of a simplex is the image of the base under a homothety.