OAI/MeasureTheory/Falconer/Estimates/PolicyPrefixLowpass.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The positive prefix lowpass inequality with the actual old masks
- theorem
OAI.Falconer.uniform_policy_prefix_lowpassline 12