OAI/MeasureTheory/Falconer/Slicing/GaussianBadTripleMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Expected mass of nearly dependent retained original triples

  1. theorem OAI.Falconer.gaussian_bad_triple_mass line 12