OAI/Analysis/Conductivity/Flux/AttachedPhysicalSmoothGreen.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.physicalSmoothOuterTrace line 15
2. def OAI.ScalarConductivity.physicalEndLength line 20
3. lemma OAI.ScalarConductivity.H1JetOn.attached_gradient line 22
4. lemma OAI.ScalarConductivity.attached_child_end_energy_pullback line 30
5. lemma OAI.ScalarConductivity.attached_parent_jet_smooth_green line 67
6. lemma OAI.ScalarConductivity.attached_child_jet_smooth_green line 87
7. lemma OAI.ScalarConductivity.attached_physical_jet_smooth_green line 106
8. lemma OAI.ScalarConductivity.attached_physical_end_smooth_green line 121
9. lemma OAI.ScalarConductivity.attached_block_smooth_green line 152
10. theorem OAI.ScalarConductivity.physical_attached_smooth_green_exists line 176