OAI/Analysis/CircleDomains/Sobolev/BarrierEnergyAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Turn the proved reference-comparison bound into the total source barrier energy. The reference is constructed by conformal transport.

  1. theorem OAI.CircleDomainRigidity.l2_norm_le_error_add line 13
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.barrier_energy_from_reference line 39