AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasureIntegral

- Integrating a real observable against a finite measure is its total mass times the expectation under the normalized probability measure. The Bochner integral is totalized, so no separate integrability hypothesis is needed for this algebraic scaling identity.

theorem integral_eq_mass_mul_integral_normalize
    (mu : FiniteMeasure X) (f : X → ℝ) :
    (∫ x, f x ∂(mu : Measure X)) =
      (mu.mass : ℝ) * ∫ x, f x ∂(mu.normalize : Measure X) := by
  have hmeasure :
      (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
  rw [hmeasure, integral_smul_nnreal_measure]
  rfl

/-- Positive-mass specialization, packaged with the scalar positivity needed
to transport strict inequalities between normalized expectations and finite
measure integrals. -/

AutoSamplingTheory/TechnicalLemmas/Probability/NormalizedFiniteMeasureIntegral.lean:33published source at 0e31a3cda412

- Positive-mass specialization, packaged with the scalar positivity needed to transport strict inequalities between normalized expectations and finite measure integrals.

theorem integral_lt_integral_iff_normalize_of_mass_pos
    (mu : FiniteMeasure X) (f g : X → ℝ)
    (hpos : 0 < mu.mass) :
    (∫ x, f x ∂(mu : Measure X)) < (∫ x, g x ∂(mu : Measure X)) ↔
      (∫ x, f x ∂(mu.normalize : Measure X)) <
        (∫ x, g x ∂(mu.normalize : Measure X)) := by
  rw [integral_eq_mass_mul_integral_normalize,
    integral_eq_mass_mul_integral_normalize]
  have hm : (0 : ℝ) < (mu.mass : ℝ) := by
    exact_mod_cast hpos
  constructor <;> intro h <;> nlinarith

end

end NormalizedFiniteMeasureIntegral
end Probability
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Probability/NormalizedFiniteMeasureIntegral.lean:50published source at 0e31a3cda412