OAI/Analysis/Conductivity/Variational/QuantitativePhysicalMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.CompactSmoothPair.smul line 14
2. lemma OAI.ScalarConductivity.PairSupported.smul line 20
3. lemma OAI.ScalarConductivity.physicalSourceMoment_smul line 26
4. theorem OAI.ScalarConductivity.bounded_physical_moments_in_open line 38
5. lemma OAI.ScalarConductivity.integral_bound_on_compact line 79
6. theorem OAI.ScalarConductivity.physical_source_moment_bound line 89