OAI/Analysis/Conductivity/Variational/PhysicalTraceBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.sourcePhysicalEnergy_jet_le line 13
2. def OAI.ScalarConductivity.physicalRestrictedJetCLM line 28
3. lemma OAI.ScalarConductivity.physicalRestrictedJet_smooth_ae line 32
4. lemma OAI.ScalarConductivity.physical_smooth_energy_bound line 41
5. theorem OAI.ScalarConductivity.dense_linear_observable_extension line 73
6. def OAI.ScalarConductivity.physicalOuterBoundary line 117
7. lemma OAI.ScalarConductivity.physicalOuterBoundary_continuous line 121
8. lemma OAI.ScalarConductivity.physicalOuter_smooth_sq_bound line 125
9. def OAI.ScalarConductivity.smoothPiH1L line 183
10. lemma OAI.ScalarConductivity.smoothPiH1L_dense line 220