def affineBases (ι : Type u_1) (R : Type u_2) (P : Type u_4) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [AddTorsor M P] : Set (ι → P)

The set of affine bases for an affine space.

Equations

• affineBases ι R P = {v : ι → P | AffineIndependent R v ∧ affineSpan R (Set.range v) = ⊤}

theorem affineBases_findim (ι : Type u_1) (k : Type u_3) (P : Type u_4) {M : Type u_5} [AddCommGroup M] [AddTorsor M P] [Fintype ι] [Field k] [Module k M] [FiniteDimensional k M] (h : Fintype.card ι = Module.finrank k M + 1) : affineBases ι k P = {v : ι → P | AffineIndependent k v}

theorem mem_affineBases_iff (ι : Type u_1) (R : Type u_2) (P : Type u_4) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [AddTorsor M P] [Fintype ι] [DecidableEq ι] [Nontrivial R] (b : AffineBasis ι R P) (v : ι → P) : v ∈ affineBases ι R P ↔ IsUnit (b.toMatrix v)

def evalBarycentricCoords (ι : Type u_1) (R : Type u_2) (P : Type u_4) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [AddTorsor M P] [DecidablePred fun (x : ι → P) => x ∈ affineBases ι R P] (p : P) (v : ι → P) : ι → R

If P is an affine space over the ring R, v : ι → P is an affine basis (for some indexing set ι) and p : P is a point, then eval_barycentric_coords ι R P p v are the barycentric coordinates of p with respect to the affine basis v.

Actually for convenience eval_barycentric_coords is defined even when v is not an affine basis. In this case its value should be regarded as "junk".

Equations

• evalBarycentricCoords ι R P p v = if h : v ∈ affineBases ι R P then { toFun := v, ind' := ⋯, tot' := ⋯ }.coords p else 0

@[simp]

theorem evalBarycentricCoords_apply_of_mem_bases (ι : Type u_1) (R : Type u_2) (P : Type u_4) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [AddTorsor M P] [DecidablePred fun (x : ι → P) => x ∈ affineBases ι R P] (p : P) {v : ι → P} (h : v ∈ affineBases ι R P) : evalBarycentricCoords ι R P p v = { toFun := v, ind' := ⋯, tot' := ⋯ }.coords p

@[simp]

theorem evalBarycentricCoords_apply_of_not_mem_bases (ι : Type u_1) (R : Type u_2) (P : Type u_4) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [AddTorsor M P] [DecidablePred fun (x : ι → P) => x ∈ affineBases ι R P] (p : P) {v : ι → P} (h : v ∉ affineBases ι R P) : evalBarycentricCoords ι R P p v = 0

theorem evalBarycentricCoords_eq_det {ι : Type u_1} {P : Type u_4} {M : Type u_5} [AddCommGroup M] [AddTorsor M P] [Fintype ι] [DecidableEq ι] (S : Type u_6) [Field S] [Module S M] [(v : ι → P) → Decidable (v ∈ affineBases ι S P)] (b : AffineBasis ι S P) (p : P) (v : ι → P) : evalBarycentricCoords ι S P p v = (b.toMatrix v).det⁻¹ • (b.toMatrix v).transpose.cramer (b.coords p)

theorem Matrix.smooth_det (ι : Type u_1) (k : Type u_2) [Fintype ι] [DecidableEq ι] [NontriviallyNormedField k] (m : WithTop ℕ∞) : ContDiff k m det

theorem smooth_barycentric (ι : Type u_1) (𝕜 : Type u_2) (F : Type u_3) [Fintype ι] [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [DecidablePred fun (x : ι → F) => x ∈ affineBases ι 𝕜 F] [FiniteDimensional 𝕜 F] (h : Fintype.card ι = Module.finrank 𝕜 F + 1) {n : WithTop ℕ∞} : ContDiffOn 𝕜 n (Function.uncurry (evalBarycentricCoords ι 𝕜 F)) (Set.univ ×ˢ affineBases ι 𝕜 F)