Documentation

TauCeti.Analysis.Convex.MongeAmpere.Transport

Weighted Monge–Ampère measures of transport potentials #

Let E be a finite-dimensional real inner product space, f : E → EReal convex (convex real epigraph, never ⊥) with D the interior of its effective domain, and let μ and ν be measures on E with ν absolutely continuous with respect to an additive Haar measure. The weighted Monge–Ampère measure MA_{f,ν}(s) = ν(∂f(s ∩ D)) (TauCeti.mongeAmpereMeasure ν f) gives the weak sense in which f solves the transport equation g₁(∇f) det D²f = g₀ for densities μ = g₀ dx and ν = g₁ dy: then MA_{f,ν}(s) = ∫_{∂f(s ∩ D)} g₁, and the equation MA_{f,ν} = μ says ∫_{∂f(s ∩ D)} g₁ = ∫_s g₀ for every measurable s, without dividing by g₁(∇f) or differentiating ∇f.

This file shows that a transport map selecting subgradients of f makes f a weak solution: if T x ∈ ∂f(x) for μ-almost every x, μ is carried by D, and T pushes μ to ν, then MA_{f,ν} = μ (TauCeti.mongeAmpereMeasure_eq_of_hasLaw). Absolute continuity of ν is what makes the subgradient images of disjoint sets ν-almost disjoint: almost no point is a subgradient at two distinct points (TauCeti.measure_setOf_exists_ne_mem_subdifferential_eq_zero), so T⁻¹(∂f(s ∩ D)) agrees with s up to a μ-null set.

Conversely, if μ is absolutely continuous as well and ν is carried by the subgradient image ∂f(D), then MA_{f,ν} = μ forces the gradient of f to push μ to ν (TauCeti.hasLaw_gradient_of_mongeAmpereMeasure_eq). The coverage hypothesis cannot be dropped: MA_{f,ν} does not see the part of ν outside ∂f(D). Together, these characterise the potentials whose gradient pushes an absolutely continuous μ to an absolutely continuous ν (TauCeti.hasLaw_gradient_and_ae_ne_top_iff_mongeAmpereMeasure_eq_and_ae_mem_subgradientImage). Applied to the potential of Brenier's theorem, this says that the Brenier potential is a weak solution of its transport equation (TauCeti.exists_isKantorovichOptimalTransportMap_gradient_and_mongeAmpereMeasure_eq, in TauCeti.MeasureTheory.OptimalTransport.Brenier).

A weak solution need not be an Aleksandrov solution, one whose unweighted measure MA_f(s) = ρ(∂f(s ∩ D)), for an additive Haar measure ρ, is g₀ / g₁(∇f) dx. For ν = g ρ with g finite almost everywhere, the transport identity holds for every weight h, MA_{f, h ν} = h (T x) μ, and splitting ρ into g⁻¹ ν and its restriction to {g = 0} gives

MA_f = (g ∘ T)⁻¹ μ + MA_{f, ρ|{g = 0}}.

The second term is subgradient mass that the target does not see, and it vanishes exactly when ρ(∂f(D) ∩ {g = 0}) = 0. This holds when every slope of f lies in the closure of a convex set on which g is positive almost everywhere, because the frontier of a convex set is null. The Brenier corollary is TauCeti.exists_isKantorovichOptimalTransportMap_gradient_and_mongeAmpereMeasure_eq_withDensity, in TauCeti.MeasureTheory.OptimalTransport.Brenier.

Main statements #

References #

theorem TauCeti.mongeAmpereMeasure_eq_of_hasLaw {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : MeasureTheory.Measure E} {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) (hν : ν.AbsolutelyContinuous ρ) {T : E → E} (hT : ProbabilityTheory.HasLaw T ν μ) (hD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) (hsub : ∀ᵐ (x : E) ∂μ, T x ∈ subdifferential (innerₗ E) f x) :

A transport map selecting subgradients gives a weak solution of the Monge–Ampère equation. Let f : E → EReal be convex and never ⊥ on a finite-dimensional real inner product space, with D the interior of its effective domain, and let ν be absolutely continuous with respect to an additive Haar measure. If T pushes μ to ν, μ is carried by D, and T x ∈ ∂f(x) for μ-almost every x, then the Monge–Ampère measure of f weighted by ν is μ: ν(∂f(s ∩ D)) = μ(s) for every measurable s.

theorem TauCeti.hasLaw_gradient_of_mongeAmpereMeasure_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : MeasureTheory.Measure E} {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) (hμ : μ.AbsolutelyContinuous ρ) (hν : ν.AbsolutelyContinuous ρ) (hMA : mongeAmpereMeasure ν f = μ) (hcov : ∀ᵐ (y : E) ∂ν, y ∈ subgradientImage (innerₗ E) f (interior {x : E | f x ≠ ⊤})) :
ProbabilityTheory.HasLaw (gradient fun (x : E) => (f x).toReal) ν μ

A weak solution of the Monge–Ampère equation transports by its gradient. Let f : E → EReal be convex and never ⊥ on a finite-dimensional real inner product space, with D the interior of its effective domain, and let μ and ν be absolutely continuous with respect to an additive Haar measure. If the Monge–Ampère measure of f weighted by ν is μ and ν-almost every point is a subgradient of f at a point of D, then the gradient of the real representative of f pushes μ to ν.

Weak solutions of the Monge–Ampère equation are the transporting potentials. Let f : E → EReal be convex and never ⊥ on a finite-dimensional real inner product space, with D the interior of its effective domain, and let μ and ν be absolutely continuous with respect to an additive Haar measure. The gradient of the real representative of f pushes μ to ν, with f finite μ-almost everywhere, exactly when the Monge–Ampère measure of f weighted by ν is μ and ν-almost every point is a subgradient of f at a point of D.

