OAI/Analysis/StrictMeans/UniformMeans.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.dyadic_norm_power_bound line 18
2. lemma OAI.StrictInverseFirstPower.dyadicScale_for_radius line 48
3. lemma OAI.StrictInverseFirstPower.dyadicHeight_neg_rpow_le line 58
4. lemma OAI.StrictInverseFirstPower.family_uniform_mean_bound line 67
5. def OAI.StrictInverseFirstPower.normalizedDiskMap line 84
6. lemma OAI.StrictInverseFirstPower.normalizedDiskMap_extension line 87
7. lemma OAI.StrictInverseFirstPower.normalizedDiskMap_deriv line 92
8. def OAI.StrictInverseFirstPower.normalizedDiskFamily line 98
9. lemma OAI.StrictInverseFirstPower.integralMean_neg_one_as_family line 107
10. theorem OAI.StrictInverseFirstPower.uniform_integralMean_bound_above_dyadicExponent line 120