Compactness and Shrinking of Exposed Sections

This formalizes the exposed-point section estimate used in the Caffarelli argument.

Let $E$ be finite-dimensional, let $u:E\to\mathbb R$ be convex, and let $x_0,p\in E$ satisfy

Assume the contact set $C=\{x:u(x)=u(x_0)+\langle p,x-x_0\rangle\}$ is compact. Let $x_e\in C$, let $\|\theta\|=1$, assume $x_e$ is exposed in direction $\theta$, and let $h>0$. For

there is a compact set $Q$ containing $S_\varepsilon$ for all sufficiently small positive $\varepsilon$. Moreover, for every $\delta>0$, sufficiently small positive $\varepsilon$ give

The declaration is exists_compact_sections_subset_and_shrink_readable.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_compact_sections_subset_and_shrink [FiniteDimensional ℝ E] {u : E → ℝ} (hconv : ConvexOn ℝ univ u)
    {x₀ p : E} (hp : ∀ y, u x₀ + ⟪p, y - x₀⟫ ≤ u y)
    (hC : IsCompact {x | u x = u x₀ + ⟪p, x - x₀⟫}) {xe θ : E}
    (hxe : u xe = u x₀ + ⟪p, xe - x₀⟫) (hθ : ‖θ‖ = 1)
    (hexp : ∀ x, u x = u x₀ + ⟪p, x - x₀⟫ → x ≠ xe → ⟪x - xe, θ⟫ < 0) {h : ℝ} (hh : 0 < h) :
    (∃ Q : Set E, IsCompact Q ∧ ∃ ε₀ > 0, ∀ ε, 0 < ε → ε < ε₀ →
      {x | u x - (u x₀ + ⟪p, x - x₀⟫) < ε * (⟪x - xe, θ⟫ + h)} ⊆ Q) ∧
    ∀ δ > 0, ∃ ε₁ > 0, ∀ ε, 0 < ε → ε < ε₁ →
      {x | u x - (u x₀ + ⟪p, x - x₀⟫) < ε * (⟪x - xe, θ⟫ + h)} ⊆
        cthickening δ ({x | u x = u x₀ + ⟪p, x - x₀⟫} ∩ {x | -h ≤ ⟪x - xe, θ⟫})

Module navigation

Module: Analysis/Convex/Caffarelli.

Previous: infDist_frontier_image_le_of_width · Next: contact_stepA.

Source excerpt, lines 181–190 · Frozen source 408915f.