OAI/Analysis/BernoulliCone/GlobalMinimizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Bernoulli.DeSilvaJerison.U_global_minimizer line 14

   Source documentation

   The constructed double-cone is a global energy minimizer against the full arbitrary Sobolev competitor class. Upper and lower comparisons are joined by the exact Sobolev lattice identity, including its contact-level gradients.

   theorem U_global_minimizer : GlobalMinimizer U := by
   …

   Mentions: OAI.Bernoulli.GlobalMinimizer, OAI.Bernoulli.DeSilvaJerison.U

2. theorem OAI.Bernoulli.DeSilvaJerison.exists_nonflat_dimension_seven line 76