Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
production module

AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement

14 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassMathlib.Algebra.BigOperators.Group.Finset.Basic external
Imported by
AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacementAutoSamplingTheory.TechnicalLemmas.Measure.PermutedReplacementQuadraticCostTests.PermutedMarginalReplacement
Placeholder scan
0 declaration(s) flagged
Gate status
Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.mass_map_of_measurable Partial Not mapped

No declaration docstring.

theorem mass_map_of_measurable
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (rho : FiniteMeasure A) (f : A → B) (hf : Measurable f) :
    (rho.map f).mass = rho.mass := by
  unfold FiniteMeasure.mass
  rw [FiniteMeasure.map_apply rho hf MeasurableSet.univ]
  simp

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:27published source at 0e31a3cda412

def AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.sourceMarginal Partial Not mapped

No declaration docstring.

noncomputable def sourceMarginal (rho : FiniteMeasure (X × Y)) : FiniteMeasure X :=
  rho.map Prod.fst

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

def AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.targetMarginal Partial Not mapped

No declaration docstring.

noncomputable def targetMarginal (rho : FiniteMeasure (X × Y)) : FiniteMeasure Y :=
  rho.map Prod.snd

@[simp]

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:38published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.sourceMarginal_mass Partial Not mapped

No declaration docstring.

theorem sourceMarginal_mass (rho : FiniteMeasure (X × Y)) :
    (sourceMarginal rho).mass = rho.mass := by
  exact mass_map_of_measurable rho Prod.fst measurable_fst

@[simp]

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.targetMarginal_mass Partial Not mapped

No declaration docstring.

theorem targetMarginal_mass (rho : FiniteMeasure (X × Y)) :
    (targetMarginal rho).mass = rho.mass := by
  exact mass_map_of_measurable rho Prod.snd measurable_snd

/-- Pushforward commutes with a finite sum of finite measures. -/

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:47published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.finiteMeasure_map_finset_sum Partial Not mapped

- Pushforward commutes with a finite sum of finite measures.

