OAI/Analysis/CircleDomains/Sobolev/ModelUniformRowEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform image bounds give a uniform energy budget for the reference rows on the actual source working disk.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.horizontalSection_fderiv_norm_sq line 15
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.working_row_energy_le line 25