OAI/Probability/GaussianPropeller/SpanReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.Reduction.sqrt_value_lower line 36
2. lemma OAI.GaussianPropeller.Reduction.normalize_pair_constant line 48
3. theorem OAI.GaussianPropeller.Reduction.minimal_normalized_pair line 77
4. theorem OAI.GaussianPropeller.Reduction.sum_cell_probability line 97
5. theorem OAI.GaussianPropeller.Reduction.sum_active_probability line 108
6. theorem OAI.GaussianPropeller.Reduction.sum_active_norm_sq line 120
7. theorem OAI.GaussianPropeller.Reduction.sum_active_radius_sq line 130