OAI/Analysis/CircleDomains/Probability/MeasureFamilyModulusBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pointwise measure-family modulus: monotonicity, indexing invariance, and the zero-modulus family of measures charging a fixed reference-null set. Extended-valued admissible densities are retained throughout.

  1. lemma OAI.CircleDomainRigidity.measureFamilyModulus_le_admissible line 16
  2. lemma OAI.CircleDomainRigidity.exists_admissible_of_modulus_lt line 22
  3. lemma OAI.CircleDomainRigidity.measureFamilyModulus_zero_iff line 28
  4. lemma OAI.CircleDomainRigidity.measureFamilyModulus_mono_range line 40
  5. lemma OAI.CircleDomainRigidity.measureFamilyModulus_eq_of_range_eq line 54
  6. lemma OAI.CircleDomainRigidity.measureFamilyModulus_mono_reference line 60
  7. lemma OAI.CircleDomainRigidity.measureFamilyModulus_zero_of_charges_null_set line 72