OAI/Combinatorics/SumProduct/Alignment/HarmonicExposure01.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RoughFaceShift.source_face_decay line 26
2. def OAI.HarmonicExposure.pivotMass line 148
3. def OAI.HarmonicExposure.exposedWeight line 151
4. lemma OAI.HarmonicExposure.pivot_bounds line 154
5. lemma OAI.HarmonicExposure.exposed_weight_bounds line 200
6. lemma OAI.HarmonicExposure.weighted_fraction_bound line 236
7. theorem OAI.HarmonicExposure.conditional_fraction_le line 256