From a selected-curve chord inequality to its first-order bound

1. Put \(D=d(\gamma(0),\gamma(1))^2\). For 0<t<1, subtract \(F(γ(0))\) from the chord bound and divide by the strictly positive t: \[\frac{\varphi(t)-\varphi(0)}t\le F(\gamma(1))-F(\gamma(0))-\frac\alpha2(1-t)D.\] No sign restriction on \(α\) is used, and division at \(t=0\) is not performed.

2. The condition 0<t<1 holds eventually as t approaches 0 from the right. Genuine differentiability gives the restricted limit \[\lim_{t\downarrow0}\frac{\varphi(t)-\varphi(0)}t=g.\] The formal proof restricts HasDerivAt.tendsto_slope to the right-neighborhood filter; a defined-but-totalized slope value at zero is irrelevant.

3. The upper envelope \(U(t)=F(\gamma(1))-F(\gamma(0))-\frac\alpha2(1-t)D\) is continuous at zero. Taking limits in the eventual ordered inequality gives \[g\le F(\gamma(1))-F(\gamma(0))-\frac\alpha2D.\] Rearranging proves the assertion with the exact coefficient \(α/2\).

4. The proof uses the selected curve's chord inequality and scalar derivative only. It does not construct paths, prove that P encodes constant-speed geodesics, identify their velocities or define a gradient. An empty selection would make the global chord condition vacuous, but would not provide the required witness \(P(γ)\). To obtain a Riemannian or transport gradient statement one must separately identify the path derivative with the intended geometric pairing under that geometry's regularity hypotheses.

5. A totalized derivative API returns some value even when a derivative does not exist. Merely assigning that value does not justify the slope limit. The local statement explicitly supplies HasDerivAt; its proof uses only the right restriction of that stronger assumption. A genuinely one-sided variant would need its own correctly stated API, not deletion of the current premise.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.MetricSpace.Basic

