Asymptotic Lipschitz and local-slope relaxations

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_LocalSlope_Gradient
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Intrinsic_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_LowerSemicontinuous
import Definitions.Def_KLSModular_FunctionalInequalities_L2_MeanVariance

noncomputable section
open MeasureTheory Filter Topology
open scoped ENNReal NNReal ContDiff
namespace FunctionalInequalities
namespace Energy
universe u
namespace AsymptoticLipschitz
section Metric
variable {X : Type*} [MetricSpace X]
/-- Pointwise asymptotic Lipschitz constant `Lip_a f (x) = inf_{r > 0} Lip(f, B(x, r))`, the
infimum over radii of the two-moving-point secant supremum on the open ball.  The real quotient
at `y = z` is zero, so coincident pairs do not change the supremum.  This is not the one-moving-
point local slope `Energy.LocalSlope.apply`, which it dominates pointwise. -/
def apply (f : X → ℝ) (x : X) : ℝ≥0∞ :=
  ⨅ (r : ℝ) (_ : 0 < r), ⨆ (y : X) (_ : dist y x < r) (z : X) (_ : dist z x < r),
    ENNReal.ofReal (dist (f y) (f z) / dist y z)
end Metric
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
/-- The unnormalized squared asymptotic-Lipschitz integral in a coordinate space. -/
def energy (ν : ProbabilityMeasure V) (f : V → ℝ) : ℝ≥0∞ :=
  ∫⁻ x, apply f x ^ 2 ∂(ν : Measure V)
end AsymptoticLipschitz
namespace LocalSlope
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
/-- The finite squared local-slope pre-energy on the literature test domain, realized in real
`L²(ν)`.  The energy is finite on tests by `Admissible.finite_energy`, so `ENNReal.toNNReal`
loses nothing. -/
def preEnergy (ν : ProbabilityMeasure V) : PreEnergy (Lp ℝ 2 (ν : Measure V)) where
  Test := {f : V → ℝ // Admissible ν f}
  toAmbient f := f.2.memLp_two.toLp f.1
  energy f := (energy ν f.1).toNNReal
omit [InnerProductSpace ℝ V] [CompleteSpace V] [BorelSpace V] [SecondCountableTopology V]
  [FiniteDimensional ℝ V] in
/-- The ambient realization of a local-slope test is its `L²(ν)` class. -/
@[simp]
theorem preEnergy_toAmbient (ν : ProbabilityMeasure V) (f : {f : V → ℝ // Admissible ν f}) :
    (preEnergy ν).toAmbient f = f.2.memLp_two.toLp f.1 :=
  rfl
/-- The sequential `L²(ν)` relaxation of the squared local-slope energy over locally Lipschitz
tests.  Twice the metric Cheeger energy in the Blueprint normalization; see `Cheeger.energy`. -/
def relaxation (ν : ProbabilityMeasure V) : Functional (Lp ℝ 2 (ν : Measure V)) :=
  (preEnergy ν).sequentialRelaxation
end LocalSlope
end Energy
end FunctionalInequalities