Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
production module

AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential

13 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingClosedChainMonotonicityMathlib.Order.ConditionallyCompleteLattice.Basic externalMathlib.Topology.Order.WithTop external
Imported by
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarConvexDomainAutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarSubgradientTests.PairingRockafellarPotential
Placeholder scan
0 declaration(s) flagged
Gate status
Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.rockafellarValueSet Partial Not mapped

- Real values generated at `x` by nonempty chains rooted at `base` whose pair points all belong to `Gamma`.

def rockafellarValueSet
    (base : E × E) (Gamma : Set (E × E)) (x : E) : Set ℝ :=
  {r | ∃ l : List (E × E),
      l ≠ [] ∧ l.head? = some base ∧
        List.Forall (fun p => p ∈ Gamma) l ∧
        r = chainValue l x}

/-- The same rooted finite-chain values embedded in `WithTop ℝ`. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:33published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarValueSet Partial Not mapped

- The same rooted finite-chain values embedded in `WithTop ℝ`.

def properRockafellarValueSet
    (base : E × E) (Gamma : Set (E × E)) (x : E) : Set (WithTop ℝ) :=
  ((↑) : ℝ → WithTop ℝ) '' rockafellarValueSet base Gamma x

/-- Extended-real Rockafellar candidate.  `⊤` records target points at which the
rooted affine chain values are unbounded above. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:41published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarPotential Partial Not mapped

- Extended-real Rockafellar candidate. `⊤` records target points at which the rooted affine chain values are unbounded above.

noncomputable def properRockafellarPotential
    (base : E × E) (Gamma : Set (E × E)) (x : E) : WithTop ℝ :=
  sSup (properRockafellarValueSet base Gamma x)

/-- Finite/effective domain of an extended real potential. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:47published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.EffectiveDomain Partial Not mapped

- Finite/effective domain of an extended real potential.

def EffectiveDomain (Phi : E → WithTop ℝ) : Set E :=
  {x | Phi x < ⊤}

/-- The singleton root chain contributes its supporting affine functional. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:52published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.singleton_mem_rockafellarValueSet Partial Not mapped

- The singleton root chain contributes its supporting affine functional.

theorem singleton_mem_rockafellarValueSet
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma) (x : E) :
    inner ℝ base.2 (x - base.1) ∈ rockafellarValueSet base Gamma x := by
  refine ⟨[base], by simp, by simp, ?_, ?_⟩
  · simp [hbase]
  · simp [chainValue]

/-- Hence every rooted real value set is nonempty once the root belongs to the
relation. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:56published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.rockafellarValueSet_nonempty Partial Not mapped

- Hence every rooted real value set is nonempty once the root belongs to the relation.

theorem rockafellarValueSet_nonempty
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma) (x : E) :
    (rockafellarValueSet base Gamma x).Nonempty :=
  ⟨_, singleton_mem_rockafellarValueSet hbase x⟩

/-- The extended value set is nonempty for the same reason. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:66published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarValueSet_nonempty Partial Not mapped

- The extended value set is nonempty for the same reason.

theorem properRockafellarValueSet_nonempty
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma) (x : E) :
    (properRockafellarValueSet base Gamma x).Nonempty := by
  rcases rockafellarValueSet_nonempty hbase x with ⟨r, hr⟩
  exact ⟨(r : WithTop ℝ), ⟨r, hr, rfl⟩⟩

/-- Closed-chain nonpositivity bounds every real rooted chain value at the root
by zero. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:73published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.rockafellarValueSet_at_root_nonpos Partial Not mapped

- Closed-chain nonpositivity bounds every real rooted chain value at the root by zero.

theorem rockafellarValueSet_at_root_nonpos
    {base : E × E} {Gamma : Set (E × E)}
    (hclosed : PairingClosedChainMonotone Gamma)
    {r : ℝ} (hr : r ∈ rockafellarValueSet base Gamma base.1) :
    r ≤ 0 := by
  rcases hr with ⟨l, hlne, hhead, hforall, rfl⟩
  exact hclosed hlne hhead hforall

/-- At the root, zero is the greatest extended rooted-chain value: the singleton
chain attains zero and every closed chain is nonpositive. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:82published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.isGreatest_zero_properRockafellarValueSet_at_root Partial Not mapped