open Filter Set
open scoped Topology
namespace AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity
def IsAlphaGeodesicallyConvex
    {M : Type*} [MetricSpace M]
    (isGeodesic : (ℝ → M) → Prop) (F : M → ℝ) (alpha : ℝ) : Prop :=
  ∀ path : ℝ → M, isGeodesic path →
    ∀ t : ℝ, t ∈ Icc (0 : ℝ) 1 →
      F (path t) ≤
        (1 - t) * F (path 0) + t * F (path 1) -
          (alpha * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2
end AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity
open AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity

example
    {M : Type*} [MetricSpace M]
    {isGeodesic : (ℝ → M) → Prop} {F : M → ℝ} {alpha : ℝ}
    (hconvex : IsAlphaGeodesicallyConvex isGeodesic F alpha)
    {path : ℝ → M} (hpath : isGeodesic path)
    {gradientPairing : ℝ}
    (hderiv : HasDerivAt (fun t => F (path t)) gradientPairing 0) :
    F (path 1) ≥
      F (path 0) + gradientPairing +
        alpha / 2 * dist (path 0) (path 1) ^ 2 := by
  let phi : ℝ → ℝ := fun t => F (path t)
  let upper : ℝ → ℝ := fun t =>
    F (path 1) - F (path 0) -
      alpha * (1 - t) / 2 * dist (path 0) (path 1) ^ 2
  have hslope :
      Tendsto (slope phi 0) (𝓝[>] 0) (𝓝 gradientPairing) := by
    apply hderiv.tendsto_slope.mono_left
    apply nhdsWithin_mono
    intro t ht
    simpa only [mem_compl_iff, mem_singleton_iff] using ne_of_gt ht
  have hupper :
      Tendsto upper (𝓝[>] 0) (𝓝 (upper 0)) := by
    have hcontinuous : ContinuousAt upper 0 := by
      dsimp only [upper]
      fun_prop
    have hfilter : 𝓝[>] (0 : ℝ) ≤ 𝓝 0 := inf_le_left
    exact hcontinuous.tendsto.mono_left hfilter
  have hslope_le : slope phi 0 ≤ᶠ[𝓝[>] 0] upper := by
    filter_upwards [self_mem_nhdsWithin,
      (eventually_lt_nhds zero_lt_one).filter_mono inf_le_left]
      with t ht htle
    have htpos : 0 < t := ht
    have hchord := hconvex path hpath t ⟨htpos.le, htle.le⟩
    have hquotient :
        (F (path t) - F (path 0)) / t ≤ upper t := by
      apply (div_le_iff₀ htpos).2
      dsimp only [upper]
      nlinarith
    rw [div_eq_inv_mul] at hquotient
    simpa [phi, slope, htpos.ne'] using hquotient
  have hfirst := le_of_tendsto_of_tendsto hslope hupper hslope_le
  dsimp only [upper, sub_zero, one_mul] at hfirst
  linarith

1. Derives the exact chord quotient for strictly positive t with the \(α/2\) normalization and without assuming \(α\ge 0\). (1 point)
2. Justifies eventual 0<t<1 and the right-hand slope limit from the genuine derivative hypothesis rather than a totalized value. (1 point)
3. Passes the inequality to the limit using the continuous upper envelope and rearranges the exact endpoint bound. (1 point)
4. Separates selected-curve/scalar facts from curve existence, constant-speed geodesicity and geometric gradient-pairing adapters, retaining the actual differentiability premise. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.MetricSpace.Basic

open Filter Set
open scoped Topology
namespace AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity
def IsAlphaGeodesicallyConvex
    {M : Type*} [MetricSpace M]
    (isGeodesic : (ℝ → M) → Prop) (F : M → ℝ) (alpha : ℝ) : Prop :=
  ∀ path : ℝ → M, isGeodesic path →
    ∀ t : ℝ, t ∈ Icc (0 : ℝ) 1 →
      F (path t) ≤
        (1 - t) * F (path 0) + t * F (path 1) -
          (alpha * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2
end AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity
open AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity

example
    {M : Type*} [MetricSpace M]
    {isGeodesic : (ℝ → M) → Prop} {F : M → ℝ} {alpha : ℝ}
    (hconvex : IsAlphaGeodesicallyConvex isGeodesic F alpha)
    {path : ℝ → M} (hpath : isGeodesic path)
    {gradientPairing : ℝ}
    (hderiv : HasDerivAt (fun t => F (path t)) gradientPairing 0) :
    F (path 1) ≥
      F (path 0) + gradientPairing +
        alpha / 2 * dist (path 0) (path 1) ^ 2 := by
  -- Replace this comment with your proof.

Download task template

The context supplies only the exact existing chord predicate. The reference constructs a scalar upper envelope, restricts hderiv.tendsto_slope to 𝓝[>]0, proves the quotient inequality eventually by positive division, and calls le_of_tendsto_of_tendsto before algebraic rearrangement. No source theorem or geometric gradient identity is imported as an answer. The Lean conclusion is the scalar endpoint inequality; the discussion about absent adapters is an explanation of its scope, not a new Riemannian/Wasserstein theorem.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.MetricSpace.Basic

open Filter Set
open scoped Topology
namespace AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity
def IsAlphaGeodesicallyConvex
    {M : Type*} [MetricSpace M]
    (isGeodesic : (ℝ → M) → Prop) (F : M → ℝ) (alpha : ℝ) : Prop :=
  ∀ path : ℝ → M, isGeodesic path →
    ∀ t : ℝ, t ∈ Icc (0 : ℝ) 1 →
      F (path t) ≤
        (1 - t) * F (path 0) + t * F (path 1) -
          (alpha * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2
end AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity
open AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity

example
    {M : Type*} [MetricSpace M]
    {isGeodesic : (ℝ → M) → Prop} {F : M → ℝ} {alpha : ℝ}
    (hconvex : IsAlphaGeodesicallyConvex isGeodesic F alpha)
    {path : ℝ → M} (hpath : isGeodesic path)
    {gradientPairing : ℝ}
    (hderiv : HasDerivAt (fun t => F (path t)) gradientPairing 0) :
    F (path 1) ≥
      F (path 0) + gradientPairing +
        alpha / 2 * dist (path 0) (path 1) ^ 2 := by
  let phi : ℝ → ℝ := fun t => F (path t)
  let upper : ℝ → ℝ := fun t =>
    F (path 1) - F (path 0) -
      alpha * (1 - t) / 2 * dist (path 0) (path 1) ^ 2
  have hslope :
      Tendsto (slope phi 0) (𝓝[>] 0) (𝓝 gradientPairing) := by
    apply hderiv.tendsto_slope.mono_left
    apply nhdsWithin_mono
    intro t ht
    simpa only [mem_compl_iff, mem_singleton_iff] using ne_of_gt ht
  have hupper :
      Tendsto upper (𝓝[>] 0) (𝓝 (upper 0)) := by
    have hcontinuous : ContinuousAt upper 0 := by
      dsimp only [upper]
      fun_prop
    have hfilter : 𝓝[>] (0 : ℝ) ≤ 𝓝 0 := inf_le_left
    exact hcontinuous.tendsto.mono_left hfilter
  have hslope_le : slope phi 0 ≤ᶠ[𝓝[>] 0] upper := by
    filter_upwards [self_mem_nhdsWithin,
      (eventually_lt_nhds zero_lt_one).filter_mono inf_le_left]
      with t ht htle
    have htpos : 0 < t := ht
    have hchord := hconvex path hpath t ⟨htpos.le, htle.le⟩
    have hquotient :
        (F (path t) - F (path 0)) / t ≤ upper t := by
      apply (div_le_iff₀ htpos).2
      dsimp only [upper]
      nlinarith
    rw [div_eq_inv_mul] at hquotient
    simpa [phi, slope, htpos.ne'] using hquotient
  have hfirst := le_of_tendsto_of_tendsto hslope hupper hslope_le
  dsimp only [upper, sub_zero, one_mul] at hfirst
  linarith

Download runnable reference