production module

`AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean.

Imports

Mathlib.MeasureTheory.Integral.Bochner.Basic externalMathlib.MeasureTheory.Measure.Prod external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.RegistryTests.KantorovichDual

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.DualFeasible Compiled Not mapped

- A pair of integrable potentials is dual-feasible when its sum is bounded by the cost almost everywhere under the product of the marginals.

def DualFeasible
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F)
    (f : E → ℝ) (g : F → ℝ) : Prop :=
  Integrable f mu ∧ Integrable g nu ∧
    ∀ᵐ z ∂mu.prod nu, f z.1 + g z.2 ≤ cost z

/-- Chewi Definition 1.3.6: the value of the Kantorovich dual optimization
problem.  At the source's finite-second-moment quadratic cost, the feasible
objectives are nonempty and bounded above; those analytic facts are not hidden
inside this definition. -/

AutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean:21published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.dualTransportValue Compiled Compiled

- Chewi Definition 1.3.6: the value of the Kantorovich dual optimization problem. At the source's finite-second-moment quadratic cost, the feasible objectives are nonempty and bounded above; those analytic facts are not hidden inside this definition.

noncomputable def dualTransportValue
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F) : ℝ :=
  sSup {r : ℝ | ∃ (f : E → ℝ) (g : F → ℝ),
    DualFeasible cost mu nu f g ∧
      r = (∫ x, f x ∂mu) + ∫ y, g y ∂nu}

/-- Chewi display (1.3.7): source-facing expansion of the dual value. -/

AutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean:32published source at 7bcd37294df1Open detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.dualTransportValue_eq_sSup Compiled Compiled

- Chewi display (1.3.7): source-facing expansion of the dual value.

theorem dualTransportValue_eq_sSup
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F) :
    dualTransportValue cost mu nu =
      sSup {r : ℝ | ∃ (f : E → ℝ) (g : F → ℝ),
        DualFeasible cost mu nu f g ∧
          r = (∫ x, f x ∂mu) + ∫ y, g y ∂nu} :=
  rfl

end KantorovichDual
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean:40published source at 7bcd37294df1Open detailed card