OAI/Analysis/KLS/Spectral/BrascampLiebPerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.KLS.blPerturbation line 17
  2. theorem OAI.LeanBlast.KLS.contDiff_blPerturbation line 21
  3. theorem OAI.LeanBlast.KLS.fderiv_blPerturbation_apply line 26
  4. theorem OAI.LeanBlast.KLS.second_fderiv_blPerturbation_apply line 46
  5. theorem OAI.LeanBlast.KLS.second_fderiv_blPerturbation_zero_pos line 85
  6. theorem OAI.LeanBlast.KLS.exists_blPerturbation_convex line 109