Local and asymptotic Lipschitz secants

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Cheeger_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_LipschitzApproximation_Kernel

noncomputable section
open MeasureTheory Filter Topology Set
open FunctionalInequalities.Energy.Euclidean.LipschitzApproximation
open scoped ENNReal NNReal ContDiff
namespace FunctionalInequalities
namespace Energy
universe u
namespace LocalSlope
section Metric
variable {X : Type*} [MetricSpace X]
/-- The one-moving-point secant supremum on the open ball of radius `r` around `x`.  The local
slope is its infimum over positive radii. -/
def secant (f : X → ℝ) (r : ℝ) (x : X) : ℝ≥0∞ :=
  ⨆ (y : X) (_ : dist y x < r), ENNReal.ofReal (dist (f y) (f x) / dist y x)
end Metric
end LocalSlope
namespace AsymptoticLipschitz
section Metric
variable {X : Type*} [MetricSpace X]
/-- The two-moving-point secant supremum on the open ball of radius `r` around `x`.  The
asymptotic Lipschitz constant is its infimum over positive radii. -/
def secant (f : X → ℝ) (r : ℝ) (x : X) : ℝ≥0∞ :=
  ⨆ (y : X) (_ : dist y x < r) (z : X) (_ : dist z x < r),
    ENNReal.ofReal (dist (f y) (f z) / dist y z)
end Metric
end AsymptoticLipschitz
end Energy
end FunctionalInequalities