OAI/Analysis/VlasovMaxwell/Retarded/DirectDeficitUniform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.log_four_le_linear line 13
2. lemma OAI.RVM.Admissible.direct_remaining_source_deficit_short_uniform line 26