OAI/MeasureTheory/Falconer/Geometry/InactiveBinGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.AngularBinActive line 13
2. def OAI.PlanarFalconer.inactiveAngularLabels line 16
3. theorem OAI.PlanarFalconer.inactiveAngularLabels_separation line 19
4. theorem OAI.PlanarFalconer.inactive_angular_sum_support line 26
5. theorem OAI.PlanarFalconer.sourceUnitDirection_dist_sq line 42
6. theorem OAI.PlanarFalconer.sine_separation_of_forward_chord line 48
7. theorem OAI.PlanarFalconer.inactive_bin_sine_separation line 60