OAI/Analysis/NodalLength/Vitali.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.vitali_measure_bound line 277
2. lemma OAI.SharpNodal.Profiles.inverse_norm_integrableOn_ball line 310
3. lemma OAI.SharpNodal.Profiles.integral_inverse_norm_ball line 318
4. lemma OAI.SharpNodal.Profiles.inverse_translate_integrable_bound line 326
5. lemma OAI.SharpNodal.Profiles.complex_difference_norm line 351
6. def OAI.SharpNodal.Profiles.weightMeasure line 364
7. lemma OAI.SharpNodal.Profiles.weightMeasure_unit_bound line 367
8. lemma OAI.SharpNodal.Profiles.weightMeasure_local_lower line 388
9. lemma OAI.SharpNodal.Profiles.nodal_length_of_weight line 427
10. lemma OAI.SharpNodal.Profiles.nodal_length_holomorphic_comparison line 487