OAI/Analysis/LipschitzHilbert/Trees/SourceMaskIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source-normalized mask error. The weak count is derived from the actual popular witnesses, and the area relation removes its square root factors. The mask scale is fixed before all finite families.

  1. theorem OAI.LipschitzHilbert.source_mask_integral line 15