OAI/Analysis/CircleDomains/Probability/MeasureFamilyNullRemoval.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing a pointwise zero-modulus family does not alter modulus. Minkowski's inequality controls the arbitrarily cheap admissible repair.

  1. lemma OAI.CircleDomainRigidity.measureFamilyModulus_le_admissible_off_null_family line 13
  2. lemma OAI.CircleDomainRigidity.measureFamilyModulus_remove_null_family line 48