OAI/MeasureTheory/Falconer/Estimates/DescriptorTests.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual all-dimensional tests indexed by policy descriptors

The policy list is scalar. Its tests use original occupied cells and the full conditional probability of the current ambient-dimensional class. The tolerance is the manuscript's 500-sigma width at every level.

  1. def OAI.Falconer.descriptorValid line 23
  2. def OAI.Falconer.descriptorGoodDirections line 27
  3. theorem OAI.Falconer.descriptorGoodDirections_measurable line 38
  4. theorem OAI.Falconer.descriptor_projection_original_bound line 46
  5. theorem OAI.Falconer.uniform_descriptor_direction_buffer line 61
  6. theorem OAI.Falconer.policy_descriptor_valid line 91