OAI/Analysis/BernoulliCone/ConePicone.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Halfspace.positiveSquareRatio_hasFDerivAt line 13
2. lemma OAI.Bernoulli.Halfspace.positiveSquareRatio_gradient line 29
3. lemma OAI.Bernoulli.Halfspace.weighted_positiveSquareRatio_gradient line 38
4. theorem OAI.Bernoulli.Halfspace.picone_gradient_equality line 55

   Source documentation

   Picone ground-state equality from full minimizing comparison. It is a consequence, not a stationarity or regularity assumption in GlobalMinimizer.

   theorem picone_gradient_equality {u v : Space d → ℝ} {L M C : ℝ≥0}
       (hm : GlobalMinimizer u) (hL : LipschitzWith L u) (hM : LipschitzWith M v)
       (hom : ∀r:ℝ, 0<r → ∀x, u (r•x)=r*u x)
       (hC : 1≤C) (hbound : ∀x, |v x| ≤ (C:ℝ)*u x)
       (hvI : (∫ x in ball (0:Space d) 2, potential x*‖gradient v x‖^2-rawKernel x*v x^2)=0) :
       ∀ᵐ x ∂volume.restrict (ball (0:Space d) 1),
         gradient v x=(v x/u x) • gradient u x := by
   …

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