OAI/Probability/GaussianInformation/Dyadic/RefinementCost.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.finite_entropy_le_subprob_reference line 18
2. lemma OAI.RepeatedLocalization.weighted_log_max_ratio_le line 31
3. lemma OAI.RepeatedLocalization.finite_log_concentration_le line 52
4. def OAI.RepeatedLocalization.depthGeometric line 61
5. lemma OAI.RepeatedLocalization.depthGeometric_pos line 62
6. lemma OAI.RepeatedLocalization.depthGeometric_le_one line 63
7. lemma OAI.RepeatedLocalization.log_depthGeometric line 64
8. lemma OAI.RepeatedLocalization.depthGeometric_sum_le_one line 69
9. lemma OAI.RepeatedLocalization.entropy_and_concentration_depth line 79
10. structure OAI.RepeatedLocalization.HeavyRefinement line 103
11. lemma OAI.RepeatedLocalization.exists_heavy_refinement line 127