OAI/Geometry/PrescribedPotential/BallSubmean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Ball Submean.

  1. lemma OAI.PotentialABP.hessian_affine_comp line 22
  2. def OAI.PotentialABP.unitScalarIso line 42
  3. lemma OAI.PotentialABP.ball_integral_unit_smul line 47
  4. lemma OAI.PotentialABP.ball_integral_translate line 57
  5. lemma OAI.PotentialABP.complexLine_hessian line 68
  6. theorem OAI.PotentialABP.smooth_ball_submean line 77