production module

`AutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitor`

4 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/CanonicalGlobalCompetitor.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacementAutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainderAutoSamplingTheory.TechnicalLemmas.Measure.FiniteSumDominationAutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitor

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalSupportCyclicTests.CanonicalGlobalCompetitor

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitor.canonicalGlobalCompetitor Partial Not mapped

- The canonical ambient competitor associated with positive local blocks and a target-marginal permutation.

noncomputable def canonicalGlobalCompetitor {n : ℕ}
    (ambient : FiniteMeasure (X × Y))
    (localBlock : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) : FiniteMeasure (X × Y) :=
  replacementCompetitor
    (finiteRemainder ambient (commonSliceRemoved localBlock))
    (commonSlicePermutationReplacement localBlock σ)

/-- The canonical common-mass removed sum is dominated by the ambient measure
whenever the original local-block sum is dominated by the ambient measure. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CanonicalGlobalCompetitor.lean:43published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitor.commonSliceRemoved_toMeasure_le_ambient Partial Not mapped

- The canonical common-mass removed sum is dominated by the ambient measure whenever the original local-block sum is dominated by the ambient measure.

theorem commonSliceRemoved_toMeasure_le_ambient {n : ℕ}
    (ambient : FiniteMeasure (X × Y))
    (localBlock : Fin (n + 1) → FiniteMeasure (X × Y))
    (hpos : ∀ i, 0 < (localBlock i).mass)
    (hlocal : ((∑ i, localBlock i : FiniteMeasure (X × Y)) : Measure (X × Y)) ≤
      (ambient : Measure (X × Y))) :
    (commonSliceRemoved localBlock : Measure (X × Y)) ≤
      (ambient : Measure (X × Y)) := by
  unfold commonSliceRemoved
  exact toMeasure_fintypeSum_le_ambient
    (fun i => commonMassSliceFamily localBlock i) localBlock ambient
    (fun i => commonMassSliceFamily_toMeasure_le localBlock hpos i) hlocal

/-- The ambient measure decomposes into the canonical remainder plus the
canonical removed common-mass slice sum. -/

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitor.ambient_eq_remainder_add_commonSliceRemoved Partial Not mapped

- The ambient measure decomposes into the canonical remainder plus the canonical removed common-mass slice sum.

theorem ambient_eq_remainder_add_commonSliceRemoved {n : ℕ}
    (ambient : FiniteMeasure (X × Y))
    (localBlock : Fin (n + 1) → FiniteMeasure (X × Y))
    (hpos : ∀ i, 0 < (localBlock i).mass)
    (hlocal : ((∑ i, localBlock i : FiniteMeasure (X × Y)) : Measure (X × Y)) ≤
      (ambient : Measure (X × Y))) :
    ambient = finiteRemainder ambient (commonSliceRemoved localBlock) +
      commonSliceRemoved localBlock := by
  exact ambient_eq_finiteRemainder_add_removed ambient (commonSliceRemoved localBlock)
    (commonSliceRemoved_toMeasure_le_ambient ambient localBlock hpos hlocal)

/-- The canonical global competitor preserves both marginals of the ambient
joint finite measure. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CanonicalGlobalCompetitor.lean:68published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitor.canonicalGlobalCompetitor_preserves_marginals Partial Not mapped

- The canonical global competitor preserves both marginals of the ambient joint finite measure.

theorem canonicalGlobalCompetitor_preserves_marginals {n : ℕ}
    (ambient : FiniteMeasure (X × Y))
    (localBlock : Fin (n + 1) → FiniteMeasure (X × Y))
    (hpos : ∀ i, 0 < (localBlock i).mass)
    (hlocal : ((∑ i, localBlock i : FiniteMeasure (X × Y)) : Measure (X × Y)) ≤
      (ambient : Measure (X × Y)))
    (σ : Equiv.Perm (Fin (n + 1))) :
    (canonicalGlobalCompetitor ambient localBlock σ).map Prod.fst =
        ambient.map Prod.fst ∧
      (canonicalGlobalCompetitor ambient localBlock σ).map Prod.snd =
        ambient.map Prod.snd := by
  have hdecomp := ambient_eq_remainder_add_commonSliceRemoved
    ambient localBlock hpos hlocal
  have hmarg :=
    commonSlicePermutationReplacement_preserves_removed_marginals localBlock hpos σ
  exact replacementCompetitor_preserves_marginals
    ambient
    (finiteRemainder ambient (commonSliceRemoved localBlock))
    (commonSliceRemoved localBlock)
    (commonSlicePermutationReplacement localBlock σ)
    hdecomp hmarg.1 hmarg.2

end

end CanonicalGlobalCompetitor
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/CanonicalGlobalCompetitor.lean:81published source at 0e31a3cda412