OAI/Analysis/CircleDomains/Modulus/CostPerturbation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Positive perturbations of the physical density and atomic tolls. Their norm increase is controlled by the finite physical area and the chosen square-summable countable weights.

  1. def OAI.CircleDomainRigidity.squareIntegralNorm line 18
  2. theorem OAI.CircleDomainRigidity.squareIntegralNorm_add_le line 21
  3. theorem OAI.CircleDomainRigidity.squareIntegralNorm_const line 28
  4. theorem OAI.CircleDomainRigidity.countingSquareNorm_mul line 38
  5. def OAI.CircleDomainRigidity.perturbedPhysicalDensity line 50
  6. def OAI.CircleDomainRigidity.perturbedAtomicToll line 53
  7. theorem OAI.CircleDomainRigidity.perturbedPhysicalDensity_norm line 56
  8. theorem OAI.CircleDomainRigidity.perturbedAtomicToll_norm line 70
  9. theorem OAI.CircleDomainRigidity.exists_small_positive_perturbation line 83
  10. theorem OAI.CircleDomainRigidity.perturbed_cost_ge_one line 111