OAI/Combinatorics/SumProduct/Alignment/HarmonicExposure02.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RoughFaceShift.source_conditional_face_decay line 26
2. structure OAI.RoughFaceShift.Exposure line 93
3. def OAI.RoughFaceShift.Exposure.Legal line 101
4. theorem OAI.RoughFaceShift.conditional_face_uniform line 109
5. def OAI.HarmonicExposure.pivotFiber line 230
6. lemma OAI.HarmonicExposure.pivot_parameter_nonneg line 233
7. theorem OAI.HarmonicExposure.pivotMass_eq_raw line 241
8. lemma OAI.HarmonicExposure.residue_unit line 295
9. def OAI.HarmonicExposure.rawFiberMass line 306
10. theorem OAI.HarmonicExposure.rawFiberMass_eq_exposed line 311