OAI/Analysis/CircleDomains/Probability/CompactMeasureMajorantCost.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual least L² cost of a bounded continuous majorant on a compact family of finite measures. Feasibility follows from its positive minimum mass; sublinearity follows from the triangle inequality in L².

  1. def OAI.CircleDomainRigidity.majorantNorms line 20
  2. def OAI.CircleDomainRigidity.compactMeasureMajorantCost line 24
  3. lemma OAI.CircleDomainRigidity.majorantNorms_bddBelow line 26
  4. lemma OAI.CircleDomainRigidity.majorantNorms_nonempty line 31
  5. lemma OAI.CircleDomainRigidity.compactMeasureMajorantCost_nonneg line 37
  6. lemma OAI.CircleDomainRigidity.le_compactMeasureMajorantCost line 43
  7. lemma OAI.CircleDomainRigidity.compactMeasureMajorantCost_le line 53
  8. lemma OAI.CircleDomainRigidity.compactMeasureMajorantCost_nonpos line 58
  9. lemma OAI.CircleDomainRigidity.compactMeasureMajorantCost_smul_le line 66
  10. lemma OAI.CircleDomainRigidity.compactMeasureMajorantCost_smul line 81
  11. lemma OAI.CircleDomainRigidity.compactMeasureMajorantCost_add line 91