Curvature of finite soft support functions

For the log-sum-exp regularization h of a finite directional support function, the support-curve curvature radius is h + h''. This file computes the two derivatives through the finite exponential partition and proves that this radius is nonnegative. The proof separates into two elementary finite inequalities: each exponent is bounded by the log partition, and weighted Cauchy--Schwarz makes the velocity variance nonnegative.

noncomputable def polytopeDirectionalVelocity (z : ℂ) (theta : ℝ) : ℝ

Angular velocity of one vertex's directional value.

Equations

• polytopeDirectionalVelocity z theta = -z.re * Real.sin theta + z.im * Real.cos theta

noncomputable def polytopeSoftPartitionFirst (u : Finset ℂ) (delta theta : ℝ) : ℝ

The first derivative of the exponential partition sum.

Equations

• polytopeSoftPartitionFirst u delta theta = ∑ z ∈ u, Real.exp (polytopeDirectionalValue z theta / delta) * (polytopeDirectionalVelocity z theta / delta)

noncomputable def polytopeSoftPartitionSecond (u : Finset ℂ) (delta theta : ℝ) : ℝ

The second derivative of the exponential partition sum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def polytopeSoftPartitionPositionMoment (u : Finset ℂ) (delta theta : ℝ) : ℝ

Weighted directional-position moment of the partition.

Equations

• polytopeSoftPartitionPositionMoment u delta theta = ∑ z ∈ u, Real.exp (polytopeDirectionalValue z theta / delta) * (polytopeDirectionalValue z theta / delta)

noncomputable def polytopeSoftPartitionVelocitySqMoment (u : Finset ℂ) (delta theta : ℝ) : ℝ

Weighted square angular-velocity moment of the partition.

Equations

• polytopeSoftPartitionVelocitySqMoment u delta theta = ∑ z ∈ u, Real.exp (polytopeDirectionalValue z theta / delta) * (polytopeDirectionalVelocity z theta / delta) ^ 2

noncomputable def polytopeSoftSupportFirst (u : Finset ℂ) (delta theta : ℝ) : ℝ

First derivative of the log-sum-exp support, in partition coordinates.

Equations

• polytopeSoftSupportFirst u delta theta = delta * (polytopeSoftPartitionFirst u delta theta / polytopeSoftPartition u delta theta)

noncomputable def polytopeSoftSupportSecond (u : Finset ℂ) (delta theta : ℝ) : ℝ

Second derivative of the log-sum-exp support, in partition coordinates.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def polytopeRoundedSupport (u : Finset ℂ) (delta rho theta : ℝ) : ℝ

A strictly rounded support function, obtained by adding a positive constant to the soft support.

Equations

• polytopeRoundedSupport u delta rho theta = polytopeSoftSupport u delta theta + rho

theorem hasDerivAt_polytopeDirectionalValue (z : ℂ) (theta : ℝ) : HasDerivAt (polytopeDirectionalValue z) (polytopeDirectionalVelocity z theta) theta

First angular derivative of a vertex directional value.

theorem hasDerivAt_polytopeDirectionalVelocity (z : ℂ) (theta : ℝ) : HasDerivAt (polytopeDirectionalVelocity z) (-polytopeDirectionalValue z theta) theta

The angular velocity differentiates to minus the directional value.

theorem hasDerivAt_polytopeSoftPartition (u : Finset ℂ) (delta theta : ℝ) : HasDerivAt (polytopeSoftPartition u delta) (polytopeSoftPartitionFirst u delta theta) theta

Exact first derivative of the finite exponential partition.

theorem hasDerivAt_polytopeSoftPartitionFirst (u : Finset ℂ) (delta theta : ℝ) : HasDerivAt (polytopeSoftPartitionFirst u delta) (polytopeSoftPartitionSecond u delta theta) theta

Exact second derivative of the finite exponential partition.

theorem hasDerivAt_polytopeSoftSupport {u : Finset ℂ} (hu : u.Nonempty) (delta theta : ℝ) : HasDerivAt (polytopeSoftSupport u delta) (polytopeSoftSupportFirst u delta theta) theta

Exact first derivative of the log-sum-exp support.

