production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCost`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCouplingAutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpaceMathlib.MeasureTheory.Integral.Lebesgue.Map externalMathlib.Tactic external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationConstantSpeedTests.DisplacementInterpolationCost

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCost.pointMap_sub_pointMap Partial Not mapped

- Difference of two affine displacement maps.

theorem pointMap_sub_pointMap
    (s t : ℝ) (z : E × E) :
    pointMap (E := E) s z - pointMap (E := E) t z =
      (s - t) • (z.2 - z.1) := by
  unfold pointMap
  module

/-- The quadratic Wasserstein cost function is measurable on a finite-
dimensional Borel normed space. -/
@[fun_prop]

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean:39published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCost.measurable_quadraticCost Partial Not mapped

No declaration docstring.

theorem measurable_quadraticCost :
    Measurable (WassersteinSpace.quadraticCost (E := E)) := by
  unfold WassersteinSpace.quadraticCost
  fun_prop

/-- Pointwise quadratic cost scaling under the two-time displacement map. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean:49published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCost.quadraticCost_pairPointMap_eq Partial Not mapped

- Pointwise quadratic cost scaling under the two-time displacement map.

theorem quadraticCost_pairPointMap_eq
    (s t : ℝ) (z : E × E) :
    WassersteinSpace.quadraticCost (E := E)
        (pointMap (E := E) s z, pointMap (E := E) t z) =
      ENNReal.ofReal (|s - t| ^ 2) *
        WassersteinSpace.quadraticCost (E := E) z := by
  rw [WassersteinSpace.quadraticCost, pointMap_sub_pointMap]
  rw [norm_smul]
  simp only [Real.norm_eq_abs, mul_pow]
  rw [ENNReal.ofReal_mul (sq_nonneg |s - t|)]
  congr 1
  rw [WassersteinSpace.quadraticCost]
  congr 1
  exact congrArg (fun r : ℝ => r ^ 2) (norm_sub_rev z.2 z.1)

/-- The exact quadratic cost of the canonical two-time interpolation coupling
is `|s-t|^2` times the original endpoint-plan cost. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean:55published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCost.lintegral_quadraticCost_interpolationCoupling_eq

Partial Not mapped

- The exact quadratic cost of the canonical two-time interpolation coupling is `|s-t|^2` times the original endpoint-plan cost.

theorem lintegral_quadraticCost_interpolationCoupling_eq
    (gamma : Measure (E × E)) (s t : ℝ) :
    (∫⁻ w,
      WassersteinSpace.quadraticCost (E := E) w
        ∂interpolationCoupling gamma s t) =
      ENNReal.ofReal (|s - t| ^ 2) *
        ∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂gamma := by
  rw [interpolationCoupling]
  rw [lintegral_map measurable_quadraticCost (measurable_pairPointMap s t)]
  simp_rw [quadraticCost_pairPointMap_eq]
  exact lintegral_const_mul _ measurable_quadraticCost

/-- Any endpoint coupling therefore gives the expected upper bound between two
of its displacement-interpolation marginals. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean:72published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCost.wassersteinDistance_sq_interpolation_le Partial Not mapped

- Any endpoint coupling therefore gives the expected upper bound between two of its displacement-interpolation marginals.

theorem wassersteinDistance_sq_interpolation_le
    (gamma : Measure (E × E)) (s t : ℝ) :
    WassersteinSpace.wassersteinDistance
        (DisplacementInterpolation.displacementInterpolation gamma s)
        (DisplacementInterpolation.displacementInterpolation gamma t) ^ 2 ≤
      ENNReal.ofReal (|s - t| ^ 2) *
        ∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂gamma := by
  calc
    WassersteinSpace.wassersteinDistance
        (DisplacementInterpolation.displacementInterpolation gamma s)
        (DisplacementInterpolation.displacementInterpolation gamma t) ^ 2 ≤
      ∫⁻ w, WassersteinSpace.quadraticCost (E := E) w
        ∂interpolationCoupling gamma s t :=
      WassersteinSpace.wassersteinDistance_sq_le_lintegral_of_isCoupling
        _ _ _ (isCoupling_interpolationCoupling gamma s t)
    _ = ENNReal.ofReal (|s - t| ^ 2) *
        ∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂gamma :=
      lintegral_quadraticCost_interpolationCoupling_eq gamma s t

end

end DisplacementInterpolationCost
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean:86published source at 0e31a3cda412