OAI/Geometry/PrescribedPotential/RealSmoothOperator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real Smooth Operator.

  1. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.ext_value line 16
  2. lemma OAI.GlobalElliptic.Smooth.ofReal_part_re line 26
  3. lemma OAI.GlobalElliptic.Smooth.ofReal_part_im line 30
  4. lemma OAI.GlobalElliptic.laplacian_constant line 34
  5. lemma OAI.GlobalElliptic.complexL_ofReal line 43
  6. lemma OAI.GlobalElliptic.exists_real_smooth_poisson line 53