OAI/NumberTheory/JointDickman/Counting/SamplingFamilyRate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The column-family entropy is absorbed by concentration

  1. theorem OAI.JointDickman.samplingFamily_scale_bound line 11
  2. theorem OAI.JointDickman.samplingFamily_envelope_tendsto line 45
  3. theorem OAI.JointDickman.sampling_sites_le_scale line 53
  4. theorem OAI.JointDickman.sampling_sample_size line 68