OAI/Analysis/VlasovMaxwell/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Global classical solvability and uniqueness for smooth admissible data.

  1. lemma OAI.RVM.Admissible.uniform_physical_population_increment line 31
  2. theorem OAI.RVM.global_classical_solution line 44

    Distinct definitions of this name: ComparatorChallenges/VlasovMaxwell.lean:103 (same statement text; different proof or body). Qualify references as OAI.RVM.global_classical_solution@path.