OAI/Analysis/CircleDomains/Sobolev/CirclePartitionEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative energy control for the actual smooth circle map. Local weak-gradient bounds survive positive mixing, while the selected smoothing errors contribute an arbitrarily small additive L² term.

  1. theorem OAI.CircleDomainRigidity.partition_field_energy line 16
  2. theorem OAI.CircleDomainRigidity.exists_positive_circle_smoothing_with_energy line 50