theorem logarithmic_transform_concave_on {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {Q : Set E} {ψ : E → ℝ} (hψ_concave : ConcaveOn ℝ (interior Q) ψ) (hψ_pos : ∀ (x : ↑(interior Q)), 0 < ψ ↑x) : ConcaveOn ℝ (interior Q) (logarithmicTransform ψ)

Helper for Lemma 7.14: the logarithmic transform of a positive concave function is concave on the same feasible interior set.

theorem has_gradient_at_logarithmic_transform {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {Q : Set E} {ψ : E → ℝ} (hψ_grad : ∀ (x : ↑(interior Q)), HasGradientAt ψ (gradient ψ ↑x) ↑x) (hψ_pos : ∀ (x : ↑(interior Q)), 0 < ψ ↑x) (x : ↑(interior Q)) : HasGradientAt (logarithmicTransform ψ) ((ψ ↑x)⁻¹ • gradient ψ ↑x) ↑x

Helper for Lemma 7.14: differentiating x ↦ log (ψ x) multiplies the gradient of ψ by ψ x inverse.

theorem logarithmic_transform_upper_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {Q : Set E} {ψ : E → ℝ} (hψ_grad : ∀ (x : ↑(interior Q)), HasGradientAt ψ (gradient ψ ↑x) ↑x) (hψ_concave : ConcaveOn ℝ (interior Q) ψ) (hψ_pos : ∀ (x : ↑(interior Q)), 0 < ψ ↑x) (x : ↑(interior Q)) {y : E} (hy : y ∈ interior Q) : logarithmicTransform ψ y ≤ logarithmicTransform ψ ↑x + inner ℝ (gradient (logarithmicTransform ψ) ↑x) (y - ↑x)

Helper for Lemma 7.14: concavity of the logarithmic transform yields the affine upper-support inequality at each interior point.

theorem dual_norm_neg_gradient_logarithmic_transform_le_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {Q : Set E} {ψ : E → ℝ} {pointNorm : ↑(interior Q) → Seminorm ℝ E} (hpointNorm : ∀ (x : ↑(interior Q)), (pointNorm x).IsNorm) (hψ_grad : ∀ (x : ↑(interior Q)), HasGradientAt ψ (gradient ψ ↑x) ↑x) (hψ_pos : ∀ (x : ↑(interior Q)), 0 < ψ ↑x) (hψ_dual_bound : ∀ (x : ↑(interior Q)), have x_1 := ⋯; (pointNorm x).dualNorm (gradient ψ ↑x) ≤ ψ ↑x) (x : ↑(interior Q)) : have x_1 := ⋯; (pointNorm x).dualNorm (-gradient (logarithmicTransform ψ) ↑x) ≤ 1

Helper for Lemma 7.14: the negated logarithmic gradient has pointwise dual norm at most 1 under the source bound ‖∇ ψ x‖ₓ* ≤ ψ x.

theorem logarithmicTransform_has_constrained_subgradient_norm_le_one_and_concaveOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {Q : Set E} {ψ : E → ℝ} {pointNorm : ↑(interior Q) → Seminorm ℝ E} (hpointNorm : ∀ (x : ↑(interior Q)), (pointNorm x).IsNorm) (hψ_grad : ∀ (x : ↑(interior Q)), HasGradientAt ψ (gradient ψ ↑x) ↑x) (hψ_concave : ConcaveOn ℝ (interior Q) ψ) (hψ_pos : ∀ (x : ↑(interior Q)), 0 < ψ ↑x) (hψ_dual_bound : ∀ (x : ↑(interior Q)), have x_1 := ⋯; (pointNorm x).dualNorm (gradient ψ ↑x) ≤ ψ ↑x) : (∀ (x : ↑(interior Q)), -gradient (logarithmicTransform ψ) ↑x ∈ subdifferentialWithin (interior Q) (-logarithmicTransform ψ) ↑x ∧ have x_1 := ⋯; (pointNorm x).dualNorm (-gradient (logarithmicTransform ψ) ↑x) ≤ 1) ∧ (fun (y : E) => -logarithmicTransform ψ y) ∈ barrierSubgradientClass (interior Q) (interior Q) pointNorm hpointNorm 1 ∧ ConcaveOn ℝ (interior Q) (logarithmicTransform ψ)

Lemma 7.14: if ψ is concave and strictly positive on interior Q, and its gradient has pointwise pointNorm-dual norm at most ψ x, then at every x ∈ interior Q the gradient of x ↦ ln (ψ x) yields, after the standard sign flip, a constrained subgradient of y ↦ - ln (ψ y) over interior Q, written on the chapter notation -∇ (logarithmicTransform ψ) x ∈ ∂[interior Q] (-logarithmicTransform ψ) (x), and this same canonical witness has pointNorm-dual norm at most 1; equivalently the negated logarithmic transform belongs to the barrier subgradient class with bound 1; moreover x ↦ ln (ψ x) is concave on interior Q.