OAI/MeasureTheory/Falconer/Incidence/WideProductIncidence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Product incidence for the actual width-three packet geometry. The rounding and bounded-chart normalization are performed inside the proof; separation of the original union is not required.

  1. theorem OAI.Falconer.wide_product_incidence line 12