Affine Image Frontier Bound from Widths

This formalizes the affine-normalized frontier-distance estimate used in the Caffarelli argument.

Let $E$ be finite-dimensional, let $S\subseteq E$ be open and bounded, let $x\in S$, and let $\theta$ be a unit vector. Suppose $\alpha\ge0$, $\beta>0$, and

while some $y\in S$ satisfies $\langle y-x,\theta\rangle\le-\beta$. If $e:E\simeq_A E$ is an affine equivalence with $e(S)\subseteq\overline B(0,C_0)$ for $C_0>0$, then

The declaration is infDist_frontier_image_le_of_width_readable. The inequalities are respectively non-strict above and strict in the positivity hypothesis for $\beta$ and $C_0$.

Original Lean declaration header

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

theorem infDist_frontier_image_le_of_width {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} (hS : IsOpen S)
    (hb : Bornology.IsBounded S) {x : E} (hx : x ∈ S) {θ : E} (hθ : ‖θ‖ = 1) {α β : ℝ}
    (hα : 0 ≤ α) (hβ : 0 < β) (hup : ∀ y ∈ S, ⟪y - x, θ⟫ ≤ α) (hlow : ∃ y ∈ S, ⟪y - x, θ⟫ ≤ -β)
    (e : E ≃ᵃ[ℝ] E) {C₀ : ℝ} (hC₀ : 0 < C₀) (himg : e '' S ⊆ closedBall (0 : E) C₀) :
    infDist (e x) (frontier (e '' S)) ≤ 2 * C₀ * α / β

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: infDist_frontier_le_of_forall_inner_le.

Next: exists_compact_sections_subset_and_shrink.

Source excerpt, lines 29–34 · Frozen source 408915f.