OAI/Analysis/LipschitzHilbert/Trees/SourceMaskedReference.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The reference square and cubic-variation moments for actual masked synthesis. The original analyzing budget is retained; the synthesis constant doubles and the annulus is relaxed by half its lower endpoint.

  1. theorem OAI.LipschitzHilbert.LinePacketFamily.sinc_masked_uniform_moments line 15