OAI/Geometry/TamingCompatibility/Hodge/DyadicCorrectionProgress.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.RadialPotential.sum_halves line 10
2. lemma OAI.TamingCompatibility.RadialPotential.sum_halves_le_two line 18
3. lemma OAI.TamingCompatibility.RadialPotential.dyadic_norm_sum_inverse_bound line 26
4. lemma OAI.TamingCompatibility.RadialPotential.dyadic_count_bound line 38
5. lemma OAI.TamingCompatibility.RadialPotential.dyadic_norm_sum_log_bound line 51