OAI/Analysis/CircleDomains/Sobolev/ScalarFlatteningEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The flattening construction retains a genuine Sobolev witness. Its squared gradient error is exactly the energy above the removed values.

  1. theorem OAI.CircleDomainRigidity.flattenValues_zero line 12
  2. theorem OAI.CircleDomainRigidity.flattenValues_norm_le line 15
  3. theorem OAI.CircleDomainRigidity.flattenValues_monotone line 20
  4. theorem OAI.CircleDomainRigidity.flattenValues_unit_interval line 28
  5. def OAI.CircleDomainRigidity.flattenedGradient line 35
  6. def OAI.CircleDomainRigidity.flattenedSobolevWitness line 39
  7. theorem OAI.CircleDomainRigidity.flattenValues_compact_support line 64
  8. theorem OAI.CircleDomainRigidity.flattenedGradient_energy_error line 68