OAI/Analysis/CircleDomains/Probability/MeasureFamilySubadditivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The square root of pointwise 2-modulus is subadditive. This is the quantitative form needed when discarding measures outside a compact set.

  1. lemma OAI.CircleDomainRigidity.measureFamilyModulus_sqrt_eq_iInf line 13
  2. lemma OAI.CircleDomainRigidity.measureFamilyModulus_sqrt_subadditive line 24