OAI/Analysis/CircleDomains/Sobolev/BoundedContinuousL2Dual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The L² representation of a functional on bounded continuous tests. Only the bound through their actual L² image is required.

  1. lemma OAI.CircleDomainRigidity.exists_L2_pairing_of_boundedContinuous_bound line 18