OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/ConditionalHardness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuum Coulomb hardness under explicit analytic hypotheses, for the full spinful weak-H1 infimum and the encoded unit- and binary-charge promises.

  1. theorem OAI.ContinuumCoulomb.conditional_unit_coulomb_qmaHard line 13
  2. theorem OAI.ContinuumCoulomb.conditional_binary_coulomb_qmaHard line 22