AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexDomainACAEDifferentiable

- A real-valued convex function is `μ`-a.e. Frechet differentiable whenever `μ` is absolutely continuous with respect to additive Haar measure and is almost everywhere concentrated on the convex domain on which convexity is known.

theorem ae_differentiableAt_of_convexOn_of_absolutelyContinuous
    {phi : E → ℝ} {s : Set E}
    (hs : Convex ℝ s)
    (hconv : ConvexOn ℝ s phi)
    (hμm : Measure.AbsolutelyContinuous μ m)
    (hmem : ∀ᵐ x ∂μ, x ∈ s) :
    ∀ᵐ x ∂μ, DifferentiableAt ℝ phi x := by
  have hsInterior : Convex ℝ (interior s) := hs.interior
  have hconvInterior : ConvexOn ℝ (interior s) phi :=
    hconv.subset interior_subset hsInterior
  have hdiff_m : ∀ᵐ x ∂m,
      x ∈ interior s → DifferentiableAt ℝ phi x :=
    ae_differentiableAt_of_convexOn_isOpen isOpen_interior hconvInterior
  have hdiff_μ : ∀ᵐ x ∂μ,
      x ∈ interior s → DifferentiableAt ℝ phi x :=
    hμm.ae_le hdiff_m
  have hinterior_μ : ∀ᵐ x ∂μ, x ∈ interior s :=
    ae_mem_interior_of_convex_of_absolutelyContinuous hs hμm hmem
  filter_upwards [hinterior_μ, hdiff_μ] with x hx hdiff
  exact hdiff hx

end

end ConvexDomainACAEDifferentiable
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexDomainACAEDifferentiable.lean:35published source at 0e31a3cda412