OAI/Analysis/CircleDomains/Sobolev/PartitionPlateaus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact constant values under the constructed positive smoothing.

  1. theorem OAI.CircleDomainRigidity.partition_samples_within_plateau line 13
  2. theorem OAI.CircleDomainRigidity.interval_smoothing_eq_on_plateau line 24