OAI/MeasureTheory/Falconer/Graphs/TwoProfileGraph.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The graph reduction for two original regularized profiles

Only geometric scales are shared. The laws, profiles, descriptor lists, mask families and endpoint multipliers remain separate.

  1. structure OAI.Falconer.JetGraphAlignment line 15
  2. def OAI.Falconer.JetStateGraphData.twoProfileCoefficient line 30
  3. def OAI.Falconer.JetStateGraphData.twoProfileError line 38
  4. theorem OAI.Falconer.exists_two_profile_graph_step line 50