OAI/MeasureTheory/Falconer/Graphs/ProfileGraphBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The model masses pay for both graph errors

The child masses cancel before estimating. Only the two parent profile values remain, so the combined normalization costs at most R^(5d).

  1. theorem OAI.Falconer.graph_error_mass_cancellation line 14
  2. theorem OAI.Falconer.profile_graph_error_weight_bound line 21