AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve

- A curve has metric derivative `speed` at `t` when its distance quotient converges to that finite nonnegative real along punctured times.

def HasMetricDerivativeAt
    {M : Type*} [PseudoMetricSpace M]
    (curve : ℝ → M) (speed t : ℝ) : Prop :=
  0 ≤ speed ∧
    Tendsto
      (fun s => dist (curve s) (curve t) / |s - t|)
      (𝓝[≠] t) (𝓝 speed)

/-- Chewi Definition 1.3.16 (informal): a measure-valued curve is absolutely
continuous when a finite metric derivative exists for almost every time.

The name is intentionally source-facing: the stronger standard metric-space
definition using an integrable upper gradient is a later refinement. -/

AutoSamplingTheory/TechnicalLemmas/Geometry/MetricCurve.lean:21published source at 7bcd37294df1

- Chewi Definition 1.3.16 (informal): a measure-valued curve is absolutely continuous when a finite metric derivative exists for almost every time. The name is intentionally source-facing: the stronger standard metric-space definition using an integrable upper gradient is a later refinement.

def IsAbsolutelyContinuousMetricCurve
    {M : Type*} [PseudoMetricSpace M]
    (curve : ℝ → M) : Prop :=
  ∀ᵐ t ∂(by volume_tac : Measure ℝ),
    ∃ speed : ℝ, HasMetricDerivativeAt curve speed t

end MetricCurve
end Geometry
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Geometry/MetricCurve.lean:34published source at 7bcd37294df1Open detailed card