OAI/MeasureTheory/Falconer/Fourier/PolicyJetChildren.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual policy states at the child cells of an angular step

  1. def OAI.Falconer.PolicyJetData.child line 15
  2. theorem OAI.Falconer.PolicyJetData.child_envelope line 57
  3. theorem OAI.Falconer.PolicyJetData.graphChild_le line 72
  4. theorem OAI.Falconer.PolicyJetData.nearBound_eq line 83