OAI/Analysis/BernoulliCone/HalfspaceGroundstate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Halfspace.radial_potential_test line 13
2. lemma OAI.Bernoulli.Halfspace.radial_outer_integrable line 19
3. theorem OAI.Bernoulli.Halfspace.gradient_parallel_of_halfspace_support line 32

   Source documentation

   Ground-state equality for a true homogeneous minimizing cone supported in one closed halfspace. This uses a Lipschitz perspective competitor, not a regularity assumption or a boundary trace quotient.

   theorem gradient_parallel_of_halfspace_support {u : Space d → ℝ} {L : ℝ≥0}
       (hm : GlobalMinimizer u) (hL : LipschitzWith L u)
       (hom : ∀r:ℝ, 0<r → ∀x, u (r•x)=r*u x)
       {e : Space d} (he : ‖e‖=1) (hz : ∀x, inner ℝ x e ≤ 0 → u x=0) :
       ∀ᵐ x ∂volume.restrict (ball (0:Space d) 1),
         gradient u x=(u x/inner ℝ x e) • e := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.GlobalMinimizer