AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicCostExpectation

- If every coordinate law is concentrated on a local set and the whole local box carries one uniform positive cycle-value margin, then the normalized cyclic re-pairing has strictly smaller expected quadratic cost. Integrability of the two finite cost functions is explicit here. The later bounded-neighborhood node discharges it from the metric-ball localization.

theorem integral_cyclicCost_lt_diagonal_of_uniform_cycleValue
    {n : ℕ}
    (mu : Fin (n + 1) → ProbabilityMeasure (E × E))
    (s : Fin (n + 1) → Set (E × E))
    (hsMeas : ∀ i, MeasurableSet (s i))
    (hsProb : ∀ i, mu i (s i) = 1)
    {ε : ℝ} (hε : 0 < ε)
    (hcycle : ∀ q : Fin (n + 1) → E × E,
      (∀ i, q i ∈ s i) → ε < cycleValue q)
    (hdiag : Integrable diagonalQuadraticCost
      (ProbabilityMeasure.pi mu : Measure (Fin (n + 1) → E × E)))
    (hcyc : Integrable
      (fun q => permutedQuadraticCost q (cycleSuccessorPerm (n := n)))
      (ProbabilityMeasure.pi mu : Measure (Fin (n + 1) → E × E))) :
    (∫ q, permutedQuadraticCost q (cycleSuccessorPerm (n := n))
        ∂(ProbabilityMeasure.pi mu : Measure (Fin (n + 1) → E × E))) <
      ∫ q, diagonalQuadraticCost q
        ∂(ProbabilityMeasure.pi mu : Measure (Fin (n + 1) → E × E)) := by
  have hbox := ae_mem_pi_box mu s hsMeas hsProb
  have hgap :
      ∀ᵐ q ∂(ProbabilityMeasure.pi mu : Measure (Fin (n + 1) → E × E)),
        2 * ε ≤ diagonalQuadraticCost q -
          permutedQuadraticCost q (cycleSuccessorPerm (n := n)) := by
    filter_upwards [hbox] with q hq
    have hcoords : ∀ i, q i ∈ s i := by
      intro i
      exact hq i (mem_univ i)
    have hcycleq := hcycle q hcoords
    rw [diagonal_sub_cyclicCost_eq_two_cycleValue]
    linarith
  exact integral_lt_integral_of_ae_gap hdiag hcyc (by linarith) hgap

end

end CyclicCostExpectation
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/CyclicCostExpectation.lean:43published source at 0e31a3cda412