AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCyclicMonotonicity

- Standard finite-cycle pairing monotonicity on a relation `Gamma`.

def PairingCycleMonotone (Gamma : Set (E × E)) : Prop :=
  ∀ n (p : Fin (n + 1) → E × E),
    (∀ i, p i ∈ Gamma) →
      (∑ i, inner ℝ (p i).2 ((p (i + 1)).1 - (p i).1)) ≤ 0

/-- The distinct-point cycle contract expected directly from the future
finite-neighborhood perturbation proof of optimality. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:45published source at 0e31a3cda412

- The distinct-point cycle contract expected directly from the future finite-neighborhood perturbation proof of optimality.

def PairingDistinctCycleMonotone (Gamma : Set (E × E)) : Prop :=
  ∀ n (p : Fin (n + 1) → E × E), Function.Injective p →
    (∀ i, p i ∈ Gamma) →
      (∑ i, inner ℝ (p i).2 ((p (i + 1)).1 - (p i).1)) ≤ 0

/-- The standard finite-cycle condition in diagonal-versus-shifted pairing
form. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:52published source at 0e31a3cda412

- The standard finite-cycle condition in diagonal-versus-shifted pairing form.

def PairingShiftedCycleMonotone (Gamma : Set (E × E)) : Prop :=
  ∀ n (p : Fin (n + 1) → E × E),
    (∀ i, p i ∈ Gamma) →
      (∑ i, inner ℝ (p i).2 (p (i + 1)).1) ≤
        ∑ i, inner ℝ (p i).2 (p i).1

/-- Pointwise algebra behind the increment and shifted cycle conventions. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:59published source at 0e31a3cda412

- Pointwise algebra behind the increment and shifted cycle conventions.

theorem cycle_increment_sum_eq_shifted_sub_diag
    {n : ℕ} (p : Fin (n + 1) → E × E) :
    (∑ i, inner ℝ (p i).2 ((p (i + 1)).1 - (p i).1)) =
      (∑ i, inner ℝ (p i).2 (p (i + 1)).1) -
        ∑ i, inner ℝ (p i).2 (p i).1 := by
  simp_rw [inner_sub_right]
  rw [Finset.sum_sub_distrib]

/-- Rockafellar increment form and diagonal/shifted form are exactly
equivalent. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:66published source at 0e31a3cda412

- Rockafellar increment form and diagonal/shifted form are exactly equivalent.

theorem pairingCycleMonotone_iff_shifted
    (Gamma : Set (E × E)) :
    PairingCycleMonotone Gamma ↔ PairingShiftedCycleMonotone Gamma := by
  constructor
  · intro h n p hmem
    have hcycle := h n p hmem
    rw [cycle_increment_sum_eq_shifted_sub_diag] at hcycle
    exact sub_nonpos.mp hcycle
  · intro h n p hmem
    rw [cycle_increment_sum_eq_shifted_sub_diag]
    exact sub_nonpos.mpr (h n p hmem)

/-- The standard all-cycle property immediately implies the distinct-cycle
contract used by perturbation arguments. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:76published source at 0e31a3cda412

- The standard all-cycle property immediately implies the distinct-cycle contract used by perturbation arguments.

theorem PairingCycleMonotone.distinct
    {Gamma : Set (E × E)}
    (hmono : PairingCycleMonotone Gamma) :
    PairingDistinctCycleMonotone Gamma := by
  intro n p _hp hmem
  exact hmono n p hmem

/-- Restricting a pairing-cyclically-monotone relation preserves the property. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:90published source at 0e31a3cda412

- Restricting a pairing-cyclically-monotone relation preserves the property.

theorem PairingCycleMonotone.mono
    {Gamma₁ Gamma₂ : Set (E × E)}
    (hsub : Gamma₁ ⊆ Gamma₂)
    (hmono : PairingCycleMonotone Gamma₂) :
    PairingCycleMonotone Gamma₁ := by
  intro n p hmem
  exact hmono n p (fun i => hsub (hmem i))

/-- Restriction also preserves the distinct-cycle contract. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:98published source at 0e31a3cda412

- Restriction also preserves the distinct-cycle contract.

theorem PairingDistinctCycleMonotone.mono
    {Gamma₁ Gamma₂ : Set (E × E)}
    (hsub : Gamma₁ ⊆ Gamma₂)
    (hmono : PairingDistinctCycleMonotone Gamma₂) :
    PairingDistinctCycleMonotone Gamma₁ := by
  intro n p hp hmem
  exact hmono n p hp (fun i => hsub (hmem i))

/-- The empty relation is vacuously pairing cyclically monotone. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:107published source at 0e31a3cda412

- The empty relation is vacuously pairing cyclically monotone.

theorem pairingCycleMonotone_empty :
    PairingCycleMonotone (∅ : Set (E × E)) := by
  intro n p hmem
  simpa using hmem 0

end

end PairingCyclicMonotonicity
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean:116published source at 0e31a3cda412