8 (continued). Mesh Control
Theorem 8.5
Theorem 8.5 (mesh). Say a subdivision has mesh \le M if any two vertices of
a common face are within distance M. If K has mesh \le M then K' has mesh
\le \tfrac{k}{k+1} M. Consequently, for every \varepsilon > 0 there is r with
K^{(r)} of mesh \le \varepsilon.
Proof. First, the centroid of a finite set s of diameter \le D is within
(1 - 1/|s|)\,D of each point x \in s: the average of the vectors y - x,
y \in s, has norm at most \tfrac{1}{|s|}(|s|-1)D (the term y = x vanishes). By
convexity of the distance function, the same bound holds for every point of
\operatorname{conv}(s), not just of s. Now two vertices of a face of K' are
centroids b(\tau_a), b(\tau_b) with (say) \tau_a \subseteq \tau_b, both faces of
K; then b(\tau_a) \in \operatorname{conv}(\tau_b), and the bound above (with
s = \tau_b, D = M) gives
\|b(\tau_b) - b(\tau_a)\| \le (1 - 1/|\tau_b|)\,M \le \tfrac{k}{k+1}M, since faces
in \mathbb R^k have at most k+1 vertices (affine independence). Every subdivision
has some finite mesh bound (finitely many vertices), and (k/(k+1))^r \to 0, so
iterating drives the mesh below any \varepsilon. \blacksquare
In Lean, the centroid contraction estimates come first:
open scoped BigOperators
open Geometry
namespace Submission
namespace Fine
variable {k : ℕ}
/-- The sum of distances from `x ∈ s` to the points of `s` is at most `(|s|-1)*D`. -/
lemma sum_dist_le
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(s : Finset E) (x : E) (hx : x ∈ s)
(D : ℝ) (hD : ∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D) :
(∑ y ∈ s, ‖y - x‖) ≤ ((s.card : ℝ) - 1) * D := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ∑ y ∈ s, ‖y - x‖ ≤ (↑s.card - 1) * D
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ∑ y ∈ s, ‖y - x‖ = ∑ i ∈ s.erase ?convert_2, ‖i - x‖E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ (↑s.card - 1) * D = ∑ i ∈ s.erase ?convert_2, DE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ DecidableEq EE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ E;
any_goals All goals completed! 🐙;
all_goals try All goals completed! 🐙;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ∑ y ∈ s, ‖y - x‖ = ∑ i ∈ s.erase x, ‖i - x‖ All goals completed! 🐙;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ (↑s.card - 1) * D = ∑ i ∈ s.erase x, D E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ↑s.card - 1 = ↑(s.card - 1) ∨ D = 0;
exact Or.inl ( E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ex:Ehx:x ∈ sD:ℝhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ↑s.card - 1 = ↑(s.card - 1) All goals completed! 🐙 )
/-- Centroid-to-point distance bound: the centroid of a finite nonempty set `s` is within
`(1 - 1/|s|) * D` of any point `x ∈ s`, where `D` bounds pairwise distances in `s`. -/
lemma centroid_dist_le
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(s : Finset E) (hs : s.Nonempty) (x : E) (hx : x ∈ s)
(D : ℝ) (hDnn : 0 ≤ D) (hD : ∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D) :
‖(s.card : ℝ)⁻¹ • (∑ y ∈ s, y) - x‖ ≤ (1 - (s.card : ℝ)⁻¹) * D := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ ≤ (1 - (↑s.card)⁻¹) * D
have h1 : ‖(s.card : ℝ)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(s.card : ℝ)⁻¹ • ∑ y ∈ s, (y - x)‖ := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ ≤ (1 - (↑s.card)⁻¹) * D
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D⊢ ‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(↑s.card)⁻¹ • ∑ y ∈ s, y - (↑s.card)⁻¹ • ↑s.card • x‖;
All goals completed! 🐙;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dh1:‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(↑s.card)⁻¹ • ∑ y ∈ s, (y - x)‖⊢ ‖(↑s.card)⁻¹‖ * ‖∑ y ∈ s, (y - x)‖ ≤ (1 - (↑s.card)⁻¹) * D;
refine' le_trans ( mul_le_mul_of_nonneg_left ( norm_sum_le _ _ ) ( E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dh1:‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(↑s.card)⁻¹ • ∑ y ∈ s, (y - x)‖⊢ 0 ≤ ‖(↑s.card)⁻¹‖ All goals completed! 🐙 ) ) _;
exact le_trans ( mul_le_mul_of_nonneg_left ( sum_dist_le s x hx D hD ) ( norm_nonneg _ ) ) ( E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dh1:‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(↑s.card)⁻¹ • ∑ y ∈ s, (y - x)‖⊢ ‖(↑s.card)⁻¹‖ * ((↑s.card - 1) * D) ≤ (1 - (↑s.card)⁻¹) * D E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dh1:‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(↑s.card)⁻¹ • ∑ y ∈ s, (y - x)‖⊢ (↑s.card)⁻¹ * ((↑s.card - 1) * D) ≤ (1 - (↑s.card)⁻¹) * D ; nlinarith [ inv_mul_cancel₀ ( show ( s.card : ℝ ) ≠ 0 E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonemptyx:Ehx:x ∈ sD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dh1:‖(↑s.card)⁻¹ • ∑ y ∈ s, y - x‖ = ‖(↑s.card)⁻¹ • ∑ y ∈ s, (y - x)‖⊢ ‖(↑s.card)⁻¹‖ * ((↑s.card - 1) * D) ≤ (1 - (↑s.card)⁻¹) * D All goals completed! 🐙 ) ] )
/-
The centroid `(1/|s|) • ∑ s` is within `(1 - 1/|s|)·D` of **every** point of the convex
hull of `s`, where `D` bounds pairwise distances in `s`. (The distance-to-centroid
function is convex, so its max over the hull is attained on `s`.)
-/
lemma centroid_dist_convexHull_le
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(s : Finset E) (hs : s.Nonempty)
(D : ℝ) (hDnn : 0 ≤ D) (hD : ∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ D)
{y : E} (hy : y ∈ convexHull ℝ (s : Set E)) :
‖(s.card : ℝ)⁻¹ • (∑ z ∈ s, z) - y‖ ≤ (1 - (s.card : ℝ)⁻¹) * D := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑s⊢ ‖(↑s.card)⁻¹ • ∑ z ∈ s, z - y‖ ≤ (1 - (↑s.card)⁻¹) * D
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑s⊢ ‖(↑s.card)⁻¹ • ∑ z ∈ s, z - y‖ ≤ (1 - (↑s.card)⁻¹) * D ↔ y ∈ Metric.closedBall ?convert_2 ?convert_3E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑s⊢ ↑s ⊆ Metric.closedBall ?convert_2 ?convert_3E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑s⊢ EE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑s⊢ ℝ;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑s⊢ ↑s ⊆ Metric.closedBall ((↑s.card)⁻¹ • ∑ z ∈ s, z) ((1 - (↑s.card)⁻¹) * D);
intro x E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑sx:Ehx:x ∈ ↑s⊢ x ∈ Metric.closedBall ((↑s.card)⁻¹ • ∑ z ∈ s, z) ((1 - (↑s.card)⁻¹) * D); E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.NonemptyD:ℝhDnn:0 ≤ DhD:∀ a ∈ s, ∀ b ∈ s, ‖a - b‖ ≤ Dy:Ehy:y ∈ (convexHull ℝ) ↑sx:Ehx:x ∈ ↑s⊢ ‖(↑s.card)⁻¹ • ∑ z ∈ s, z - x‖ ≤ (1 - (↑s.card)⁻¹) * D ; All goals completed! 🐙;
/-
Bridge: in a vector space, `Finset.centroid ℝ s id` is the average `(1/|s|) • ∑ s`.
-/
lemma centroid_eq_smul_sum
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(s : Finset E) (hs : s.Nonempty) :
Finset.centroid ℝ s id = (s.card : ℝ)⁻¹ • (∑ z ∈ s, z) := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonempty⊢ Finset.centroid ℝ s id = (↑s.card)⁻¹ • ∑ z ∈ s, z
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonempty⊢ (Finset.affineCombination ℝ s id) (Finset.centroidWeights ℝ s) = (↑s.card)⁻¹ • ∑ z ∈ s, z; E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Es:Finset Ehs:s.Nonempty⊢ ∑ x ∈ s, (↑s.card)⁻¹ • x = (↑s.card)⁻¹ • ∑ z ∈ s, z ;
All goals completed! 🐙
/-
**Per-face barycentric shrinkage.** If `a, b` are centroids of two members `τa ⊆ τb`
of a `⊆`-chain, `τb` is nonempty with `‖u-v‖ ≤ M` for all `u,v ∈ τb` and `τb.card ≤ n+1`,
then `‖a - b‖ ≤ (n/(n+1)) * M`.
-/
lemma centroid_pair_dist_le
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{τa τb : Finset E} (hsub : τa ⊆ τb) (hane : τa.Nonempty) (hbne : τb.Nonempty)
(n : ℕ) (hcard : τb.card ≤ n + 1)
(M : ℝ) (hMnn : 0 ≤ M) (hM : ∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M) :
‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖
≤ ((n : ℝ) / (n + 1)) * M := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M
-- By definition of centroid, we know that the centroid of a set is within `(1 - 1/|s|) * D` of any point in the convex hull of `s`.
have h_centroid_dist : ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ ≤ (1 - 1 / (τb.card : ℝ)) * M := E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - ?convert_1‖E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ (1 - 1 / ↑τb.card) * M = (1 - (↑τb.card)⁻¹) * ME:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ EE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ?convert_1 ∈ (convexHull ℝ) ↑τb;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - ?convert_1‖ ↔
Finset.centroid ℝ τb id = (↑τb.card)⁻¹ • ∑ z ∈ τb, zE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ (1 - 1 / ↑τb.card) * M = (1 - (↑τb.card)⁻¹) * ME:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ EE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ?convert_1 ∈ (convexHull ℝ) ↑τb;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ (1 - 1 / ↑τb.card) * M = (1 - (↑τb.card)⁻¹) * ME:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ EE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ?convert_1 ∈ (convexHull ℝ) ↑τbE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - ?convert_1‖ ↔
Finset.centroid ℝ τb id = (↑τb.card)⁻¹ • ∑ z ∈ τb, z;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ EE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ?convert_1 ∈ (convexHull ℝ) ↑τbE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - ?convert_1‖ ↔
Finset.centroid ℝ τb id = (↑τb.card)⁻¹ • ∑ z ∈ τb, z;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ Finset.centroid ℝ τa id ∈ (convexHull ℝ) ↑τbE:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - Finset.centroid ℝ τa id‖ ↔
Finset.centroid ℝ τb id = (↑τb.card)⁻¹ • ∑ z ∈ τb, z;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ Finset.centroid ℝ τa id ∈ (convexHull ℝ) ↑τb All goals completed! 🐙;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - Finset.centroid ℝ τa id‖ ↔
Finset.centroid ℝ τb id = (↑τb.card)⁻¹ • ∑ z ∈ τb, z E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - Finset.centroid ℝ τa id‖ = ‖(↑τb.card)⁻¹ • ∑ z ∈ τb, z - Finset.centroid ℝ τa id‖ ↔
(↑τb.card)⁻¹ • ∑ z ∈ τb, z = (↑τb.card)⁻¹ • ∑ z ∈ τb, z ; All goals completed! 🐙;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ Mh_centroid_dist:‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ ≤ (1 - 1 / ↑τb.card) * M⊢ ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ ≤ ↑n / (↑n + 1) * M;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ Mh_centroid_dist:‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ ≤ (1 - 1 / ↑τb.card) * M⊢ (1 - 1 / ↑τb.card) * M ≤ ↑n / (↑n + 1) * M;
E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ Mh_centroid_dist:‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖ ≤ (1 - 1 / ↑τb.card) * M⊢ (↑τb.card - 1) * M * (↑n + 1) ≤ ↑τb.card * M * ↑n;
nlinarith [ show ( τb.card : ℝ ) ≤ n + 1 E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M All goals completed! 🐙, mul_le_mul_of_nonneg_left ( show ( τb.card : ℝ ) ≤ n + 1 E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Eτa:Finset Eτb:Finset Ehsub:τa ⊆ τbhane:τa.Nonemptyhbne:τb.Nonemptyn:ℕhcard:τb.card ≤ n + 1M:ℝhMnn:0 ≤ MhM:∀ u ∈ τb, ∀ v ∈ τb, ‖u - v‖ ≤ M⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M All goals completed! 🐙 ) hMnn ]
/-
**Barycentric mesh shrinkage (per face).** If every face of `K` has at most `n+1`
vertices and pairwise vertex distances `≤ M`, then any two vertices of a barycentric face
of `K` are within `(n/(n+1))·M`.
-/
lemma baryFaces_pairwise_dist_le
(K : SimplicialComplex ℝ (Fin k → ℝ))
(n : ℕ) (hdim : ∀ σ ∈ K.faces, σ.card ≤ n + 1)
(M : ℝ) (hMnn : 0 ≤ M)
(hmesh : ∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ M)
{s : Finset (Fin k → ℝ)}
(hs : s ∈ Submission.FamiliesOfMapsB01Bary.baryFaces K)
{a b : Fin k → ℝ} (ha : a ∈ s) (hb : b ∈ s) :
‖a - b‖ ≤ ((n : ℝ) / (n + 1)) * M := k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Ms:Finset (Fin k → ℝ)hs:s ∈ FamiliesOfMapsB01Bary.baryFaces Ka:Fin k → ℝb:Fin k → ℝha:a ∈ shb:b ∈ s⊢ ‖a - b‖ ≤ ↑n / (↑n + 1) * M
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Ma:Fin k → ℝb:Fin k → ℝch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyha:a ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chhb:b ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) ch⊢ ‖a - b‖ ≤ ↑n / (↑n + 1) * M;
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mb:Fin k → ℝch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyhb:b ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chτa:Finset (Fin k → ℝ)hτa:τa ∈ chha:Finset.centroid ℝ τa id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) ch⊢ ‖Finset.centroid ℝ τa id - b‖ ≤ ↑n / (↑n + 1) * M
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chha:Finset.centroid ℝ τa id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chτb:Finset (Fin k → ℝ)hτb:τb ∈ chhb:Finset.centroid ℝ τb id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) ch⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M
have h_subset : τa ⊆ τb ∨ τb ⊆ τa := k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Ms:Finset (Fin k → ℝ)hs:s ∈ FamiliesOfMapsB01Bary.baryFaces Ka:Fin k → ℝb:Fin k → ℝha:a ∈ shb:b ∈ s⊢ ‖a - b‖ ≤ ↑n / (↑n + 1) * M
All goals completed! 🐙
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chha:Finset.centroid ℝ τa id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chτb:Finset (Fin k → ℝ)hτb:τb ∈ chhb:Finset.centroid ℝ τb id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chh_subset:τa ⊆ τb⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * Mk:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chha:Finset.centroid ℝ τa id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chτb:Finset (Fin k → ℝ)hτb:τb ∈ chhb:Finset.centroid ℝ τb id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chh_subset:τb ⊆ τa⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chha:Finset.centroid ℝ τa id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chτb:Finset (Fin k → ℝ)hτb:τb ∈ chhb:Finset.centroid ℝ τb id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chh_subset:τa ⊆ τb⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * Mk:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chha:Finset.centroid ℝ τa id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chτb:Finset (Fin k → ℝ)hτb:τb ∈ chhb:Finset.centroid ℝ τb id ∈ Finset.image (fun σ => Finset.centroid ℝ σ id) chh_subset:τb ⊆ τa⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chτb:Finset (Fin k → ℝ)ha:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τa idhτb:τb ∈ chhb:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τb idh_subset:τb ⊆ τa⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M;
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chτb:Finset (Fin k → ℝ)ha:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τa idhτb:τb ∈ chhb:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τb idh_subset:τa ⊆ τb⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M All goals completed! 🐙;
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chτb:Finset (Fin k → ℝ)ha:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τa idhτb:τb ∈ chhb:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τb idh_subset:τb ⊆ τa⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ ≤ ↑n / (↑n + 1) * M k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)n:ℕhdim:∀ σ ∈ K.faces, σ.card ≤ n + 1M:ℝhMnn:0 ≤ Mhmesh:∀ σ ∈ K.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ Mch:Finset (Finset (Fin k → ℝ))hch₁:↑ch ⊆ K.faceshch₂:IsChain (fun x1 x2 => x1 ⊆ x2) ↑chhch₃:ch.Nonemptyτa:Finset (Fin k → ℝ)hτa:τa ∈ chτb:Finset (Fin k → ℝ)ha:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τa idhτb:τb ∈ chhb:∃ a ∈ ch, Finset.centroid ℝ a id = Finset.centroid ℝ τb idh_subset:τb ⊆ τa⊢ ‖Finset.centroid ℝ τa id - Finset.centroid ℝ τb id‖ = ‖Finset.centroid ℝ τb id - Finset.centroid ℝ τa id‖;
All goals completed! 🐙
then the mesh of a subdivision, the \le k+1 bound on face sizes, and the
iterated shrinkage:
open _root_.FamiliesOfMapsB01 (Subdivision)
/-- A subdivision has *mesh `≤ M`* if all pairwise vertex distances within faces are `≤ M`. -/
def MeshLE {P : Set (Fin k → ℝ)} (S : Subdivision P) (M : ℝ) : Prop :=
∀ σ ∈ S.complex.faces, ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ M
/-
Every face of a subdivision of `P ⊆ ℝᵏ` has at most `k+1` vertices (affine independence
in a `k`-dimensional space).
-/
lemma faces_card_le {P : Set (Fin k → ℝ)} (S : Subdivision P)
{σ : Finset (Fin k → ℝ)} (hσ : σ ∈ S.complex.faces) : σ.card ≤ k + 1 := k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.faces⊢ σ.card ≤ k + 1
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ σ.card ≤ k + 1;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ σ.card < (k + 1).succ;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis✝:AffineIndependent ℝ Subtype.valthis:LinearIndependent ℝ fun i => ↑↑i -ᵥ ↑?convert_3.i1⊢ σ.card < (k + 1).succk:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ ↥σ;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis✝¹:AffineIndependent ℝ Subtype.valthis✝:LinearIndependent ℝ fun i => ↑↑i -ᵥ ↑?convert_3.i1this:Cardinal.mk { x // x ≠ ?convert_3.i1 } ≤ Module.rank ℝ (Fin k → ℝ)⊢ σ.card < (k + 1).succk:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ ↥σ; k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ ↥σ ;
exact ⟨ Classical.choose ( Finset.card_pos.mp ( show 0 < Finset.card σ from Finset.card_pos.mpr ( k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ σ.Nonempty k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis✝:AffineIndependent ℝ Subtype.valthis:σ.Nonempty⊢ σ.Nonempty; All goals completed! 🐙 ) ) ), Classical.choose_spec ( Finset.card_pos.mp ( show 0 < Finset.card σ from Finset.card_pos.mpr ( k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis:AffineIndependent ℝ Subtype.val⊢ σ.Nonempty k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesthis✝:AffineIndependent ℝ Subtype.valthis:σ.Nonempty⊢ σ.Nonempty; All goals completed! 🐙 ) ) ) ⟩
/-- The barycentric subdivision of a subdivision, again a subdivision of `P`. -/
noncomputable def barySub {P : Set (Fin k → ℝ)} (S : Subdivision P) : Subdivision P :=
Submission.FamiliesOfMapsB01Bary.barycentricSubdivision S.complex S.faces_finite S.space_eq
/-
Every subdivision has some finite mesh bound.
-/
lemma exists_meshLE {P : Set (Fin k → ℝ)} (S : Subdivision P) :
∃ M : ℝ, 0 ≤ M ∧ MeshLE S M := k:ℕP:Set (Fin k → ℝ)S:Subdivision P⊢ ∃ M, 0 ≤ M ∧ MeshLE S M
k:ℕP:Set (Fin k → ℝ)S:Subdivision P⊢ 0 ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖k:ℕP:Set (Fin k → ℝ)S:Subdivision P⊢ MeshLE S (2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖);
k:ℕP:Set (Fin k → ℝ)S:Subdivision P⊢ 0 ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖ All goals completed! 🐙;
k:ℕP:Set (Fin k → ℝ)S:Subdivision P⊢ MeshLE S (2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖) intro σ k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.faces⊢ ∀ u ∈ σ, ∀ v ∈ σ, ‖u - v‖ ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖ k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝ⊢ u ∈ σ → ∀ v ∈ σ, ‖u - v‖ ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖ k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σ⊢ ∀ v ∈ σ, ‖u - v‖ ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖ k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝ⊢ v ∈ σ → ‖u - v‖ ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖ k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ ‖u - v‖ ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ ‖u‖ + ‖v‖ ≤ 2 * ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ ‖u‖ + ‖v‖ ≤ ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖ + ∑ x ∈ ⋯.toFinset.biUnion id, ‖x‖;
exact add_le_add ( Finset.single_le_sum ( fun x _ => norm_nonneg x ) ( k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ u ∈ ⋯.toFinset.biUnion id All goals completed! 🐙 ) ) ( Finset.single_le_sum ( fun x _ => norm_nonneg x ) ( k:ℕP:Set (Fin k → ℝ)S:Subdivision Pσ:Finset (Fin k → ℝ)hσ:σ ∈ S.complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ v ∈ ⋯.toFinset.biUnion id All goals completed! 🐙 ) )
/-
Barycentric subdivision shrinks the mesh by the factor `k/(k+1)`.
-/
lemma barySub_meshLE {P : Set (Fin k → ℝ)} (S : Subdivision P)
(M : ℝ) (hMnn : 0 ≤ M) (hS : MeshLE S M) :
MeshLE (barySub S) (((k : ℝ) / (k + 1)) * M) := k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S M⊢ MeshLE (barySub S) (↑k / (↑k + 1) * M)
intro s k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Ms:Finset (Fin k → ℝ)hs:s ∈ (barySub S).complex.faces⊢ ∀ u ∈ s, ∀ v ∈ s, ‖u - v‖ ≤ ↑k / (↑k + 1) * M k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Ms:Finset (Fin k → ℝ)hs:s ∈ (barySub S).complex.facesa:Fin k → ℝ⊢ a ∈ s → ∀ v ∈ s, ‖a - v‖ ≤ ↑k / (↑k + 1) * M k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Ms:Finset (Fin k → ℝ)hs:s ∈ (barySub S).complex.facesa:Fin k → ℝha:a ∈ s⊢ ∀ v ∈ s, ‖a - v‖ ≤ ↑k / (↑k + 1) * M k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Ms:Finset (Fin k → ℝ)hs:s ∈ (barySub S).complex.facesa:Fin k → ℝha:a ∈ sb:Fin k → ℝ⊢ b ∈ s → ‖a - b‖ ≤ ↑k / (↑k + 1) * M k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Ms:Finset (Fin k → ℝ)hs:s ∈ (barySub S).complex.facesa:Fin k → ℝha:a ∈ sb:Fin k → ℝhb:b ∈ s⊢ ‖a - b‖ ≤ ↑k / (↑k + 1) * M;
All goals completed! 🐙
/-
Iterated barycentric subdivision shrinks the mesh geometrically.
-/
lemma iter_barySub_meshLE {P : Set (Fin k → ℝ)} (S : Subdivision P)
(M : ℝ) (hMnn : 0 ≤ M) (hS : MeshLE S M) (r : ℕ) :
MeshLE (barySub^[r] S) ((((k : ℝ) / (k + 1)) ^ r) * M) := k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕ⊢ MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)
k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S M⊢ MeshLE (barySub^[0] S) ((↑k / (↑k + 1)) ^ 0 * M)k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ MeshLE (barySub^[r + 1] S) ((↑k / (↑k + 1)) ^ (r + 1) * M);
k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S M⊢ MeshLE (barySub^[0] S) ((↑k / (↑k + 1)) ^ 0 * M) All goals completed! 🐙;
k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ MeshLE (barySub^[r + 1] S) ((↑k / (↑k + 1)) ^ (r + 1) * M) convert barySub_meshLE ( barySub^[r] S ) ( ( k / ( k + 1 ) ) ^ r * M ) ( k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ 0 ≤ (↑k / (↑k + 1)) ^ r * M All goals completed! 🐙 ) ih using 1 ; k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ barySub^[1 + r] S = barySub (barySub^[r] S)k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ (↑k / (↑k + 1)) ^ (r + 1) * M = ↑k / (↑k + 1) * ((↑k / (↑k + 1)) ^ r * M);
k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ barySub^[1 + r] S = barySub (barySub^[r] S) -- By definition of function iteration, we have `barySub^[1 + r] S = barySub (barySub^[r] S)`.
All goals completed! 🐙;
k:ℕP:Set (Fin k → ℝ)S:Subdivision PM:ℝhMnn:0 ≤ MhS:MeshLE S Mr:ℕih:MeshLE (barySub^[r] S) ((↑k / (↑k + 1)) ^ r * M)⊢ (↑k / (↑k + 1)) ^ (r + 1) * M = ↑k / (↑k + 1) * ((↑k / (↑k + 1)) ^ r * M) All goals completed! 🐙
/-
**Existence of arbitrarily fine subdivisions.** Any subdivision of `P` admits an
iterated barycentric subdivision with mesh `≤ ε`, for any `ε > 0`.
-/
theorem exists_fine_subdivision {P : Set (Fin k → ℝ)} (S : Subdivision P)
(ε : ℝ) (hε : 0 < ε) :
∃ r : ℕ, MeshLE (barySub^[r] S) ε := k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < ε⊢ ∃ r, MeshLE (barySub^[r] S) ε
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S M⊢ ∃ r, MeshLE (barySub^[r] S) ε;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < M⊢ ∃ r, MeshLE (barySub^[r] S) εk:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:¬0 < M⊢ ∃ r, MeshLE (barySub^[r] S) ε;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < M⊢ ∃ r, MeshLE (barySub^[r] S) ε obtain ⟨ r, hr ⟩ := exists_pow_lt_of_lt_one ( show 0 < ε / M k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < ε⊢ ∃ r, MeshLE (barySub^[r] S) ε All goals completed! 🐙 ) ( show ( k : ℝ ) / ( k + 1 ) < 1 k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < ε⊢ ∃ r, MeshLE (barySub^[r] S) ε k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < M⊢ ↑k < 1 * (↑k + 1)k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < M⊢ 0 < ↑k + 1 k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < M⊢ ↑k < 1 * (↑k + 1)k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < M⊢ 0 < ↑k + 1 All goals completed! 🐙 );
exact ⟨ r, fun σ hσ u hu v hv => le_trans ( iter_barySub_meshLE S M hM_nn hM r σ hσ u hu v hv ) ( k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < Mr:ℕhr:(↑k / (↑k + 1)) ^ r < ε / Mσ:Finset (Fin k → ℝ)hσ:σ ∈ (barySub^[r] S).complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ (↑k / (↑k + 1)) ^ r * M ≤ ε k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:0 < Mr:ℕhr:(↑k / (↑k + 1)) ^ r * M < εσ:Finset (Fin k → ℝ)hσ:σ ∈ (barySub^[r] S).complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ (↑k / (↑k + 1)) ^ r * M ≤ ε; All goals completed! 🐙 ) ⟩;
k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:¬0 < M⊢ ∃ r, MeshLE (barySub^[r] S) ε exact ⟨ 0, fun σ hσ u hu v hv => k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:¬0 < Mσ:Finset (Fin k → ℝ)hσ:σ ∈ (barySub^[0] S).complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ ‖u - v‖ ≤ ε simpa [ show M = 0 k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:¬0 < Mσ:Finset (Fin k → ℝ)hσ:σ ∈ (barySub^[0] S).complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ ‖u - v‖ ≤ ε All goals completed! 🐙 ] using hM σ hσ u hu v hv |> le_trans <| k:ℕP:Set (Fin k → ℝ)S:Subdivision Pε:ℝhε:0 < εM:ℝhM_nn:0 ≤ MhM:MeshLE S MhM_pos:¬0 < Mσ:Finset (Fin k → ℝ)hσ:σ ∈ (barySub^[0] S).complex.facesu:Fin k → ℝhu:u ∈ σv:Fin k → ℝhv:v ∈ σ⊢ M ≤ ε All goals completed! 🐙 ⟩
Lemma 8.6
Lemma 8.6 (refinement). Every face of K' lies in the closed cell of a
single face of K; iterating, every face of K^{(r)} lies in the closed cell of a
single face of K. (Immediate: the greatest member of the defining chain contains
every member, so all the centroids lie in its closed cell. Used in Step 5.4.)
\blacksquare
/-
**Refinement (one step).** Every barycentric face of `K` lies in the convex hull of a
single face of `K` (the top element of its defining chain).
-/
lemma baryFaces_subset_face_hull
(K : SimplicialComplex ℝ (Fin k → ℝ))
{s : Finset (Fin k → ℝ)}
(hs : s ∈ Submission.FamiliesOfMapsB01Bary.baryFaces K) :
∃ σ ∈ K.faces, ∀ a ∈ s, a ∈ convexHull ℝ (σ : Set (Fin k → ℝ)) := k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ FamiliesOfMapsB01Bary.baryFaces K⊢ ∃ σ ∈ K.faces, ∀ a ∈ s, a ∈ (convexHull ℝ) ↑σ
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))hch:↑ch ⊆ K.faces ∧ IsChain (fun x1 x2 => x1 ⊆ x2) ↑ch ∧ ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) ch⊢ ∃ σ ∈ K.faces, ∀ a ∈ s, a ∈ (convexHull ℝ) ↑σ;
obtain ⟨σmax, hσmax⟩ : ∃ σmax ∈ ch, ∀ σ ∈ ch, σ ⊆ σmax := k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))hch:↑ch ⊆ K.faces ∧ IsChain (fun x1 x2 => x1 ⊆ x2) ↑ch ∧ ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) ch⊢ ∃ σmax ∈ ch, ∀ σ ∈ ch, σ ⊆ σmax
All goals completed! 🐙;
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))hch:↑ch ⊆ K.faces ∧ IsChain (fun x1 x2 => x1 ⊆ x2) ↑ch ∧ ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) chσmax:Finset (Fin k → ℝ)hσmax:σmax ∈ ch ∧ ∀ σ ∈ ch, σ ⊆ σmax⊢ ∀ a ∈ s, a ∈ (convexHull ℝ) ↑σmax ; k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))σmax:Finset (Fin k → ℝ)hch:↑ch ⊆ K.faces ∧
IsChain (fun x1 x2 => ∀ ⦃x : Fin k → ℝ⦄, x ∈ x1 → x ∈ x2) ↑ch ∧
ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) chhσmax:σmax ∈ ch ∧ ∀ σ ∈ ch, ∀ ⦃x : Fin k → ℝ⦄, x ∈ σ → x ∈ σmax⊢ ∀ a ∈ ch, Finset.centroid ℝ a id ∈ (convexHull ℝ) ↑σmax;
intro a k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))σmax:Finset (Fin k → ℝ)hch:↑ch ⊆ K.faces ∧
IsChain (fun x1 x2 => ∀ ⦃x : Fin k → ℝ⦄, x ∈ x1 → x ∈ x2) ↑ch ∧
ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) chhσmax:σmax ∈ ch ∧ ∀ σ ∈ ch, ∀ ⦃x : Fin k → ℝ⦄, x ∈ σ → x ∈ σmaxa:Finset (Fin k → ℝ)ha:a ∈ ch⊢ Finset.centroid ℝ a id ∈ (convexHull ℝ) ↑σmax; exact (k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))σmax:Finset (Fin k → ℝ)hch:↑ch ⊆ K.faces ∧
IsChain (fun x1 x2 => ∀ ⦃x : Fin k → ℝ⦄, x ∈ x1 → x ∈ x2) ↑ch ∧
ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) chhσmax:σmax ∈ ch ∧ ∀ σ ∈ ch, ∀ ⦃x : Fin k → ℝ⦄, x ∈ σ → x ∈ σmaxa:Finset (Fin k → ℝ)ha:a ∈ ch⊢ Finset.centroid ℝ a id ∈ (convexHull ℝ) ↑σmax
have h_centroid_mem_convexHull : Finset.centroid ℝ a id ∈ convexHull ℝ (a : Set (Fin k → ℝ)) := k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))σmax:Finset (Fin k → ℝ)hch:↑ch ⊆ K.faces ∧
IsChain (fun x1 x2 => ∀ ⦃x : Fin k → ℝ⦄, x ∈ x1 → x ∈ x2) ↑ch ∧
ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) chhσmax:σmax ∈ ch ∧ ∀ σ ∈ ch, ∀ ⦃x : Fin k → ℝ⦄, x ∈ σ → x ∈ σmaxa:Finset (Fin k → ℝ)ha:a ∈ ch⊢ Finset.centroid ℝ a id ∈ (convexHull ℝ) ↑σmax
k:ℕK:SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)ch:Finset (Finset (Fin k → ℝ))σmax:Finset (Fin k → ℝ)hch:↑ch ⊆ K.faces ∧
IsChain (fun x1 x2 => ∀ ⦃x : Fin k → ℝ⦄, x ∈ x1 → x ∈ x2) ↑ch ∧
ch.Nonempty ∧ s = Finset.image (fun σ => Finset.centroid ℝ σ id) chhσmax:σmax ∈ ch ∧ ∀ σ ∈ ch, ∀ ⦃x : Fin k → ℝ⦄, x ∈ σ → x ∈ σmaxa:Finset (Fin k → ℝ)ha:a ∈ ch⊢ a.Nonempty;
All goals completed! 🐙;
All goals completed! 🐙);
end Fine
end Submission
This completes Theorem A in full.