production module

`AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Geometry/MetricCurve.lean.

Imports

Mathlib.MeasureTheory.Measure.Lebesgue.Basic externalMathlib.Topology.MetricSpace.Basic external

Imported by

AutoSamplingTheory.TechnicalLemmas.GeometryAutoSamplingTheory.TechnicalLemmas.RegistryTests.MetricCurve

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve.HasMetricDerivativeAt Partial Not mapped

- 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 ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve.IsAbsolutelyContinuousMetricCurve Partial Compiled

- 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 ed709a7f320dOpen detailed card

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Geometry/MetricCurve.lean — full module with imports and context

Download module (.lean)

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Topology.MetricSpace.Basic

/-!
# Metric derivatives of curves

This is the metric-space interface behind Chewi's informal Definition 1.3.16.
It does not presuppose a linear tangent space or a Wasserstein velocity field.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace Geometry
namespace MetricCurve

open Filter MeasureTheory Set
open scoped Topology

/-- 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. -/
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