OAI/Analysis/BernoulliCone/SobolevIdeals.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Bernoulli.SobolevCalculus.cutPrimitive_eq_zero_of_nonpos line 11
  2. def OAI.Bernoulli.SobolevCalculus.innerCut line 23
  3. def OAI.Bernoulli.SobolevCalculus.innerSlope line 24
  4. lemma OAI.Bernoulli.SobolevCalculus.innerCut_zero line 26
  5. lemma OAI.Bernoulli.SobolevCalculus.innerCut_deriv line 30
  6. lemma OAI.Bernoulli.SobolevCalculus.innerCut_contDiff line 34
  7. lemma OAI.Bernoulli.SobolevCalculus.innerCut_lipschitz line 36
  8. lemma OAI.Bernoulli.SobolevCalculus.innerSlope_continuous line 40
  9. lemma OAI.Bernoulli.SobolevCalculus.innerSlope_norm_le line 42
  10. lemma OAI.Bernoulli.SobolevCalculus.innerCut_vanish line 43
  11. lemma OAI.Bernoulli.SobolevCalculus.innerCut_tendsto line 46
  12. lemma OAI.Bernoulli.SobolevCalculus.innerSlope_tendsto line 56
  13. lemma OAI.Bernoulli.SobolevCalculus.h10_innerCut line 79
  14. theorem OAI.Bernoulli.SobolevCalculus.h10_positive_domain line 86
  15. theorem OAI.Bernoulli.SobolevCalculus.h10_positive_domain_inter line 153