OAI/Probability/SignedSweeps/UniformMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.coefficient_mono_depth line 10
2. lemma OAI.SignedSweeps.signed_sweep_recurrence_depth_sum line 18
3. theorem OAI.SignedSweeps.signed_occurrence_moment_bound_fixed line 40
4. theorem OAI.SignedSweeps.signed_occurrence_moment_bound line 128

   Distinct definitions of this name: ComparatorChallenges/SignedSweepMoment.lean:169 (same statement text; different proof or body). Qualify references as OAI.SignedSweeps.signed_occurrence_moment_bound@path.