OAI/MeasureTheory/Falconer/Graphs/TwoGraphChildren.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Separate self energies for the children of a two-profile graph

  1. def OAI.Falconer.JetStateGraphData.selfChildMaximum line 15
  2. theorem OAI.Falconer.JetStateGraphData.selfChildMaximum_nonneg line 21
  3. def OAI.Falconer.JetStateGraphData.childTransform line 25
  4. theorem OAI.Falconer.JetStateGraphData.child_self_energy_le line 31
  5. theorem OAI.Falconer.two_graph_child_energy_le line 47