OAI/Analysis/CircleDomains/Sobolev/FilledScalarGlobalEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite holes contribute no ordinary gradient energy. Their circular boundaries are null, including degenerate point circles.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_fderiv_on_ball line 21
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_energy_eq_indicator_ae line 28
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.filled_energy_integrable_iff line 51
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.HoleFilling.integral_filled_energy line 59
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.eventually_filled_global_energy line 68