OAI/Analysis/LipschitzHilbert/Estimates/MaskNormalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalize the weak-L2 mask error by the source relation between total top area and the two testing measures.

  1. theorem OAI.LipschitzHilbert.sqrt_area_product line 11
  2. theorem OAI.LipschitzHilbert.mask_error_normalization line 29