AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexOpenAEDifferentiable

- A finite-valued convex function on an open convex domain of a finite-dimensional real normed space is Frechet differentiable almost everywhere at points of that domain.

theorem ae_differentiableAt_of_convexOn_isOpen
    {phi : E → ℝ} {s : Set E}
    (hs : IsOpen s) (hconv : ConvexOn ℝ s phi) :
    ∀ᵐ x ∂m, x ∈ s → DifferentiableAt ℝ phi x := by
  letI : LocallyCompactSpace s := hs.isLocallyClosed.locallyCompactSpace
  letI : SigmaCompactSpace s := inferInstance

  let K : ℕ → Set E := fun n =>
    Subtype.val '' SigmaCompactSpace.compactCovering s n
  have hKcompact : ∀ n, IsCompact (K n) := by
    intro n
    exact (SigmaCompactSpace.isCompact_compactCovering s n).image continuous_subtype_val
  have hKsub : ∀ n, K n ⊆ s := by
    intro n x hx
    rcases hx with ⟨y, _hy, rfl⟩
    exact y.property

  choose L hLcompact hKinterior hLsub using fun n =>
    exists_compact_between (hKcompact n) hs (hKsub n)

  have hcover : s ⊆ ⋃ n, interior (L n) := by
    intro x hx
    rcases SigmaCompactSpace.exists_mem_compactCovering (⟨x, hx⟩ : s) with ⟨n, hn⟩
    have hxK : x ∈ K n := by
      exact ⟨⟨x, hx⟩, hn, rfl⟩
    exact Set.mem_iUnion.2 ⟨n, hKinterior n hxK⟩

  have hlocal : LocallyLipschitzOn s phi :=
    hconv.locallyLipschitzOn hs
  have hcompactLip : ∀ n, ∃ C : ℝ≥0, LipschitzOnWith C phi (L n) := by
    intro n
    exact (hlocal.mono (hLsub n)).exists_lipschitzOnWith_of_compact (hLcompact n)
  choose C hLip using hcompactLip

  have hAe : ∀ n : ℕ, ∀ᵐ x ∂m,
      x ∈ interior (L n) → DifferentiableAt ℝ phi x := by
    intro n
    have hLipInterior : LipschitzOnWith (C n) phi (interior (L n)) :=
      (hLip n).mono interior_subset
    filter_upwards [hLipInterior.ae_differentiableWithinAt_of_mem] with x hx
    intro hxInt
    rcases hx hxInt with ⟨A, hA⟩
    exact ⟨A, (hasFDerivWithinAt_of_isOpen isOpen_interior hxInt).mp hA⟩
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexOpenAEDifferentiable.lean:40published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.