OAI/MeasureTheory/Falconer/Estimates/PolicyEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual energies represented by scalar branch states

The context fixes the original measure, masks and profile. The constructors carry the actual positive count or angular envelope, and the positive case records the cell separation supplied by the far partition.

  1. structure OAI.Falconer.PolicyContext line 16
  2. def OAI.Falconer.PolicyJetData.context line 30
  3. inductive OAI.Falconer.PolicyEnergy line 33
  4. theorem OAI.Falconer.PolicyJetData.context_child line 47
  5. theorem OAI.Falconer.PolicyJetData.context_positiveSuccessor line 53
  6. theorem OAI.Falconer.PolicyJetData.context_farPositiveSuccessor line 56
  7. theorem OAI.Falconer.PolicyJetData.energy_farPositiveSuccessor line 62
  8. theorem OAI.Falconer.PolicyJetData.energy_child line 73
  9. theorem OAI.Falconer.PolicyJetData.energy_positiveSuccessor line 81