OAI/Analysis/CircleDomains/Sobolev/L2AdditiveMajorant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A scalar L2 majorant bounds the differential error of the actual priority interpolation.

  1. theorem OAI.CircleDomainRigidity.l2_norm_le_of_additive_majorant line 12