OAI/Analysis/VlasovMaxwell/Population/SourceJointFlux.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.Magnetic.sourceJointFlux line 12
2. lemma OAI.RVM.Magnetic.sourceJointFlux_contDiffAt line 15
3. lemma OAI.RVM.Magnetic.sourceJointFlux_derivative_bound line 30
4. lemma OAI.RVM.Magnetic.sourceFixedFlux_spatial_derivative line 49
5. lemma OAI.RVM.Magnetic.sourceFixedFlux_field_derivative line 57
6. lemma OAI.RVM.Magnetic.sourceFixedFlux_field_differentiable line 64
7. lemma OAI.RVM.Magnetic.sourceFixedFlux_field_rescale line 69
8. lemma OAI.RVM.Magnetic.sourceFixedFlux_bounds line 81
9. lemma OAI.RVM.Magnetic.divergence_parameter_chain line 121