OAI/MeasureTheory/Falconer/Estimates/TwoPolicyEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Separating the exact left and right policy symbols

Each self energy retains its own original regularized measure, descriptor list, mask family and scalar normalization.

  1. def OAI.Falconer.PolicyJetData.diagonal line 18
  2. def OAI.Falconer.PolicyJetData.endpoint line 22
  3. theorem OAI.Falconer.PolicyJetData.endpoint_measurable line 29
  4. def OAI.Falconer.PolicyJetData.endpointBound line 36
  5. theorem OAI.Falconer.PolicyJetData.endpointBound_nonneg line 42
  6. theorem OAI.Falconer.PolicyJetData.endpoint_norm_le line 49
  7. theorem OAI.Falconer.PolicyJetData.endpoint_self_energy_le line 57
  8. theorem OAI.Falconer.two_policy_energy_le line 71