OAI/Analysis/Littlewood/Cutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth cutoffs of nearly full squared mass, required by both the spreading and sampling constructions.

  1. lemma OAI.AsymptoticallyMinimalLittlewood.Cutoff.bump_mass line 13
  2. theorem OAI.AsymptoticallyMinimalLittlewood.Cutoff.unit_cutoff line 35