production module

`AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/CyclicQuadraticCost.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleNeighborhoodAutoSamplingTheory.TechnicalLemmas.Analysis.PermutedQuadraticCost

Imported by

AutoSamplingTheory.TechnicalLemmas.AnalysisAutoSamplingTheory.TechnicalLemmas.Analysis.CycleSuccessorDistinctAutoSamplingTheory.TechnicalLemmas.Analysis.CyclicCostExpectationTests.CyclicQuadraticCost

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost.cycleSuccessorPerm Partial Not mapped

- Modular successor permutation on the nonempty finite cycle.

noncomputable def cycleSuccessorPerm {n : ℕ} : Equiv.Perm (Fin (n + 1)) :=
  Equiv.addRight (1 : Fin (n + 1))

@[simp]

AutoSamplingTheory/TechnicalLemmas/Analysis/CyclicQuadraticCost.lean:29published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost.cycleSuccessorPerm_apply Partial Not mapped

No declaration docstring.

theorem cycleSuccessorPerm_apply {n : ℕ} (i : Fin (n + 1)) :
    cycleSuccessorPerm (n := n) i = i + 1 := by
  rfl

/-- The permutation-generic pairing gap becomes exactly the existing
`cycleValue` for the modular successor. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/CyclicQuadraticCost.lean:33published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost.permutedPairingGap_cycleSuccessor_eq_cycleValue Partial Not mapped

- The permutation-generic pairing gap becomes exactly the existing `cycleValue` for the modular successor.

theorem permutedPairingGap_cycleSuccessor_eq_cycleValue
    {n : ℕ} (p : Fin (n + 1) → E × E) :
    permutedPairingGap p (cycleSuccessorPerm (n := n)) = cycleValue p := by
  simp [permutedPairingGap, cycleValue, cycleSuccessorPerm]

/-- Exact quadratic cost identity for the cyclic successor. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/CyclicQuadraticCost.lean:39published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost.diagonal_sub_cyclicCost_eq_two_cycleValue Partial Not mapped

- Exact quadratic cost identity for the cyclic successor.

theorem diagonal_sub_cyclicCost_eq_two_cycleValue
    {n : ℕ} (p : Fin (n + 1) → E × E) :
    diagonalQuadraticCost p -
        permutedQuadraticCost p (cycleSuccessorPerm (n := n)) =
      2 * cycleValue p := by
  rw [diagonal_sub_permuted_eq_two_pairingGap,
    permutedPairingGap_cycleSuccessor_eq_cycleValue]

/-- A strict positive pairing-cycle violation produces a strictly cheaper
quadratic cyclic re-pairing. -/

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

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost.cyclicQuadraticCost_lt_of_cycleValue_pos Partial Not mapped

- A strict positive pairing-cycle violation produces a strictly cheaper quadratic cyclic re-pairing.

theorem cyclicQuadraticCost_lt_of_cycleValue_pos
    {n : ℕ} (p : Fin (n + 1) → E × E)
    (hpos : 0 < cycleValue p) :
    permutedQuadraticCost p (cycleSuccessorPerm (n := n)) <
      diagonalQuadraticCost p := by
  apply permutedQuadraticCost_lt_of_pairingGap_pos
  simpa [permutedPairingGap_cycleSuccessor_eq_cycleValue] using hpos

end

end CyclicQuadraticCost
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/CyclicQuadraticCost.lean:55published source at 0e31a3cda412