OAI/Analysis/BernoulliCone/UpperLipschitzComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.DeSilvaJerison.energyDifference line 12
2. lemma OAI.Bernoulli.DeSilvaJerison.comparisonR_upper_limit line 16
3. theorem OAI.Bernoulli.DeSilvaJerison.U_upper_lipschitz_comparison line 65

   Source documentation

   Actual one-sided global energy comparison for every Lipschitz compact upper perturbation. All flux/slopes have been constructed explicitly.

   theorem U_upper_lipschitz_comparison {v:Space 7→ℝ} {L:ℝ≥0}
       (hv:LipschitzWith L v) (hUv:∀x,U x≤v x)
       (hc:HasCompactSupport (fun y=>v y-U y))
       {c:Space 7} {r:ℝ} (hS:tsupport (fun y=>v y-U y)⊆Metric.ball c r) :
       energy (Metric.ball c r) U (gradient U)≤energy (Metric.ball c r) v (gradient v) := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.energy