theorem finiteMeasure_map_finset_sum
    {A B I : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (s : Finset I) (rho : I → FiniteMeasure A) (f : A → B)
    (hf : Measurable f) :
    (s.sum rho).map f = s.sum (fun i => (rho i).map f) := by
  classical
  induction s using Finset.induction_on with
  | empty =>
      simp only [Finset.sum_empty]
      apply FiniteMeasure.eq_of_forall_apply_eq
      intro t ht
      rw [FiniteMeasure.map_apply (0 : FiniteMeasure A) hf ht]
      simp
  | @insert a s ha ih =>
      rw [Finset.sum_insert ha, FiniteMeasure.map_add hf, ih, Finset.sum_insert ha]

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:52published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.finiteMeasure_map_fintype_sum Partial Not mapped

No declaration docstring.

theorem finiteMeasure_map_fintype_sum
    {A B I : Type*} [MeasurableSpace A] [MeasurableSpace B] [Fintype I]
    (rho : I → FiniteMeasure A) (f : A → B) (hf : Measurable f) :
    (∑ i, rho i).map f = ∑ i, (rho i).map f := by
  classical
  exact finiteMeasure_map_finset_sum Finset.univ rho f hf

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

def AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint Partial Not mapped

No declaration docstring.

noncomputable def permutedMarginalJoint {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) :
    FiniteMeasure (X × Y) :=
  commonMassProduct (sourceMarginal (rho i)) (targetMarginal (rho (σ i)))

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:75published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint_map_fst Partial Not mapped

No declaration docstring.

theorem permutedMarginalJoint_map_fst {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) (m : ℝ≥0)
    (hmass : ∀ i, (rho i).mass = m) (hpos : 0 < m)
    (i : Fin (n + 1)) :
    (permutedMarginalJoint rho σ i).map Prod.fst = sourceMarginal (rho i) := by
  apply commonMassProduct_map_fst
  · simp [hmass]
  · simpa [hmass] using hpos

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint_map_snd Partial Not mapped

No declaration docstring.

theorem permutedMarginalJoint_map_snd {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) (m : ℝ≥0)
    (hmass : ∀ i, (rho i).mass = m) (hpos : 0 < m)
    (i : Fin (n + 1)) :
    (permutedMarginalJoint rho σ i).map Prod.snd = targetMarginal (rho (σ i)) := by
  apply commonMassProduct_map_snd
  · simp [hmass]
  · simpa [hmass] using hpos

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:91published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint_mass Partial Not mapped

No declaration docstring.

theorem permutedMarginalJoint_mass {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) (m : ℝ≥0)
    (hmass : ∀ i, (rho i).mass = m) (hpos : 0 < m)
    (i : Fin (n + 1)) :
    (permutedMarginalJoint rho σ i).mass = m := by
  calc
    (permutedMarginalJoint rho σ i).mass
        = (sourceMarginal (rho i)).mass := by
          apply commonMassProduct_mass
          · simp [hmass]
          · simpa [hmass] using hpos
    _ = (rho i).mass := sourceMarginal_mass (rho i)
    _ = m := hmass i

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:101published source at 0e31a3cda412

def AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalReplacement Partial Not mapped

No declaration docstring.

noncomputable def permutedMarginalReplacement {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) : FiniteMeasure (X × Y) :=
  ∑ i, permutedMarginalJoint rho σ i

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:116published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalReplacement_map_fst Partial Not mapped

No declaration docstring.

theorem permutedMarginalReplacement_map_fst {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) (m : ℝ≥0)
    (hmass : ∀ i, (rho i).mass = m) (hpos : 0 < m) :
    (permutedMarginalReplacement rho σ).map Prod.fst =
      (∑ i, rho i).map Prod.fst := by
  classical
  calc
    (permutedMarginalReplacement rho σ).map Prod.fst
        = ∑ i, (permutedMarginalJoint rho σ i).map Prod.fst := by
          simpa [permutedMarginalReplacement] using
            (finiteMeasure_map_fintype_sum
              (fun i => permutedMarginalJoint rho σ i) Prod.fst measurable_fst)
    _ = ∑ i, sourceMarginal (rho i) := by
          apply Finset.sum_congr rfl
          intro i _hi
          exact permutedMarginalJoint_map_fst rho σ m hmass hpos i
    _ = ∑ i, (rho i).map Prod.fst := by rfl
    _ = (∑ i, rho i).map Prod.fst := by
          exact (finiteMeasure_map_fintype_sum rho Prod.fst measurable_fst).symm

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:121published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalReplacement_map_snd Partial Not mapped

No declaration docstring.

theorem permutedMarginalReplacement_map_snd {n : ℕ}
    (rho : Fin (n + 1) → FiniteMeasure (X × Y))
    (σ : Equiv.Perm (Fin (n + 1))) (m : ℝ≥0)
    (hmass : ∀ i, (rho i).mass = m) (hpos : 0 < m) :
    (permutedMarginalReplacement rho σ).map Prod.snd =
      (∑ i, rho i).map Prod.snd := by
  classical
  calc
    (permutedMarginalReplacement rho σ).map Prod.snd
        = ∑ i, (permutedMarginalJoint rho σ i).map Prod.snd := by
          simpa [permutedMarginalReplacement] using
            (finiteMeasure_map_fintype_sum
              (fun i => permutedMarginalJoint rho σ i) Prod.snd measurable_snd)
    _ = ∑ i, targetMarginal (rho (σ i)) := by
          apply Finset.sum_congr rfl
          intro i _hi
          exact permutedMarginalJoint_map_snd rho σ m hmass hpos i
    _ = ∑ i, targetMarginal (rho i) :=
          Equiv.sum_comp σ (fun i => targetMarginal (rho i))
    _ = ∑ i, (rho i).map Prod.snd := by rfl
    _ = (∑ i, rho i).map Prod.snd := by
          exact (finiteMeasure_map_fintype_sum rho Prod.snd measurable_snd).symm

end

end PermutedMarginalReplacement
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean:142published source at 0e31a3cda412