OAI/Probability/BinarySweep/Analytic/OneAxisPerturbation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.oneAxis_gridWeight_affine line 13
2. lemma OAI.BinaryCoordinateSweeps.oneAxis_gridWeight_one_nonneg line 18
3. lemma OAI.BinaryCoordinateSweeps.oneAxis_conditional_norm_le_z_div line 23
4. lemma OAI.BinaryCoordinateSweeps.oneAxis_normalizer_lower line 72
5. theorem OAI.BinaryCoordinateSweeps.oneAxis_conditional_norm_le line 95