OAI/Analysis/Conductivity/Branching/PhysicalFiniteEndingData.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ScalarConductivity.PhysicalFiniteEndingData line 12
2. lemma OAI.ScalarConductivity.physicalFiniteEndingData_nonempty line 21
3. def OAI.ScalarConductivity.PhysicalFiniteEndingData.traces line 33
4. def OAI.ScalarConductivity.PhysicalFiniteEndingData.compression line 35
5. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.ending_R_pos line 38
6. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.compression_parent line 41
7. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.compression_child line 46
8. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.compression_ne line 50
9. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.end_length line 53
10. def OAI.ScalarConductivity.PhysicalFiniteEndingData.correctedEndJet line 62
11. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.correction_initial_zero line 66
12. theorem OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_pair_exists line 73