AutoSamplingTheory.TechnicalLemmas.Measure.PositiveComponentAE

- A measure is absolutely continuous with respect to any mixture containing it with nonzero `ENNReal` weight.

theorem absolutelyContinuous_smul_add_left
    {α : Type*} [MeasurableSpace α]
    {μ ν : Measure α} {c : ℝ≥0∞} (hc : c ≠ 0) :
    μ ≪ c • μ + ν := by
  intro s hs
  have hparts : c * μ s = 0 ∧ ν s = 0 := by
    simpa [Measure.smul_apply] using hs
  exact (mul_eq_zero.mp hparts.1).resolve_left hc

/-- Symmetric version for the right component. -/

AutoSamplingTheory/TechnicalLemmas/Measure/PositiveComponentAE.lean:25published source at 0e31a3cda412

- Symmetric version for the right component.

theorem absolutelyContinuous_add_smul_right
    {α : Type*} [MeasurableSpace α]
    {μ ν : Measure α} {c : ℝ≥0∞} (hc : c ≠ 0) :
    ν ≪ μ + c • ν := by
  simpa [add_comm] using
    (absolutelyContinuous_smul_add_left (μ := ν) (ν := μ) hc)

/-- Any property holding almost everywhere under a positive mixture also holds
almost everywhere under its left component. -/

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

- Any property holding almost everywhere under a positive mixture also holds almost everywhere under its left component.

theorem ae_of_ae_smul_add_left
    {α : Type*} [MeasurableSpace α]
    {μ ν : Measure α} {c : ℝ≥0∞} (hc : c ≠ 0)
    {P : α → Prop}
    (hP : ∀ᵐ x ∂(c • μ + ν), P x) :
    ∀ᵐ x ∂μ, P x :=
  (absolutelyContinuous_smul_add_left (μ := μ) (ν := ν) hc).ae_le hP

/-- Any property holding almost everywhere under a positive mixture also holds
almost everywhere under its right component. -/

AutoSamplingTheory/TechnicalLemmas/Measure/PositiveComponentAE.lean:44published source at 0e31a3cda412

- Any property holding almost everywhere under a positive mixture also holds almost everywhere under its right component.

theorem ae_of_ae_add_smul_right
    {α : Type*} [MeasurableSpace α]
    {μ ν : Measure α} {c : ℝ≥0∞} (hc : c ≠ 0)
    {P : α → Prop}
    (hP : ∀ᵐ x ∂(μ + c • ν), P x) :
    ∀ᵐ x ∂ν, P x :=
  (absolutelyContinuous_add_smul_right (μ := μ) (ν := ν) hc).ae_le hP

end

end PositiveComponentAE
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/PositiveComponentAE.lean:54published source at 0e31a3cda412