- At the root, zero is the greatest extended rooted-chain value: the singleton chain attains zero and every closed chain is nonpositive.

theorem isGreatest_zero_properRockafellarValueSet_at_root
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    IsGreatest (properRockafellarValueSet base Gamma base.1) (0 : WithTop ℝ) := by
  constructor
  · refine ⟨(0 : ℝ), ?_, by simp⟩
    simpa using singleton_mem_rockafellarValueSet hbase base.1
  · intro u hu
    rcases hu with ⟨r, hr, rfl⟩
    exact WithTop.coe_le_coe.mpr (rockafellarValueSet_at_root_nonpos hclosed hr)

/-- The proper Rockafellar candidate is normalized to zero at its chosen root. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:92published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarPotential_at_root_eq_zero Partial Not mapped

- The proper Rockafellar candidate is normalized to zero at its chosen root.

theorem properRockafellarPotential_at_root_eq_zero
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    properRockafellarPotential base Gamma base.1 = 0 := by
  have hgreatest :=
    isGreatest_zero_properRockafellarValueSet_at_root hbase hclosed
  simpa [properRockafellarPotential] using hgreatest.csSup_eq

/-- Therefore the root belongs to the finite domain of the extended potential. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:105published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.root_mem_effectiveDomain Partial Not mapped

- Therefore the root belongs to the finite domain of the extended potential.

theorem root_mem_effectiveDomain
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    base.1 ∈ EffectiveDomain (properRockafellarPotential base Gamma) := by
  change properRockafellarPotential base Gamma base.1 < ⊤
  rw [properRockafellarPotential_at_root_eq_zero hbase hclosed]
  simp

/-- In particular, the finite domain is nonempty. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:115published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.effectiveDomain_nonempty Partial Not mapped

- In particular, the finite domain is nonempty.

theorem effectiveDomain_nonempty
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    (EffectiveDomain (properRockafellarPotential base Gamma)).Nonempty :=
  ⟨base.1, root_mem_effectiveDomain hbase hclosed⟩

/-- Direct composition from the transport-produced distinct-cycle condition. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:125published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarPotential_at_root_eq_zero_of_distinct Partial Not mapped

- Direct composition from the transport-produced distinct-cycle condition.

theorem properRockafellarPotential_at_root_eq_zero_of_distinct
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hmono : PairingDistinctCycleMonotone Gamma) :
    properRockafellarPotential base Gamma base.1 = 0 :=
  properRockafellarPotential_at_root_eq_zero hbase
    (pairingClosedChainMonotone_of_distinct hmono)

end

end PairingRockafellarPotential
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean:133published source at ed709a7f320d

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean — full module with imports and context
Download module (.lean)
import AutoSamplingTheory.TechnicalLemmas.Analysis.PairingClosedChainMonotonicity
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Topology.Order.WithTop

/-!
# List-based proper Rockafellar potential

This module starts the convex-potential side of the Brenier frontier from the
canonical ASTIS list interface.  A rooted nonempty chain of pair points in
`Gamma` contributes its affine `PairingClosedChain.chainValue`; the potential is
the supremum of all such real values inside `WithTop ℝ`.

The first theorem boundary is deliberately small.  Under closed-chain
nonpositivity, the chosen root has potential exactly zero, hence the extended
potential is proper in the minimal sense that its finite domain is nonempty.
Convexity, lower semicontinuity, and subgradient containment are downstream
nodes.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace Analysis
namespace PairingRockafellarPotential

open PairingClosedChain PairingClosedChainMonotonicity

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/-- Real values generated at `x` by nonempty chains rooted at `base` whose pair
points all belong to `Gamma`. -/
def rockafellarValueSet
    (base : E × E) (Gamma : Set (E × E)) (x : E) : Set ℝ :=
  {r | ∃ l : List (E × E),
      l ≠ [] ∧ l.head? = some base ∧
        List.Forall (fun p => p ∈ Gamma) l ∧
        r = chainValue l x}

/-- The same rooted finite-chain values embedded in `WithTop ℝ`. -/
def properRockafellarValueSet
    (base : E × E) (Gamma : Set (E × E)) (x : E) : Set (WithTop ℝ) :=
  ((↑) : ℝ → WithTop ℝ) '' rockafellarValueSet base Gamma x

