OAI/MeasureTheory/Falconer/Radial/ProjectedHyperplaneNull.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Independent sampled tuples exclude mass on projected hyperplanes

  1. theorem OAI.Falconer.orthogonal_independent_square_eq_zero line 11
  2. theorem OAI.Falconer.projected_hyperplane_null_of_tuples line 21
  3. theorem OAI.Falconer.gaussian_projected_hyperplanes_null_ae line 44