OAI/Analysis/Conductivity/Geometry/PhysicalCollarBand.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.squareFace_scaled_surjective line 12
2. def OAI.ScalarConductivity.sourceClosedCollarBand line 22
3. lemma OAI.ScalarConductivity.sourceRadial_pos_of_time line 25
4. lemma OAI.ScalarConductivity.sourceCollarPiece_cover_extended line 35
5. lemma OAI.ScalarConductivity.sourcePhysicalCoordinates_right line 72
6. lemma OAI.ScalarConductivity.sourceClosedCollarBand_eq line 86
7. lemma OAI.ScalarConductivity.isCompact_sourceClosedCollarBand line 106
8. lemma OAI.ScalarConductivity.sourceDirection_ne_zero_of_time line 115
9. lemma OAI.ScalarConductivity.sourceClosedCollarBand_measure_le line 133
10. lemma OAI.ScalarConductivity.sourceClosedCollarBand_memLp line 151