AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassNormalizedProduct

- The equal-mass finite product is the common mass times the product of the normalized probability laws.

theorem commonMassProduct_toMeasure_eq_mass_smul_normalized_prod
    (mu : FiniteMeasure X) (nu : FiniteMeasure Y)
    (hmass : mu.mass = nu.mass) (hpos : 0 < mu.mass) :
    (commonMassProduct mu nu : Measure (X × Y)) =
      (mu.mass : ℝ≥0) •
        ((mu.normalize : Measure X).prod (nu.normalize : Measure Y)) := by
  have hmu :
      (mu : Measure X) =
        (mu.mass : ℝ≥0) • (mu.normalize : Measure X) := by
    have h := congrArg
      (fun eta : FiniteMeasure X => (eta : Measure X))
      mu.self_eq_mass_smul_normalize
    simpa using h
  have hnu :
      (nu : Measure Y) =
        (mu.mass : ℝ≥0) • (nu.normalize : Measure Y) := by
    have h := congrArg
      (fun eta : FiniteMeasure Y => (eta : Measure Y))
      nu.self_eq_mass_smul_normalize
    simpa [← hmass] using h
  change (mu.mass⁻¹ : ℝ≥0) • ((mu : Measure X).prod (nu : Measure Y)) = _
  rw [hmu, hnu, Measure.prod_smul_left, Measure.prod_smul_right]
  simp [ne_of_gt hpos, smul_smul, mul_assoc]

end

end CommonMassNormalizedProduct
end Measure
end TechnicalLemmas
end AutoSamplingTheory

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