theorem
mem_convexHull_image
{ι : Type u_1}
{R : Type u_2}
{E : Type u_3}
[Field R]
[LinearOrder R]
[IsStrictOrderedRing R]
[AddCommGroup E]
[Module R E]
{s : Finset ι}
{f : ι → E}
{x : E}
:
x ∈ (convexHull R) (f '' ↑s) ↔ ∃ (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ s.centerMass w f = x
theorem
centerMass_union
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s t : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
[DecidableEq ι]
(hst : Disjoint s t)
(hs : (∀ i ∈ s, w i = 0) ∨ ∑ i ∈ s, w i ≠ 0)
(ht : (∀ i ∈ t, w i = 0) ∨ ∑ i ∈ t, w i ≠ 0)
(hw₁ : ∑ i ∈ s ∪ t, w i = 1)
:
theorem
centerMass_union_of_ne_zero
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s t : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
[DecidableEq ι]
(hst : Disjoint s t)
(hs : ∑ i ∈ s, w i ≠ 0)
(ht : ∑ i ∈ t, w i ≠ 0)
(hw₁ : ∑ i ∈ s ∪ t, w i = 1)
:
theorem
lineMap_centerMass_centerMass
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s t : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
[DecidableEq ι]
(hst : Disjoint s t)
(hs : (∀ i ∈ s, w i = 0) ∨ ∑ i ∈ s, w i ≠ 0)
(ht : (∀ i ∈ t, w i = 0) ∨ ∑ i ∈ t, w i ≠ 0)
(hw₁ : ∑ i ∈ s ∪ t, w i = 1)
:
theorem
lineMap_centerMass_centerMass_of_ne_zero
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s t : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
[DecidableEq ι]
(hst : Disjoint s t)
(hs : ∑ i ∈ s, w i ≠ 0)
(ht : ∑ i ∈ t, w i ≠ 0)
(hw₁ : ∑ i ∈ s ∪ t, w i = 1)
:
theorem
lineMap_centerMass_sdiff
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
{i : ι}
[DecidableEq ι]
(hi : i ∈ s)
(hi₀ : w i ≠ 0)
(hi₁ : w i ≠ 1)
(hw₁ : ∑ i ∈ s, w i = 1)
:
theorem
centerMass_sdiff_of_weight_eq_zero
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
{i : ι}
[DecidableEq ι]
(hi : i ∈ s)
(hi₀ : w i = 0)
:
theorem
lineMap_centerMass_sdiff_singleton_of_ne_one
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
{i : ι}
[DecidableEq ι]
(hi : i ∈ s)
(hi₁ : w i ≠ 1)
(hw₁ : ∑ j ∈ s, w j = 1)
:
theorem
centerMass_union_of_nonneg
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s t : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
[DecidableEq ι]
[LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜]
(hst : Disjoint s t)
(hw₀ : ∀ i ∈ s ∪ t, 0 ≤ w i)
(hw₁ : ∑ i ∈ s ∪ t, w i = 1)
:
theorem
lineMap_centerMass_centerMass_of_nonneg
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s t : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
[DecidableEq ι]
[LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜]
(hst : Disjoint s t)
(hw₀ : ∀ i ∈ s ∪ t, 0 ≤ w i)
(hw₁ : ∑ i ∈ s ∪ t, w i = 1)
:
theorem
lineMap_centerMass_sdiff_singleton_of_nonneg
{ι : Type u_1}
{𝕜 : Type u_2}
{V : Type u_3}
[Field 𝕜]
[AddCommGroup V]
[Module 𝕜 V]
{s : Finset ι}
{w : ι → 𝕜}
{x : ι → V}
{i : ι}
[DecidableEq ι]
[LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜]
(hi : i ∈ s)
(hw₀ : ∀ j ∈ s \ {i}, 0 ≤ w j)
(hw₁ : ∑ j ∈ s, w j = 1)
: