AutoSamplingTheory.TechnicalLemmas.Measure.StrictCycleCheaperLocalReplacement

- A strict positive cycle through distinct support points yields positive local blocks whose canonical inverse-successor marginal replacement is strictly cheaper than the common-mass slice sum removed from those blocks.

theorem exists_localBlocks_cyclicReplacement_lt_of_cycleValue_pos
    {n : ℕ} (gamma : FiniteMeasure (E × E))
    {p : Fin (n + 1) → E × E}
    (hp : Function.Injective p)
    (hcycle : 0 < cycleValue p)
    (hsupp : ∀ i, p i ∈ (gamma : Measure (E × E)).support) :
    ∃ localBlock : Fin (n + 1) → FiniteMeasure (E × E),
      (∀ i, 0 < (localBlock i).mass) ∧
      ((↑(∑ i, localBlock i) : Measure (E × E)) ≤
        (gamma : Measure (E × E))) ∧
      (∫ z : E × E, realQuadraticCost z
          ∂(commonSlicePermutationReplacement localBlock
            (cycleSuccessorPerm (n := n)).symm : Measure (E × E))) <
        ∫ z : E × E, realQuadraticCost z
          ∂(commonSliceRemoved localBlock : Measure (E × E)) := by
  obtain ⟨ε, hε, U, V, hU, hV, _hpair, hlocalPos, hlocalLe, hstable⟩ :=
    exists_quantitative_positive_local_blocks_of_cycleValue_pos
      gamma hp hcycle hsupp (r := (1 : ℝ)) zero_lt_one
  let localBlock : Fin (n + 1) → FiniteMeasure (E × E) :=
    fun i => gamma.restrict (U i ×ˢ V i)
  let slice : Fin (n + 1) → FiniteMeasure (E × E) :=
    fun i => commonMassSliceFamily localBlock i
  have hlocalPos' : ∀ i, 0 < (localBlock i).mass := by
    intro i
    simpa [localBlock] using hlocalPos i
  have hlocalLe' :
      (↑(∑ i, localBlock i) : Measure (E × E)) ≤
        (gamma : Measure (E × E)) := by
    simpa [localBlock] using hlocalLe
  have hsliceMass : ∀ i, (slice i).mass = commonRemovableMass localBlock := by
    intro i
    simpa [slice] using commonMassSliceFamily_mass localBlock hlocalPos' i
  have hslicePos : ∀ i, 0 < (slice i).mass := by
    intro i
    simpa [slice] using commonMassSliceFamily_mass_pos localBlock hlocalPos' i
  have hprobMeasure : ∀ i,
      ((slice i).normalize : Measure (E × E)) (U i ×ˢ V i) = 1 := by
    intro i
    have hle : (slice i : Measure (E × E)) ≤
        (gamma : Measure (E × E)).restrict (U i ×ˢ V i) := by
      simpa [slice, localBlock] using
        commonMassSliceFamily_toMeasure_le localBlock hlocalPos' i
    exact normalize_apply_eq_one_of_toMeasure_le_restrict
      (slice i) gamma ((hU i).1.measurableSet.prod (hV i).1.measurableSet)
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Measure/StrictCycleCheaperLocalReplacement.lean:53published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.