OAI/MeasureTheory/Falconer/Slicing/GaussianFullRank.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A square Gaussian matrix is nonsingular almost surely

Each zero Gram--Schmidt residual lies in a Gaussian-null fixed hyperplane when the other rows are fixed. No polynomial zero-set theorem is assumed.

  1. theorem OAI.Falconer.gaussian_residual_zero_mass line 17
  2. theorem OAI.Falconer.gaussian_square_det_ne_zero_ae line 43