AutoSamplingTheory.TechnicalLemmas.Probability.UniformExpectationGap

- If `f` dominates `g` by one uniform positive margin almost everywhere, then the expectation of `f` is strictly larger than that of `g`.

theorem integral_lt_integral_of_ae_add_le
    {f g : Ω → ℝ} {ε : ℝ}
    (hf : Integrable f μ) (hg : Integrable g μ)
    (hε : 0 < ε)
    (hgap : ∀ᵐ x ∂μ, g x + ε ≤ f x) :
    (∫ x, g x ∂μ) < ∫ x, f x ∂μ := by
  have hconst : Integrable (fun _ : Ω => ε) μ := by fun_prop
  have hsum : Integrable (fun x => g x + ε) μ := hg.add hconst
  have hle := integral_mono_ae hsum hf hgap
  have hsumIntegral :
      (∫ x, g x + ε ∂μ) = (∫ x, g x ∂μ) + ε := by
    rw [integral_add hg hconst]
    simp
  rw [hsumIntegral] at hle
  linarith

/-- Difference form, convenient when a pointwise cost identity is already
available. -/

AutoSamplingTheory/TechnicalLemmas/Probability/UniformExpectationGap.lean:28published source at 0e31a3cda412

- Difference form, convenient when a pointwise cost identity is already available.

theorem integral_lt_integral_of_ae_gap
    {f g : Ω → ℝ} {ε : ℝ}
    (hf : Integrable f μ) (hg : Integrable g μ)
    (hε : 0 < ε)
    (hgap : ∀ᵐ x ∂μ, ε ≤ f x - g x) :
    (∫ x, g x ∂μ) < ∫ x, f x ∂μ := by
  apply integral_lt_integral_of_ae_add_le hf hg hε
  filter_upwards [hgap] with x hx
  linarith

end

end UniformExpectationGap
end Probability
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Probability/UniformExpectationGap.lean:46published source at 0e31a3cda412