@[simp]

theorem negative_entropy_on_stdSimplex_toReal_of_mem {n : ℕ} {x : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) : (negative_entropy_on_stdSimplex n x).toReal = ∑ i : Fin n, x i * Real.log (x i)

On simplex points, the real-valued branch of negative_entropy_on_stdSimplex is the usual coordinatewise negative-entropy sum.

theorem convexOn_mul_log_sub_half_sq : ConvexOn ℝ (Set.Icc 0 1) fun (x : ℝ) => x * Real.log x - x ^ 2 / 2

Helper for Proposition 5.14: the scalar entropy correction x ↦ x log x - x² / 2 is convex on [0,1].

theorem weighted_square_defect_eq {a b u v : ℝ} (hab : a + b = 1) : a * u ^ 2 + b * v ^ 2 - (a * u + b * v) ^ 2 = a * b * (u - v) ^ 2

Helper for Proposition 5.14: under a + b = 1, the weighted square defect of two scalars is a * b * (u - v)^2.

theorem coordEntropyGap_ge_weightedSquareDefect {u v a b : ℝ} (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (a * u + b * v) * Real.log (a * u + b * v) + a * b / 2 * (u - v) ^ 2 ≤ a * (u * Real.log u) + b * (v * Real.log v)

Helper for Proposition 5.14: convexity of x ↦ x log x - x² / 2 on [0,1] yields the coordinatewise entropy gap with the exact quadratic defect.

theorem entropyJensenGap_ge_l2Square {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (negative_entropy_on_stdSimplex n (a • x + b • y)).toReal + a * b / 2 * ∑ i : Fin n, (x i - y i) ^ 2 ≤ a * (negative_entropy_on_stdSimplex n x).toReal + b * (negative_entropy_on_stdSimplex n y).toReal

Helper for Proposition 5.14: the simplex negative entropy satisfies the Euclidean Jensen gap with modulus 1 in raw coordinates.

theorem simplexCoords_eq_zero_of_add_eq_zero {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) {i : Fin n} (hxy : x i + y i = 0) : x i = 0 ∧ y i = 0

Helper for Proposition 5.14: if two simplex coordinates sum to zero, then each coordinate vanishes.

theorem segmentSupportSum_eq_one {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) (t : ℝ) : ∑ i : Fin n with x i + y i ≠ 0, ((1 - t) * x i + t * y i) = 1

Helper for Proposition 5.14: the fixed active support of a simplex segment carries all of the segment mass.

theorem segmentCoordinate_pos_of_mem_support {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) {i : Fin n} (hi : i ∈ {j : Fin n | x j + y j ≠ 0}) : 0 < (1 - t) * x i + t * y i

Helper for Proposition 5.14: on the fixed active support, every interior segment coordinate is strictly positive.

theorem weightedL1Square_le_segmentReciprocalForm {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : (∑ i : Fin n, |y i - x i|) ^ 2 ≤ ∑ i : Fin n with x i + y i ≠ 0, |y i - x i| ^ 2 / ((1 - t) * x i + t * y i)

Helper for Proposition 5.14: Titu's lemma on the fixed active support yields the global ℓ₁-square reciprocal-form bound along simplex segments.

theorem segmentEntropySum_eq_fullEntropySum {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) (t : ℝ) : ∑ i : Fin n with x i + y i ≠ 0, ((1 - t) * x i + t * y i) * Real.log ((1 - t) * x i + t * y i) = ∑ i : Fin n, ((1 - t) * x i + t * y i) * Real.log ((1 - t) * x i + t * y i)

Helper for Proposition 5.14: restricting the entropy sum to the fixed active support does not change its value along the simplex segment, because the complement coordinates stay equal to 0.

theorem segmentCoordMulLog_hasDerivWithinAt2 {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) {i : Fin n} (hi : i ∈ {j : Fin n | x j + y j ≠ 0}) {t : ℝ} (ht : t ∈ interior (Set.Icc 0 1)) : HasDerivWithinAt (fun (u : ℝ) => ((1 - u) * x i + u * y i) * Real.log ((1 - u) * x i + u * y i)) ((Real.log ((1 - t) * x i + t * y i) + 1) * (y i - x i)) (interior (Set.Icc 0 1)) t ∧ HasDerivWithinAt (fun (u : ℝ) => (Real.log ((1 - u) * x i + u * y i) + 1) * (y i - x i)) ((y i - x i) ^ 2 / ((1 - t) * x i + t * y i)) (interior (Set.Icc 0 1)) t

Helper for Proposition 5.14: on the active support, the coordinate slice t ↦ ((1 - t) x_i + t y_i) log ((1 - t) x_i + t y_i) admits explicit first and second derivatives on the interior of [0, 1].

theorem entropySliceConvexOn_activeSupport {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) : ConvexOn ℝ (Set.Icc 0 1) fun (t : ℝ) => ∑ i : Fin n with x i + y i ≠ 0, ((1 - t) * x i + t * y i) * Real.log ((1 - t) * x i + t * y i) + t * (1 - t) / 2 * (∑ i : Fin n, |x i - y i|) ^ 2

Helper for Proposition 5.14: the active-support entropy slice corrected by the ℓ₁-quadratic term is convex on [0, 1].

theorem entropyJensenGap_ge_l1Square {n : ℕ} {x y : Fin n → ℝ} (hx : x ∈ stdSimplex ℝ (Fin n)) (hy : y ∈ stdSimplex ℝ (Fin n)) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (negative_entropy_on_stdSimplex n (a • x + b • y)).toReal + a * b / 2 * (∑ i : Fin n, |x i - y i|) ^ 2 ≤ a * (negative_entropy_on_stdSimplex n x).toReal + b * (negative_entropy_on_stdSimplex n y).toReal

Helper for Proposition 5.14: the simplex negative entropy satisfies the raw ℓ₁ Jensen gap with modulus 1 in coordinates.

theorem negative_entropy_on_stdSimplex_is_one_strongly_convex_l1 {n : ℕ} : StrongConvexOn (WithLp.ofLp ⁻¹' stdSimplex ℝ (Fin n)) 1 fun (x : WithLp 1 (Fin n → ℝ)) => (negative_entropy_on_stdSimplex n x.ofLp).toReal

Proposition 5.14 (1): the negative entropy on the unit simplex is 1-strongly convex with respect to the l_1 norm, stated in the canonical real-valued form on the simplex itself.

theorem negative_entropy_on_stdSimplex_is_one_strongly_convex_l2 {n : ℕ} : StrongConvexOn (WithLp.ofLp ⁻¹' stdSimplex ℝ (Fin n)) 1 fun (x : EuclideanSpace ℝ (Fin n)) => (negative_entropy_on_stdSimplex n x.ofLp).toReal

Proposition 5.14 (2): the negative entropy on the unit simplex is 1-strongly convex with respect to the l_2 norm, stated in the canonical real-valued form on the simplex itself.