OAI/Analysis/BernoulliCone/UpperComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.threshold_lipschitz line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.threshold_support line 19
3. theorem OAI.Bernoulli.DeSilvaJerison.U_upper_comparison line 30

   Source documentation

   The actual upper foliation comparison, transferred through H1-zero trace closure to every admissible upper Sobolev competitor on every ball.

   theorem U_upper_comparison (c:Space 7) (r:ℝ) (hr:0<r)
       {v:Space 7→ℝ} {V:Space 7→Space 7}
       (hv:H1 (Metric.ball c r) v V)
       (hUv:∀ᵐ x ∂volume.restrict (Metric.ball c r),U x≤v x)
       (htrace:H10 (Metric.ball c r) (fun x=>v x-U x) (fun x=>V x-gradient U x)) :
       energy (Metric.ball c r) U (gradient U)≤energy (Metric.ball c r) v V := by
   …

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