Aleksandrov solutions #

theorem TauCeti.mongeAmpereMeasure_withDensity_eq_of_hasLaw {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : MeasureTheory.Measure E} {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) (hν : ν.AbsolutelyContinuous ρ) {T : E → E} (hT : ProbabilityTheory.HasLaw T ν μ) (hD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) (hsub : ∀ᵐ (x : E) ∂μ, T x ∈ subdifferential (innerₗ E) f x) {h : E → ENNReal} (hh : Measurable h) :
mongeAmpereMeasure (ν.withDensity h) f = μ.withDensity fun (x : E) => h (T x)

A transport map selecting subgradients computes the weighted Monge–Ampère measures. Let f : E → EReal be convex and never ⊥, with D the interior of its effective domain, and let ν be absolutely continuous with respect to an additive Haar measure. If T pushes μ to ν, μ is carried by D, and T x ∈ ∂f(x) for μ-almost every x, then for every measurable weight h the Monge–Ampère measure of f weighted by h ν is h (T x) μ: ∫_{∂f(s ∩ D)} h dν = ∫_s h (T x) dμ for every measurable s.

theorem TauCeti.mongeAmpereMeasure_eq_withDensity_inv_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ : MeasureTheory.Measure E} {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {g : E → ENNReal} (hg : Measurable g) (hgtop : ∀ᵐ (y : E) ∂ρ, g y ≠ ⊤) {T : E → E} (hT : ProbabilityTheory.HasLaw T (ρ.withDensity g) μ) (hD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) (hsub : ∀ᵐ (x : E) ∂μ, T x ∈ subdifferential (innerₗ E) f x) :
mongeAmpereMeasure ρ f = (μ.withDensity fun (x : E) => (g (T x))⁻¹) + mongeAmpereMeasure (ρ.restrict {y : E | g y = 0}) f

The Aleksandrov measure of a transporting potential. Let f : E → EReal be convex and never ⊥, with D the interior of its effective domain, let ρ be an additive Haar measure, and let g be a measurable density, finite almost everywhere. If T pushes μ to g ρ, μ is carried by D, and T x ∈ ∂f(x) for μ-almost every x, then the Aleksandrov Monge–Ampère measure of f is

MA_f = (g ∘ T)⁻¹ μ + MA_{f, ρ|{g = 0}},

where the second term s ↦ ρ(∂f(s ∩ D) ∩ {g = 0}) is the subgradient mass that falls where the target density vanishes. For μ = g₀ ρ the first term is the right-hand side g₀ / g(∇f) of the Monge–Ampère equation det D²f = g₀ / g(∇f).

theorem TauCeti.mongeAmpereMeasure_eq_withDensity_inv_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ : MeasureTheory.Measure E} {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {g : E → ENNReal} (hg : Measurable g) (hgtop : ∀ᵐ (y : E) ∂ρ, g y ≠ ⊤) {T : E → E} (hT : ProbabilityTheory.HasLaw T (ρ.withDensity g) μ) (hD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) (hsub : ∀ᵐ (x : E) ∂μ, T x ∈ subdifferential (innerₗ E) f x) :
(mongeAmpereMeasure ρ f = μ.withDensity fun (x : E) => (g (T x))⁻¹) ↔ ρ (subgradientImage (innerₗ E) f (interior {x : E | f x ≠ ⊤}) ∩ {y : E | g y = 0}) = 0

When a transporting potential is an Aleksandrov solution. Let f : E → EReal be convex and never ⊥, with D the interior of its effective domain, let ρ be an additive Haar measure, and let g be a measurable density, finite almost everywhere. If T pushes μ to g ρ, μ is carried by D, and T x ∈ ∂f(x) for μ-almost every x, then f is an Aleksandrov solution of the Monge–Ampère equation MA_f = (g ∘ T)⁻¹ μ exactly when the subgradient image of D meets the zero set of the target density in a null set. Subgradient mass where g vanishes is the zero-density remainder of mongeAmpereMeasure_eq_withDensity_inv_add, invisible to the weighted transport equation MA_{f, g ρ} = μ, and it is exactly the obstruction.

theorem TauCeti.mongeAmpereMeasure_eq_withDensity_inv_of_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ : MeasureTheory.Measure E} {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {g : E → ENNReal} (hg : Measurable g) (hgtop : ∀ᵐ (y : E) ∂ρ, g y ≠ ⊤) {T : E → E} (hT : ProbabilityTheory.HasLaw T (ρ.withDensity g) μ) (hD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) (hsub : ∀ᵐ (x : E) ∂μ, T x ∈ subdifferential (innerₗ E) f x) {Y : Set E} (hY : Convex ℝ Y) (hsubY : subgradientImage (innerₗ E) f (interior {x : E | f x ≠ ⊤}) ⊆ closure Y) (hgY : ∀ᵐ (y : E) ∂ρ, y ∈ Y → g y ≠ 0) :
mongeAmpereMeasure ρ f = μ.withDensity fun (x : E) => (g (T x))⁻¹

Transporting potentials with slopes in a convex target are Aleksandrov solutions. Let f : E → EReal be convex and never ⊥, with D the interior of its effective domain, let ρ be an additive Haar measure, and let g be a measurable density, finite almost everywhere. Suppose T pushes μ to g ρ, μ is carried by D, and T x ∈ ∂f(x) for μ-almost every x. If every subgradient of f at a point of D lies in the closure of a convex set Y on which g is almost everywhere positive, then f is an Aleksandrov solution of MA_f = (g ∘ T)⁻¹ μ. Convexity enters because the frontier of a convex set is null.