OAI/MeasureTheory/Falconer/Graphs/ProfileGraph.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Profile normalization of the retained graph contribution

The sum is over the actual occupied descendants and retains both endpoint symbols. The degree is the integer degree used in the graph energy estimate.

  1. theorem OAI.Falconer.two_profile_graph_prefactor line 16
  2. def OAI.Falconer.twoProfileGraphContribution line 40
  3. theorem OAI.Falconer.two_profile_graph_contribution_bound line 53