OAI/Analysis/CircleDomains/Sobolev/SobolevTypicalLinePayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A continuous compact Sobolev function admits an actual L² payment for all intervals on almost every coordinate line. Strong mollification and a summably convergent subsequence supply the payment.

  1. theorem OAI.CircleDomainRigidity.smooth_line_increment_payment_ae line 16
  2. theorem OAI.CircleDomainRigidity.sobolev_typical_line_payment line 31