production module

`AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitor`

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

Imports

Mathlib.MeasureTheory.Measure.FiniteMeasure external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitorAutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCostTests.ReplacementCompetitor

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitor.replacementCompetitor Partial Not mapped

No declaration docstring.

noncomputable def replacementCompetitor
    (remainder replacement : FiniteMeasure (X × Y)) :
    FiniteMeasure (X × Y) :=
  remainder + replacement

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitor.lean:26published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitor.replacementCompetitor_map_fst Partial Not mapped

No declaration docstring.

theorem replacementCompetitor_map_fst
    (ambient remainder removed replacement : FiniteMeasure (X × Y))
    (hdecomp : ambient = remainder + removed)
    (hmarg : replacement.map Prod.fst = removed.map Prod.fst) :
    (replacementCompetitor remainder replacement).map Prod.fst =
      ambient.map Prod.fst := by
  calc
    (replacementCompetitor remainder replacement).map Prod.fst
        = remainder.map Prod.fst + replacement.map Prod.fst := by
          simpa [replacementCompetitor] using
            (FiniteMeasure.map_add measurable_fst remainder replacement)
    _ = remainder.map Prod.fst + removed.map Prod.fst := by rw [hmarg]
    _ = (remainder + removed).map Prod.fst := by
          symm
          exact FiniteMeasure.map_add measurable_fst remainder removed
    _ = ambient.map Prod.fst := by rw [← hdecomp]

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitor.lean:31published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitor.replacementCompetitor_map_snd Partial Not mapped

No declaration docstring.

theorem replacementCompetitor_map_snd
    (ambient remainder removed replacement : FiniteMeasure (X × Y))
    (hdecomp : ambient = remainder + removed)
    (hmarg : replacement.map Prod.snd = removed.map Prod.snd) :
    (replacementCompetitor remainder replacement).map Prod.snd =
      ambient.map Prod.snd := by
  calc
    (replacementCompetitor remainder replacement).map Prod.snd
        = remainder.map Prod.snd + replacement.map Prod.snd := by
          simpa [replacementCompetitor] using
            (FiniteMeasure.map_add measurable_snd remainder replacement)
    _ = remainder.map Prod.snd + removed.map Prod.snd := by rw [hmarg]
    _ = (remainder + removed).map Prod.snd := by
          symm
          exact FiniteMeasure.map_add measurable_snd remainder removed
    _ = ambient.map Prod.snd := by rw [← hdecomp]

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitor.lean:48published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitor.replacementCompetitor_preserves_marginals Partial Not mapped

No declaration docstring.

theorem replacementCompetitor_preserves_marginals
    (ambient remainder removed replacement : FiniteMeasure (X × Y))
    (hdecomp : ambient = remainder + removed)
    (hfst : replacement.map Prod.fst = removed.map Prod.fst)
    (hsnd : replacement.map Prod.snd = removed.map Prod.snd) :
    (replacementCompetitor remainder replacement).map Prod.fst =
        ambient.map Prod.fst ∧
      (replacementCompetitor remainder replacement).map Prod.snd =
        ambient.map Prod.snd := by
  exact ⟨replacementCompetitor_map_fst ambient remainder removed replacement hdecomp hfst,
    replacementCompetitor_map_snd ambient remainder removed replacement hdecomp hsnd⟩

end

end ReplacementCompetitor
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitor.lean:65published source at 0e31a3cda412