AutoSamplingTheory.TechnicalLemmas.Measure.ConvexInteriorAE

- If `μ` is absolutely continuous with respect to additive Haar measure and is almost everywhere supported on a convex set `s`, then `μ` is actually almost everywhere supported on `interior s`. The only removed points lie on the convex frontier, which is Haar-null.

theorem ae_mem_interior_of_convex_of_absolutelyContinuous
    {s : Set E}
    (hs : Convex ℝ s)
    (hμm : μ ≪ m)
    (hmem : ∀ᵐ x ∂μ, x ∈ s) :
    ∀ᵐ x ∂μ, x ∈ interior s := by
  have hfront_m : m (frontier s) = 0 :=
    hs.addHaar_frontier m
  have hfront_μ : μ (frontier s) = 0 :=
    hμm hfront_m
  have hnotfront : ∀ᵐ x ∂μ, x ∉ frontier s :=
    measure_eq_zero_iff_ae_notMem.mp hfront_μ
  filter_upwards [hmem, hnotfront] with x hxs hxfront
  have hxclosure : x ∈ closure s := subset_closure hxs
  by_contra hxinterior
  apply hxfront
  simp [frontier, hxclosure, hxinterior]

end ConvexInteriorAE
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/ConvexInteriorAE.lean:32published source at 0e31a3cda412