production module

`AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacement`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamilyAutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitorAutoSamplingTheory.TechnicalLemmas.Measure.StrictCycleCheaperLocalReplacementTests.CommonSlicePermutationReplacement

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacement.commonSliceRemoved Partial Not mapped

- Sum of the canonical equal-mass slices removed from the local joint blocks.

noncomputable def commonSliceRemoved {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure (X × Y)) : FiniteMeasure (X × Y) :=
  ∑ i, commonMassSliceFamily mu i

/-- Canonical replacement obtained by permuting the target marginals of the
common-mass slices. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean:29published source at 0e31a3cda412

def AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacement.commonSlicePermutationReplacement Partial Not mapped

- Canonical replacement obtained by permuting the target marginals of the common-mass slices.

noncomputable def commonSlicePermutationReplacement {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) : FiniteMeasure (X × Y) :=
  permutedMarginalReplacement (fun i => commonMassSliceFamily mu i) σ

/-- The canonical replacement has exactly the first marginal of the removed
slice sum. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean:35published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacement.commonSlicePermutationReplacement_map_fst Partial Not mapped

- The canonical replacement has exactly the first marginal of the removed slice sum.

theorem commonSlicePermutationReplacement_map_fst {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure (X × Y))
    (hpos : ∀ i, 0 < (mu i).mass)
    (σ : Equiv.Perm (Fin (n + 1))) :
    (commonSlicePermutationReplacement mu σ).map Prod.fst =
      (commonSliceRemoved mu).map Prod.fst := by
  unfold commonSlicePermutationReplacement commonSliceRemoved
  apply permutedMarginalReplacement_map_fst
      (fun i => commonMassSliceFamily mu i) σ (commonRemovableMass mu)
  · exact fun i => commonMassSliceFamily_mass mu hpos i
  · exact commonRemovableMass_pos mu hpos

/-- The canonical replacement has exactly the second marginal of the removed
slice sum. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean:42published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacement.commonSlicePermutationReplacement_map_snd Partial Not mapped

- The canonical replacement has exactly the second marginal of the removed slice sum.

theorem commonSlicePermutationReplacement_map_snd {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure (X × Y))
    (hpos : ∀ i, 0 < (mu i).mass)
    (σ : Equiv.Perm (Fin (n + 1))) :
    (commonSlicePermutationReplacement mu σ).map Prod.snd =
      (commonSliceRemoved mu).map Prod.snd := by
  unfold commonSlicePermutationReplacement commonSliceRemoved
  apply permutedMarginalReplacement_map_snd
      (fun i => commonMassSliceFamily mu i) σ (commonRemovableMass mu)
  · exact fun i => commonMassSliceFamily_mass mu hpos i
  · exact commonRemovableMass_pos mu hpos

/-- Both marginal identities packaged for the global replacement competitor. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean:56published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacement.commonSlicePermutationReplacement_preserves_removed_marginals

Partial Not mapped

- Both marginal identities packaged for the global replacement competitor.

theorem commonSlicePermutationReplacement_preserves_removed_marginals {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure (X × Y))
    (hpos : ∀ i, 0 < (mu i).mass)
    (σ : Equiv.Perm (Fin (n + 1))) :
    (commonSlicePermutationReplacement mu σ).map Prod.fst =
        (commonSliceRemoved mu).map Prod.fst ∧
      (commonSlicePermutationReplacement mu σ).map Prod.snd =
        (commonSliceRemoved mu).map Prod.snd := by
  exact ⟨commonSlicePermutationReplacement_map_fst mu hpos σ,
    commonSlicePermutationReplacement_map_snd mu hpos σ⟩

end

end CommonSlicePermutationReplacement
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean:69published source at 0e31a3cda412