theorem hasDerivAt_polytopeSoftSupportFirst {u : Finset ℂ} (hu : u.Nonempty) (delta theta : ℝ) : HasDerivAt (polytopeSoftSupportFirst u delta) (polytopeSoftSupportSecond u delta theta) theta

Exact derivative of the first-support-derivative formula.

theorem deriv_polytopeSoftSupport {u : Finset ℂ} (hu : u.Nonempty) (delta theta : ℝ) : deriv (polytopeSoftSupport u delta) theta = polytopeSoftSupportFirst u delta theta

First derivative as an equality involving deriv.

theorem deriv_deriv_polytopeSoftSupport {u : Finset ℂ} (hu : u.Nonempty) (delta theta : ℝ) : deriv (deriv (polytopeSoftSupport u delta)) theta = polytopeSoftSupportSecond u delta theta

Second derivative as an equality involving the iterated deriv.

theorem polytopeSoftPartitionSecond_eq_velocitySqMoment_sub_positionMoment (u : Finset ℂ) (delta theta : ℝ) : polytopeSoftPartitionSecond u delta theta = polytopeSoftPartitionVelocitySqMoment u delta theta - polytopeSoftPartitionPositionMoment u delta theta

The second partition derivative is the square-velocity moment minus the position moment.

theorem polytopeSoftPartitionPositionMoment_le_log_mul_partition {u : Finset ℂ} (_hu : u.Nonempty) {delta : ℝ} (_hdelta : 0 < delta) (theta : ℝ) : polytopeSoftPartitionPositionMoment u delta theta ≤ polytopeSoftPartition u delta theta * Real.log (polytopeSoftPartition u delta theta)

The weighted position moment is at most the log partition times the partition mass.

theorem polytopeSoftPartitionFirst_sq_le_partition_mul_velocitySqMoment (u : Finset ℂ) (delta theta : ℝ) : polytopeSoftPartitionFirst u delta theta ^ 2 ≤ polytopeSoftPartition u delta theta * polytopeSoftPartitionVelocitySqMoment u delta theta

Weighted finite Cauchy--Schwarz for the first partition derivative.

theorem polytopeSoftSupport_add_second_nonneg {u : Finset ℂ} (hu : u.Nonempty) {delta : ℝ} (hdelta : 0 < delta) (theta : ℝ) : 0 ≤ polytopeSoftSupport u delta theta + polytopeSoftSupportSecond u delta theta

The log-sum-exp support has nonnegative support-curve curvature radius h + h''.

theorem polytopeSoftSupport_add_const_add_second_pos {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (theta : ℝ) : 0 < polytopeSoftSupport u delta theta + rho + polytopeSoftSupportSecond u delta theta

Adding any positive constant to the soft support makes its support-curve curvature radius strictly positive.

theorem polytopeSoftSupport_add_deriv_deriv_nonneg {u : Finset ℂ} (hu : u.Nonempty) {delta : ℝ} (hdelta : 0 < delta) (theta : ℝ) : 0 ≤ polytopeSoftSupport u delta theta + deriv (deriv (polytopeSoftSupport u delta)) theta

The actual iterated derivative form of nonnegative soft-support curvature.

theorem periodic_polytopeRoundedSupport (u : Finset ℂ) (delta rho : ℝ) : Function.Periodic (polytopeRoundedSupport u delta rho) (2 * Real.pi)

The rounded support remains 2*pi-periodic.

theorem contDiff_polytopeRoundedSupport {u : Finset ℂ} (hu : u.Nonempty) (delta rho : ℝ) : ContDiff ℝ (↑⊤) (polytopeRoundedSupport u delta rho)

The rounded support remains infinitely differentiable.

theorem deriv_deriv_polytopeRoundedSupport {u : Finset ℂ} (hu : u.Nonempty) (delta rho theta : ℝ) : deriv (deriv (polytopeRoundedSupport u delta rho)) theta = polytopeSoftSupportSecond u delta theta

Adding the rounding constant does not change the second derivative.

theorem polytopeRoundedSupport_add_deriv_deriv_pos {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (theta : ℝ) : 0 < polytopeRoundedSupport u delta rho theta + deriv (deriv (polytopeRoundedSupport u delta rho)) theta

A positive rounding constant gives strictly positive support-curve curvature radius everywhere.