AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementSupportingPotential

- A vector field `T` is a global first-order supporting field for a real potential `phi` when its affine tangent expression at every `x` lies below `phi` at every `y`.

def IsSupportingField (phi : E → ℝ) (T : E → E) : Prop :=
  ∀ x y, phi x + ⟪T x, y - x⟫ ≤ phi y

/-- A global supporting field is monotone in the Hilbert-space sense used by
the interior displacement injectivity theorem. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementSupportingPotential.lean:38published source at 0e31a3cda412

- A global supporting field is monotone in the Hilbert-space sense used by the interior displacement injectivity theorem.

theorem isMonotoneMap_of_isSupportingField
    {phi : E → ℝ} {T : E → E} (h : IsSupportingField phi T) :
    IsMonotoneMap T := by
  intro x y
  have hxy := h x y
  have hyx := h y x
  have hflip : ⟪T x, y - x⟫ = -⟪T x, x - y⟫ := by
    have hsub : y - x = -(x - y) := by abel
    rw [hsub, inner_neg_right]
  rw [hflip] at hxy
  have hscalar :
      0 ≤ ⟪T x, x - y⟫ - ⟪T y, x - y⟫ := by
    linarith
  simpa [inner_sub_left] using hscalar

/-- Direct composition of the support inequality with the previously isolated
interior-injectivity leaf. This theorem still does not assume or prove that
`phi` is convex; it only exposes the exact support contract a future Brenier
bridge must construct. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementSupportingPotential.lean:43published source at 0e31a3cda412

- Direct composition of the support inequality with the previously isolated interior-injectivity leaf. This theorem still does not assume or prove that `phi` is convex; it only exposes the exact support contract a future Brenier bridge must construct.

theorem injective_affineDisplacementMap_of_supportingField
    {phi : E → ℝ} {T : E → E} (h : IsSupportingField phi T)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    Function.Injective
      (DisplacementMapDerivative.affineDisplacementMap T t) :=
  injective_affineDisplacementMap_of_monotone
    (isMonotoneMap_of_isSupportingField h) t ht0 ht1

end DisplacementSupportingPotential
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementSupportingPotential.lean:62published source at 0e31a3cda412