/-- Extended-real Rockafellar candidate.  `⊤` records target points at which the
rooted affine chain values are unbounded above. -/
noncomputable def properRockafellarPotential
    (base : E × E) (Gamma : Set (E × E)) (x : E) : WithTop ℝ :=
  sSup (properRockafellarValueSet base Gamma x)

/-- Finite/effective domain of an extended real potential. -/
def EffectiveDomain (Phi : E → WithTop ℝ) : Set E :=
  {x | Phi x < ⊤}

/-- The singleton root chain contributes its supporting affine functional. -/
theorem singleton_mem_rockafellarValueSet
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma) (x : E) :
    inner ℝ base.2 (x - base.1) ∈ rockafellarValueSet base Gamma x := by
  refine ⟨[base], by simp, by simp, ?_, ?_⟩
  · simp [hbase]
  · simp [chainValue]

/-- Hence every rooted real value set is nonempty once the root belongs to the
relation. -/
theorem rockafellarValueSet_nonempty
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma) (x : E) :
    (rockafellarValueSet base Gamma x).Nonempty :=
  ⟨_, singleton_mem_rockafellarValueSet hbase x⟩

/-- The extended value set is nonempty for the same reason. -/
theorem properRockafellarValueSet_nonempty
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma) (x : E) :
    (properRockafellarValueSet base Gamma x).Nonempty := by
  rcases rockafellarValueSet_nonempty hbase x with ⟨r, hr⟩
  exact ⟨(r : WithTop ℝ), ⟨r, hr, rfl⟩⟩

/-- Closed-chain nonpositivity bounds every real rooted chain value at the root
by zero. -/
theorem rockafellarValueSet_at_root_nonpos
    {base : E × E} {Gamma : Set (E × E)}
    (hclosed : PairingClosedChainMonotone Gamma)
    {r : ℝ} (hr : r ∈ rockafellarValueSet base Gamma base.1) :
    r ≤ 0 := by
  rcases hr with ⟨l, hlne, hhead, hforall, rfl⟩
  exact hclosed hlne hhead hforall

/-- At the root, zero is the greatest extended rooted-chain value: the singleton
chain attains zero and every closed chain is nonpositive. -/
theorem isGreatest_zero_properRockafellarValueSet_at_root
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    IsGreatest (properRockafellarValueSet base Gamma base.1) (0 : WithTop ℝ) := by
  constructor
  · refine ⟨(0 : ℝ), ?_, by simp⟩
    simpa using singleton_mem_rockafellarValueSet hbase base.1
  · intro u hu
    rcases hu with ⟨r, hr, rfl⟩
    exact WithTop.coe_le_coe.mpr (rockafellarValueSet_at_root_nonpos hclosed hr)

/-- The proper Rockafellar candidate is normalized to zero at its chosen root. -/
theorem properRockafellarPotential_at_root_eq_zero
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    properRockafellarPotential base Gamma base.1 = 0 := by
  have hgreatest :=
    isGreatest_zero_properRockafellarValueSet_at_root hbase hclosed
  simpa [properRockafellarPotential] using hgreatest.csSup_eq

/-- Therefore the root belongs to the finite domain of the extended potential. -/
theorem root_mem_effectiveDomain
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    base.1 ∈ EffectiveDomain (properRockafellarPotential base Gamma) := by
  change properRockafellarPotential base Gamma base.1 < ⊤
  rw [properRockafellarPotential_at_root_eq_zero hbase hclosed]
  simp

/-- In particular, the finite domain is nonempty. -/
theorem effectiveDomain_nonempty
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChainMonotone Gamma) :
    (EffectiveDomain (properRockafellarPotential base Gamma)).Nonempty :=
  ⟨base.1, root_mem_effectiveDomain hbase hclosed⟩

/-- Direct composition from the transport-produced distinct-cycle condition. -/
theorem properRockafellarPotential_at_root_eq_zero_of_distinct
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hmono : PairingDistinctCycleMonotone Gamma) :
    properRockafellarPotential base Gamma base.1 = 0 :=
  properRockafellarPotential_at_root_eq_zero hbase
    (pairingClosedChainMonotone_of_distinct hmono)

end

end PairingRockafellarPotential
end Analysis
end TechnicalLemmas
end AutoSamplingTheory