Research proof index

Jensen's inequality for eLpNorm: the L^p norm of a constant equal to the average is at most the L^p norm of the function. For 1 ≤ p < ⊤, an integrable f, and a finite measure μ: eLpNorm (fun _ => ⨍ x, f x ∂μ) p μ ≤ eLpNorm f p μ This is a consequence of Jensen's inequality for the convex function t ↦ |t|^p, proved here via Hölder's ine...

An a.e. upper bound on the half ball upgrades to an essential-supremum bound on the half ball.

A compact inner ball can be covered by finitely many smaller balls whose dilated closed balls still lie inside the ambient ball.

A quantitative version of exists_finite_inner_ball_cover with a coarse explicit cardinality bound depending only on r / ρ and d.

Global smooth compactly supported approximation for a local witness whose support is already compactly contained in the source open set.

A specialized quantitative cover tailored to the half-ball / eighth-ball geometry used in the crossover argument.