AutoSamplingTheory.TechnicalLemmas.Measure.CouplingConvexDomainAE

- If a coupling is almost everywhere concentrated over a convex source domain, and its first marginal is absolutely continuous with respect to Haar measure, then the first coordinate lies in the domain interior and a real convex function on that domain is Frechet differentiable there, jointly `gamma`-almost everywhere.

theorem ae_fst_mem_interior_and_differentiableAt
    {s : Set E} {phi : E → ℝ}
    (hgamma : IsCoupling gamma μ ν)
    (hs : Convex ℝ s)
    (hconv : ConvexOn ℝ s phi)
    (hμm : μ ≪ m)
    (hmem : ∀ᵐ z ∂gamma, z.1 ∈ s) :
    ∀ᵐ z ∂gamma,
      z.1 ∈ interior s ∧ DifferentiableAt ℝ phi z.1 := 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_μ
  have hnotfront_gamma : ∀ᵐ z ∂gamma, z.1 ∉ frontier s :=
    ae_fst_of_isCoupling hgamma hnotfront_μ

  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 hdiff_gamma : ∀ᵐ z ∂gamma,
      z.1 ∈ interior s → DifferentiableAt ℝ phi z.1 :=
    ae_fst_of_isCoupling hgamma hdiff_μ

  filter_upwards [hmem, hnotfront_gamma, hdiff_gamma] with z hzs hzfront hdiff
  have hzclosure : z.1 ∈ closure s := subset_closure hzs
  have hzinterior : z.1 ∈ interior s := by
    by_contra hznot
    apply hzfront
    simp [frontier, hzclosure, hznot]
  exact ⟨hzinterior, hdiff hzinterior⟩

end

end CouplingConvexDomainAE
end Measure
end TechnicalLemmas
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Measure/CouplingConvexDomainAE.lean:42published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.