OAI/MeasureTheory/Falconer/Graphs/JetStateGraph.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The profile graph estimate on the exact factorized state class

This packages the geometric hypotheses of the proved graph estimate. The child envelope uses exactly the original list with anchors at most p removed, and the same normalization and smooth multipliers.

  1. structure OAI.Falconer.JetStateGraphData line 21
  2. def OAI.Falconer.JetStateGraphData.coefficient line 91
  3. def OAI.Falconer.JetStateGraphData.error line 98
  4. abbrev OAI.Falconer.JetStateGraphData.symbol line 108
  5. def OAI.Falconer.JetStateGraphData.childMaximum line 112
  6. theorem OAI.Falconer.JetStateGraphData.symbol_parallel_test line 117
  7. theorem OAI.Falconer.JetStateGraphData.coefficient_nonneg line 138
  8. theorem OAI.Falconer.JetStateGraphData.error_nonneg line 142
  9. theorem OAI.Falconer.exists_jetState_graph_step line 151