OAI/Analysis/LipschitzHilbert/Trees/SourceMaskedPhysicalTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial thresholds for the actual masked mixed reference family. Shortness and the narrow cone supply the mask hypotheses for every sufficiently large L; no separate mask spectrum is assumed.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.masked_mixed_reference_polynomial_tails line 15