OAI/Analysis/Conductivity/Branching/PhysicalChildIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.sourceChild_integral line 13
2. lemma OAI.ScalarConductivity.originalPiGradient_memLp_on_ball line 25
3. lemma OAI.ScalarConductivity.originalPiGradient_eq_on_ball line 35
4. lemma OAI.ScalarConductivity.sourceChild_image_ball line 47
5. lemma OAI.ScalarConductivity.sourceChildTensorPush_entry_memLp line 63
6. lemma OAI.ScalarConductivity.sourceChildTensorPush_weak_integrable line 81
7. theorem OAI.ScalarConductivity.physicalChildFullEnd_weak_energy_exists line 111