Centerpoints in convex flags

This file states Corollary 3.14, the centerpoint consequence of the flag Helly theorem. We use a finite indexed weight function rather than measure theory, exactly matching the finite weighted set in the paper and its later application to local lifted mass.

noncomputable def EGZ.ConvexFlag.upperWeight {F : ConvexFlag} {n : ℕ} (points : Fin n → F.Point) (weight : Fin n → ℝ) (xi : F.LinearFunction) (center : F.Point) (hcenter : xi.EvaluableAt center) : ℝ

The total weight of the input points that lie on or above center for a flag functional. Points outside the functional's domain are omitted, as in equation ceq of the paper.

Equations

• EGZ.ConvexFlag.upperWeight points weight xi center hcenter = ∑ i : Fin n with ∃ (hi : xi.EvaluableAt (points i)), xi.eval center hcenter ≤ xi.eval (points i) hi, weight i

theorem EGZ.ConvexFlag.upperWeight_nonneg {F : ConvexFlag} {n : ℕ} (points : Fin n → F.Point) (weight : Fin n → ℝ) (hweight : ∀ (i : Fin n), 0 ≤ weight i) (xi : F.LinearFunction) (center : F.Point) (hcenter : xi.EvaluableAt center) : 0 ≤ upperWeight points weight xi center hcenter

Nonnegative point weights give nonnegative weight to every functional upper side.

theorem EGZ.ConvexFlag.hellyConstant_pos_of_weighted_points {F : ConvexFlag} {Ω : F.ProperPointSet} {n : ℕ} (points : Fin n → F.Point) (weight : Fin n → ℝ) (hproper : ∀ (i : Fin n), points i ∈ Ω) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (hweight : ∀ (i : Fin n), 0 ≤ weight i) (htotal : 0 < ∑ i : Fin n, weight i) : 0 < hellyConstant Ω

Positive total nonnegative weight, together with proper integrality of the input points, guarantees that the denominator in the centerpoint bound is positive.

theorem EGZ.ConvexFlag.flagCenterpoint_family {F : ConvexFlag} (Ω : F.ProperPointSet) {n : ℕ} (points : Fin n → F.Point) (hproper : ∀ (i : Fin n), points i ∈ Ω) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (weight : Fin n → ℝ) (hweight : ∀ (i : Fin n), 0 ≤ weight i) (htotal : 0 < ∑ i : Fin n, weight i) : ∃ q ∈ Ω, q.IsIntegral ∧ ∀ (xi : F.LinearFunction) (hq : xi.EvaluableAt q), (∑ i : Fin n, weight i) / ↑(hellyConstant Ω) ≤ upperWeight points weight xi q hq

Corollary 3.14 (central): the centerpoint theorem for convex flags.

The quantified sum includes precisely those input points at which xi is defined and whose value is at least its value at the centerpoint.

theorem EGZ.ConvexFlag.flagCenterpoint {F : ConvexFlag} (Ω : F.ProperPointSet) {n : ℕ} (points : Fin n → F.Point) (_hpoints_injective : Function.Injective points) (hproper : ∀ (i : Fin n), points i ∈ Ω) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (weight : Fin n → ℝ) (hweight : ∀ (i : Fin n), 0 ≤ weight i) (htotal : 0 < ∑ i : Fin n, weight i) : ∃ q ∈ Ω, q.IsIntegral ∧ ∀ (xi : F.LinearFunction) (hq : xi.EvaluableAt q), (∑ i : Fin n, weight i) / ↑(hellyConstant Ω) ≤ upperWeight points weight xi q hq

Compatibility form for a weighted set of distinct flag points. The centerpoint argument itself also applies to labelled points with repetition.

theorem EGZ.ConvexFlag.corollary_3_14 {F : ConvexFlag} (Ω : F.ProperPointSet) {n : ℕ} (points : Fin n → F.Point) (_hpoints_injective : Function.Injective points) (hproper : ∀ (i : Fin n), points i ∈ Ω) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (weight : Fin n → ℝ) (hweight : ∀ (i : Fin n), 0 ≤ weight i) (htotal : 0 < ∑ i : Fin n, weight i) : ∃ q ∈ Ω, q.IsIntegral ∧ ∀ (xi : F.LinearFunction) (hq : xi.EvaluableAt q), (∑ i : Fin n, weight i) / ↑(hellyConstant Ω) ≤ upperWeight points weight xi q hq

Numbered alias for Corollary 3.14.