OAI/Analysis/CircleDomains/Topology/DisjointCutoffAverages.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Averaging cutoffs with disjoint transition sets divides their common Dirichlet energy by the number of cutoffs.

  1. theorem OAI.CircleDomainRigidity.norm_sq_sum_disjoint line 12
  2. def OAI.CircleDomainRigidity.cutoffAverage line 29
  3. theorem OAI.CircleDomainRigidity.cutoffAverage_smooth line 32
  4. theorem OAI.CircleDomainRigidity.cutoffAverage_fderiv line 36
  5. theorem OAI.CircleDomainRigidity.cutoffAverage_compact line 41
  6. theorem OAI.CircleDomainRigidity.cutoffAverage_mem_unit line 50
  7. theorem OAI.CircleDomainRigidity.cutoffAverage_one line 62
  8. theorem OAI.CircleDomainRigidity.cutoffAverage_energy line 68