OAI/MeasureTheory/Falconer/Graphs/GraphEnergyEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The graph energy estimate before profile normalization

This assembles the exact splitting, proved localization and retained Schur bound. All endpoint symbols, including reached anchor masks, remain unchanged on children. The numerical error is explicit.

  1. def OAI.Falconer.capGraphError line 18
  2. theorem OAI.Falconer.dyadic_graph_energy_step line 26