OAI/Analysis/CircleDomains/Topology/CompactPositiveFunctional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The compact-space representation step for the measure-modulus dual: a positive linear functional taking the constant one to one is a genuine probability law. This is the existing Riesz representation theorem.

  1. lemma OAI.CircleDomainRigidity.exists_probability_of_compact_positive_functional line 14
  2. lemma OAI.CircleDomainRigidity.exists_probability_of_compact_positive_functional_trim line 31