OAI/MeasureTheory/Falconer/Graphs/EligibleProductGraphSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.graphProductSlotBin line 10
2. def OAI.PlanarFalconer.GraphProductEligible line 12
3. theorem OAI.PlanarFalconer.angular_label_eligible_of_transform_ne_zero line 16
4. theorem OAI.PlanarFalconer.sourceGraphFourTransform_product_eligible_of_ne_zero line 23
5. theorem OAI.PlanarFalconer.graphOriginalProductTerm_zero_of_ineligible line 44
6. def OAI.PlanarFalconer.GraphProductIndexEligible line 55
7. def OAI.PlanarFalconer.graphProductEligibleIndices line 59
8. theorem OAI.PlanarFalconer.graphOriginalProductSum_eligible line 65
9. theorem OAI.PlanarFalconer.graphProductIndexEligible_witness line 82