OAI/MeasureTheory/Falconer/Slicing/GaussianActiveRelation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Original-pair incidence after the active-cover deletion

  1. def OAI.Falconer.gaussianActiveRelation line 13
  2. theorem OAI.Falconer.gaussianActiveRelation_measurable line 21
  3. theorem OAI.Falconer.gaussian_active_bad_integral line 32
  4. theorem OAI.Falconer.gaussian_active_pruning_loss line 62